Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file Memory.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688(**************************************************************************)(* *)(* This file is part of WP plug-in of Frama-C. *)(* *)(* Copyright (C) 2007-2025 *)(* CEA (Commissariat a l'energie atomique et aux energies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file licenses/LGPLv2.1). *)(* *)(**************************************************************************)(* -------------------------------------------------------------------------- *)(** Common Types and Signatures *)(* -------------------------------------------------------------------------- *)openCil_typesopenCtypesopenLang.FopenInterpreted_automataopenSigma(* -------------------------------------------------------------------------- *)(** {1 General Definitions} *)(* -------------------------------------------------------------------------- *)type'asequence={pre:'a;post:'a}type'abinder={bind:'b'c.'a->('b->'c)->'b->'c}(** Oriented equality or arbitrary relation *)typeequation=|Setofterm*term(** [Set(a,b)] is [a := b]. *)|Assertofpred(** Access conditions *)typeacs=|RW(** Read-Write Access *)|RD(** Read-Only Access *)|OBJ(** Valid Object Pointer *)(** Abstract location or concrete value *)type'avalue=|Valofterm|Locof'a(** Contiguous set of locations *)type'arloc=|Rlocofc_object*'a|Rrangeof'a*c_object*termoption*termoption(** Structured set of locations *)type'asloc=|Slocof'a|Sarrayof'a*c_object*int(** full sized range (optimized assigns) *)|Srangeof'a*c_object*termoption*termoption|Sdescrofvarlist*'a*pred(** Typed set of locations *)type'aregion=(c_object*'asloc)list(** Logical values, locations, or sets of *)type'alogic=|Vexpofterm|Vlocof'a|VsetofVset.set|Lsetof'asloclist(** Scope management for locals and formals *)typescope=Enter|Leave(** Container for the returned value of a function *)type'aresult=|R_locof'a|R_varofvar(** Polarity of predicate compilation *)typepolarity=[`Positive|`Negative|`NoPolarity](* -------------------------------------------------------------------------- *)(** {1 Reversing Models}
It is sometimes possible to reverse memory models abstractions
into ACSL left-values via the definitions below. *)(* -------------------------------------------------------------------------- *)(** Reversed ACSL left-value *)types_lval=s_host*s_offsetlistands_host=|Mvarofvarinfo(** Variable *)|Mmemofterm(** Pointed value *)|Mvalofs_lval(** Pointed value of another abstract left-value *)ands_offset=Mfieldoffieldinfo|Mindexofterm(** Reversed abstract value *)typemval=|Maddrofs_lval(** The value is the address of an l-value in current memory *)|Mlvalofs_lval(** The value is the value of an l-value in current memory *)|Minitofs_lval(** The value is the init state of an l-value in current memory *)|MchunkofChunk.t(** The value is an abstract memory chunk (description) *)(** Reversed update *)typeupdate=Mstoreofs_lval*term(** An update of the ACSL left-value with the given value *)(* -------------------------------------------------------------------------- *)(** {1 Memory Models} *)(* -------------------------------------------------------------------------- *)(** Memory Models. *)moduletypeModel=sig(** {2 Model Definition} *)valconfigure:unit->WpContext.rollback(** Initializers to be run before using the model.
Typically push {!Context} values and returns a function to rollback. *)valconfigure_ia:automaton->vertexbinder(** Given an automaton, return a vertex's binder.
Currently used by the automata compiler to bind current vertex.
See {!StmtSemantics}. *)valdatatype:string(** For projectification. Must be unique among models. *)valhypotheses:MemoryContext.partition->MemoryContext.partition(** Computes the memory model partitionning of the memory locations.
This function typically adds new elements to the partition received
in input (that can be empty). *)typeloc(** Representation of the memory location in the model. *)typesegment=locrloc(** {2 Reversing the Model} *)(** Try to interpret a term as an in-memory operation
located at this program point. Only best-effort
shall be performed, otherwise return [Mvalue].
Recognized [Cil] patterns:
- [Mvar x,[Mindex 0]] is rendered as [*x] when [x] has a pointer type
- [Mmem p,[Mfield f;...]] is rendered as [p->f...] like in Cil
- [Mmem p,[Mindex k;...]] is rendered as [p[k]...] to catch Cil [Mem(AddPI(p,k)),...] *)vallookup:state->term->mval(** Try to interpret a sequence of states into updates.
The result shall be exhaustive with respect to values that are printed as [Memory.mval]
values at [post] label {i via} the [lookup] function.
Otherwise, those values would not be pretty-printed to the user. *)valupdates:statesequence->Vars.t->updateBag.tvalpretty:Format.formatter->loc->unit(** pretty printing of memory location *)(** {2 Memory Model API} *)valvars:loc->Vars.t(** Return the logic variables from which the given location depend on. *)valoccurs:var->loc->bool(** Test if a location depend on a given logic variable *)valnull:loc(** Return the location of the null pointer *)valliteral:eid:int->Cstring.cst->loc(** Return the memory location of a constant string,
the id is a unique identifier. *)valcvar:varinfo->loc(** Return the location of a C variable. *)valpointer_loc:term->loc(** Interpret an address value (a pointer) as an abstract location.
Might fail on memory models not supporting pointers. *)valpointer_val:loc->term(** Return the adress value (a pointer) of an abstract location.
Might fail on memory models not capable of representing pointers. *)valfield:loc->fieldinfo->loc(** Return the memory location obtained by field access from a given
memory location. *)valshift:loc->c_object->term->loc(** Return the memory location obtained by array access at an index
represented by the given {!term}. The element of the array are of
the given {!c_object} type. *)valbase_addr:loc->loc(** Return the memory location of the base address of a given memory
location. *)valbase_offset:loc->term(** Return the offset of the location, in bytes, from its base_addr. *)valblock_length:sigma->c_object->loc->term(** Returns the length (in bytes) of the allocated block containing
the given location. *)valcast:c_objectsequence->loc->loc(** Cast a memory location into another memory location.
For [cast ty loc] the cast is done from [ty.pre] to [ty.post].
Might fail on memory models not supporting pointer casts. *)valloc_of_int:c_object->term->loc(** Cast a term representing an absolute memory address (to some c_object)
given as an integer, into an abstract memory location. *)valint_of_loc:c_int->loc->term(** Cast a memory location into its absolute memory address,
given as an integer with the given C-type. *)valdomain:c_object->loc->domain(** Compute the set of chunks that hold the value of an object with
the given C-type. It is safe to retun an over-approximation of the
chunks involved. *)valis_well_formed:sigma->pred(** Provides the constraint corresponding to the kind of data stored by all
chunks in sigma. *)valload:sigma->c_object->loc->locvalue(** Return the value of the object of the given type at the given location in
the given memory state. *)valload_init:sigma->c_object->loc->term(** Return the initialization status at the given location in the given
memory state. *)valcopied:sigmasequence->c_object->loc->loc->equationlist(**
Return a set of equations that express a copy between two memory state.
[copied sigma ty loc1 loc2] returns a set of formula expressing that the
content for an object [ty] is the same in [sigma.pre] at [loc1] and in
[sigma.post] at [loc2].
*)valcopied_init:sigmasequence->c_object->loc->loc->equationlist(**
Return a set of equations that express a copy of an initialized state
between two memory state.
[copied sigma ty loc1 loc2] returns a set of formula expressing that the
initialization status for an object [ty] is the same in [sigma.pre] at
[loc1] and in [sigma.post] at [loc2].
*)valstored:sigmasequence->c_object->loc->term->equationlist(**
Return a set of formula that express a modification between two memory
state.
[stored sigma ty loc t] returns a set of formula expressing that
[sigma.pre] and [sigma.post] are identical except for an object [ty] at
location [loc] which is represented by [t] in [sigma.post].
*)valstored_init:sigmasequence->c_object->loc->term->equationlist(**
Return a set of formula that express a modification of the initialization
status between two memory state.
[stored_init sigma ty loc t] returns a set of formula expressing that
[sigma.pre] and [sigma.post] are identical except for an object [ty] at
location [loc] which has a new init represented by [t] in [sigma.post].
*)valassigned:sigmasequence->c_object->locsloc->equationlist(**
Return a set of formula that express that two memory state are the same
except at the given set of memory location.
This function can over-approximate the set of given memory location (e.g
it can return [true] as if the all set of memory location was given).
*)valis_null:loc->pred(** Return the formula that check if a given location is null *)valloc_eq:loc->loc->predvalloc_lt:loc->loc->predvalloc_neq:loc->loc->predvalloc_leq:loc->loc->pred(** Memory location comparisons *)valloc_diff:c_object->loc->loc->term(** Compute the length in bytes between two memory locations *)valvalid:sigma->acs->segment->pred(** Return the formula that tests if a memory state is valid
(according to {!acs}) in the given memory state at the given
segment.
*)valframe:sigma->predlist(** Assert the memory is a proper heap state preceeding the function
entry point. *)valalloc:sigma->varinfolist->sigma(** Allocates new chunk for the validity of variables. *)valinitialized:sigma->segment->pred(** Return the formula that tests if a memory state is initialized
(according to {!acs}) in the given memory state at the given
segment.
*)valinvalid:sigma->segment->pred(** Returns the formula that tests if the entire memory is invalid
for write access. *)valscope:sigmasequence->scope->varinfolist->predlist(** Manage the scope of variables. Returns the updated memory model
and hypotheses modeling the new validity-scope of the variables. *)valglobal:sigma->term->pred(** Given a pointer value [p], assumes this pointer [p] (when valid)
is allocated outside the function frame under analysis. This means
separated from the formals and locals of the function. *)valincluded:segment->segment->pred(** Return the formula that tests if two segment are included *)valseparated:segment->segment->pred(** Return the formula that tests if two segment are separated *)end(* -------------------------------------------------------------------------- *)(** {1 C and ACSL Compilers} *)(* -------------------------------------------------------------------------- *)(** Compiler for C expressions *)moduletypeCodeSemantics=sigmoduleM:Model(** The underlying memory model *)typeloc=M.loctypenonrecvalue=locvaluetypenonrecresult=locresultvalpp_value:Format.formatter->value->unitvalcval:value->term(** Evaluate an abstract value. May fail because of [M.pointer_val]. *)valcloc:value->loc(** Interpret a value as a location. May fail because of [M.pointer_loc]. *)valcast:typ->typ->value->value(** Applies a pointer cast or a conversion.
[cast tr te ve] transforms a value [ve] with type [te] into a value
with type [tr]. *)valequal_typ:typ->value->value->pred(** Computes the value of [(a==b)] provided both [a] and [b] are values
with the given type. *)valnot_equal_typ:typ->value->value->pred(** Computes the value of [(a==b)] provided both [a] and [b] are values
with the given type. *)valequal_obj:c_object->value->value->pred(** Same as [equal_typ] with an object type. *)valnot_equal_obj:c_object->value->value->pred(** Same as [not_equal_typ] with an object type. *)valexp:sigma->exp->value(** Evaluate the expression on the given memory state. *)valcond:sigma->exp->pred(** Evaluate the conditional expression on the given memory state. *)vallval:sigma->lval->loc(** Evaluate the left-value on the given memory state. *)valcall:sigma->exp->loc(** Address of a function pointer.
Handles [AddrOf], [StartOf] and [Lval] as usual. *)valinstance_of:loc->kernel_function->pred(** Check whether a function pointer is (an instance of)
some kernel function. Currently, the meaning
of "{i being an instance of}" is simply equality. *)valloc_of_exp:sigma->exp->loc(** Compile an expression as a location.
May (also) fail because of [M.pointer_val]. *)valval_of_exp:sigma->exp->term(** Compile an expression as a term.
May (also) fail because of [M.pointer_loc]. *)valresult:sigma->typ->result->term(** Value of an abstract result container. *)valreturn:sigma->typ->exp->term(** Return an expression with a given type.
Short cut for compiling the expression, cast into the desired type,
and finally converted to a term. *)valis_zero:sigma->c_object->loc->pred(** Express that the object (of specified type) at the given location
is filled with zeroes. *)(**
Express that all objects in a range of locations have a given value.
More precisely, [is_exp_range sigma loc ty a b v] express that
value at [( ty* )loc + k] equals [v], forall [a <= k <= b].
Value [v=None] stands for zero.
*)valis_exp_range:sigma->loc->c_object->term->term->valueoption->predvalunchanged:sigma->sigma->varinfo->pred(** Express that a given variable has the same value in two memory states. *)typewarned_hyp=Warning.Set.t*(pred*pred)valinit:sigma:sigma->varinfo->initoption->warned_hyplist(** Express that some variable has some initial value at the
given memory state. The first predicate states the value,
the second, the initialization status.
Note: we DO NOT merge values and initialization status
hypotheses as the factorization performed by Qed can make
predicates too hard to simplify later.
Remark: [None] initializer are interpreted as zeroes. This is consistent
with the [init option] associated with global variables in CIL,
for which the default initializer are zeroes. This function is called
for global initializers and local initializers ([Cil.Local_init]).
It is not called for local variables without initializers as they do not
have a [Cil.init option].
*)end(** Compiler for ACSL expressions *)moduletypeLogicSemantics=sigmoduleM:Model(** Underlying memory model *)typeloc=M.loctypenonrecvalue=M.locvaluetypenonreclogic=M.loclogictypenonrecregion=M.locregiontypenonrecresult=M.locresult(** {2 Frames}
Frames are compilation environment for ACSL. A frame typically
manages the current function, formal paramters, the memory environments
at different labels and the [\result] and [\exit_status] values.
The frame also holds the {i gamma} environment responsible for
accumulating typing constraints, and the {i pool} for generating
fresh logic variables.
Notice that a [frame] is not responsible for holding the environment
at label [Here], since this is managed by a specific compilation
environment, see {!env} below.
*)typeframevalpp_frame:Format.formatter->frame->unit(** Get the current frame, or raise a fatal error if none. *)valget_frame:unit->frame(** Execute the given closure with the specified current frame.
The [Lang.gamma] and [Lang.pool] contexts are also set accordingly. *)valin_frame:frame->('a->'b)->'a->'b(** Get the memory environment at the given label.
A fresh environment is created lazily if required.
The label must {i not} be [Here]. *)valmem_at_frame:frame->Clabels.c_label->sigma(** Update a frame with a specific environment for the given label. *)valset_at_frame:frame->Clabels.c_label->sigma->unit(** Chek if a frame already has a specific envioronement for the given label. *)valhas_at_frame:frame->Clabels.c_label->bool(** Same as [mem_at_frame] but for the current frame. *)valmem_frame:Clabels.c_label->sigma(** Full featured constructor for frames, with fresh pool and gamma. *)valmk_frame:?kf:Cil_types.kernel_function->?result:result->?status:Lang.F.var->?formals:valueCil_datatype.Varinfo.Map.t->?labels:sigmaClabels.LabelMap.t->?descr:string->unit->frame(** Make a local frame reusing the {i current} pool and gamma. *)vallocal:descr:string->frame(** Make a fresh frame with the given function. *)valframe:kernel_function->frametypecall(** Internal call data. *)(** Create call data from the callee point of view,
deriving data (gamma and pools) from the current frame.
If [result] is specified, the called function will stored its result
at the provided location in the current frame (the callee). *)valcall:?result:M.loc->kernel_function->valuelist->call(** Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state. *)valcall_pre:sigma->call->sigma->frame(** Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state and post-state. *)valcall_post:sigma->call->sigmasequence->frame(** Result type of the current function in the current frame. *)valreturn:unit->typ(** Result location of the current function in the current frame. *)valresult:unit->result(** Exit status for the current frame. *)valstatus:unit->var(** Returns the current gamma environment from the current frame. *)valguards:frame->predlist(** {2 Compilation Environment} *)typeenv(**
Compilation environment for terms and predicates. Manages
the {i current} memory state and the memory state at [Here].
Remark: don't confuse the {i current} memory state with the
memory state {i at label} [Here]. The current memory state is the one
we have at hand when compiling a term or a predicate. Hence, inside
[\at(e,L)] the current memory state when compiling [e] is the one at [L].
*)(** Create a new environment.
Current and [Here] memory points are initialized to [~here], if
provided.
The logic variables stand for
formal parameters of ACSL logic function and ACSL predicates. *)valmk_env:?here:sigma->?lvars:logic_varlist->unit->env(** The {i current} memory state. Must be propertly initialized
with a specific {!move} before. *)valcurrent:env->sigma(** Move the compilation environment to the specified [Here] memory state.
This memory state becomes also the new {i current} one. *)valmove_at:env->sigma->env(** Returns the memory state at the requested label.
Uses the local environment for [Here] and the current frame
otherwize. *)valmem_at:env->Clabels.c_label->sigma(** Returns a new environment where the current memory state is
moved to to the corresponding label. Suitable for compiling [e] inside
[\at(e,L)] ACSL construct. *)valenv_at:env->Clabels.c_label->env(** {2 Compilers} *)(** Compile a term l-value into a (typed) abstract location *)vallval:env->Cil_types.term_lval->Cil_types.typ*M.loc(** Compile a term expression. *)valterm:env->Cil_types.term->term(** Compile a predicate. The polarity is used to generate a weaker or
stronger predicate in case of unsupported feature from WP or the
underlying memory model. *)valpred:polarity->env->Cil_types.predicate->pred(** Compile a predicate call. *)valcall_pred:env->Cil_types.logic_info->Cil_types.logic_labellist->termlist->pred(** Compile a term representing a set of memory locations into an abstract
region. *)valregion:env->Cil_types.term->region(** Computes the region assigned by a list of froms. *)valassigned_of_lval:env->Cil_types.lval->region(** Computes the region assigned by a list of froms. *)valassigned_of_froms:env->fromlist->region(** Computes the region assigned by an assigns clause.
[None] means everyhting is assigned. *)valassigned_of_assigns:env->assigns->regionoption(** Same as [term] above but reject any set of locations. *)valval_of_term:env->Cil_types.term->term(** Same as [term] above but expects a single loc or a single
pointer value. *)valloc_of_term:env->Cil_types.term->loc(** Compile a lemma definition. *)vallemma:LogicUsage.logic_lemma->Definitions.dlemma(** {2 Regions} *)(** Qed variables appearing in a region expression. *)valvars:region->Vars.t(** Member of vars. *)valoccurs:var->region->bool(** Check assigns inclusion.
Compute a formula that checks whether written locations are either
invalid (at the given memory location) or included in some assignable
region. When [~unfold:n && n <> 0], compound memory locations are expanded
field-by-field and arrays, cell-by-cell (by quantification). Up to [n]
levels are unfolded, -1 means unlimited. *)valcheck_assigns:unfold:int->sigma->written:region->assignable:region->predend(** Compiler for Performing Assigns *)moduletypeLogicAssigns=sigmoduleM:ModelmoduleL:LogicSemanticswithmoduleM=MopenM(** Memory footprint of a region. *)valdomain:locregion->Heap.set(** Relates two memory states corresponding to an assigns clause
with the specified set of locations. *)valapply_assigns:sigmasequence->locregion->predlistend(** All Compilers Together *)moduletypeCompiler=sigmoduleM:ModelmoduleC:CodeSemanticswithmoduleM=MmoduleL:LogicSemanticswithmoduleM=MmoduleA:LogicAssignswithmoduleM=MandmoduleL=Lend