Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file constrSys.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299(** {{!MonSystem} constraint system} signatures. *)openBatteriesmoduletypeSysVar=sigtypetvalis_write_only:t->boolendmoduletypeVarType=sigincludeHashtbl.HashedTypeincludeSysVarwithtypet:=tvalpretty_trace:unit->t->GoblintCil.Pretty.docvalcompare:t->t->intvalprintXml:'aBatInnerIO.output->t->unitvalvar_id:t->stringvalnode:t->MyCFG.nodevalrelift:t->t(* needed only for incremental+hashcons to re-hashcons contexts after loading *)end(** Abstract incremental change to constraint system.
@param 'v constrain system variable type *)type'vsys_change_info={obsolete:'vlist;(** Variables to destabilize. *)delete:'vlist;(** Variables to delete. *)reluctant:'vlist;(** Variables to solve reluctantly. *)restart:'vlist;(** Variables to restart. *)}(** A side-effecting system. *)moduletypeMonSystem=sigtypev(* variables *)typed(* values *)type'am(* basically a monad carrier *)(** Variables must be hashable, comparable, etc. *)moduleVar:VarTypewithtypet=v(** Values must form a lattice. *)moduleDom:Lattice.Swithtypet=d(** The system in functional form. *)valsystem:v->((v->d)->(v->d->unit)->d)mvalsys_change:(v->d)->vsys_change_info(** Compute incremental constraint system change from old solution. *)end(** Any system of side-effecting equations over lattices. *)moduletypeEqConstrSys=MonSystemwithtype'am:='aoption(** A side-effecting system with globals. *)moduletypeGlobConstrSys=sigmoduleLVar:VarTypemoduleGVar:VarTypemoduleD:Lattice.SmoduleG:Lattice.Svalsystem:LVar.t->((LVar.t->D.t)->(LVar.t->D.t->unit)->(GVar.t->G.t)->(GVar.t->G.t->unit)->D.t)optionvaliter_vars:(LVar.t->D.t)->(GVar.t->G.t)->VarQuery.t->LVar.tVarQuery.f->GVar.tVarQuery.f->unitvalsys_change:(LVar.t->D.t)->(GVar.t->G.t)->[`LofLVar.t|`GofGVar.t]sys_change_infoend(** A solver is something that can translate a system into a solution (hash-table).
Incremental solver has data to be marshaled. *)moduletypeGenericEqIncrSolverBase=functor(S:EqConstrSys)->functor(H:Hashtbl.Swithtypekey=S.v)->sigtypemarshalvalcopy_marshal:marshal->marshalvalrelift_marshal:marshal->marshal(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
reached from starting values [xs].
As a second component the solver returns data structures for incremental serialization. *)valsolve:(S.v*S.d)list->S.vlist->marshaloption->S.dH.t*marshalend(** (Incremental) solver argument, indicating which postsolving should be performed by the solver. *)moduletypeIncrSolverArg=sigvalshould_prune:boolvalshould_verify:boolvalshould_warn:boolvalshould_save_run:boolend(** An incremental solver takes the argument about postsolving. *)moduletypeGenericEqIncrSolver=functor(Arg:IncrSolverArg)->GenericEqIncrSolverBase(** A solver is something that can translate a system into a solution (hash-table) *)moduletypeGenericEqSolver=functor(S:EqConstrSys)->functor(H:Hashtbl.Swithtypekey=S.v)->sig(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
reached from starting values [xs]. *)valsolve:(S.v*S.d)list->S.vlist->S.dH.tend(** A solver is something that can translate a system into a solution (hash-table) *)moduletypeGenericGlobSolver=functor(S:GlobConstrSys)->functor(LH:Hashtbl.Swithtypekey=S.LVar.t)->functor(GH:Hashtbl.Swithtypekey=S.GVar.t)->sigtypemarshalvalcopy_marshal:marshal->marshalvalrelift_marshal:marshal->marshal(** The hash-map that is the first component of [solve xs vs] is a local solution for interesting variables [vs],
reached from starting values [xs].
As a second component the solver returns data structures for incremental serialization. *)valsolve:(S.LVar.t*S.D.t)list->(S.GVar.t*S.G.t)list->S.LVar.tlist->marshaloption->(S.D.tLH.t*S.G.tGH.t)*marshalend(** Combined variables so that we can also use the more common [EqConstrSys]
that uses only one kind of a variable. *)moduleVar2(LV:VarType)(GV:VarType):VarTypewithtypet=[`LofLV.t|`GofGV.t]=structtypet=[`LofLV.t|`GofGV.t][@@derivingeq,ord,hash]letrelift=function|`Lx->`L(LV.reliftx)|`Gx->`G(GV.reliftx)letpretty_trace()=function|`La->GoblintCil.Pretty.dprintf"L:%a"LV.pretty_tracea|`Ga->GoblintCil.Pretty.dprintf"G:%a"GV.pretty_tracealetprintXmlf=function|`La->LV.printXmlfa|`Ga->GV.printXmlfaletvar_id=function|`La->LV.var_ida|`Ga->GV.var_idaletnode=function|`La->LV.nodea|`Ga->GV.nodealetis_write_only=function|`La->LV.is_write_onlya|`Ga->GV.is_write_onlyaend(** Translate a [GlobConstrSys] into a [EqConstrSys] *)moduleEqConstrSysFromGlobConstrSys(S:GlobConstrSys):EqConstrSyswithtypev=Var2(S.LVar)(S.GVar).tandtyped=Lattice.Lift2(S.G)(S.D).tandmoduleVar=Var2(S.LVar)(S.GVar)andmoduleDom=Lattice.Lift2(S.G)(S.D)=structmoduleVar=Var2(S.LVar)(S.GVar)moduleDom=structincludeLattice.Lift2(S.G)(S.D)letprintXmlf=function|`Lifted1a->S.G.printXmlfa|`Lifted2a->S.D.printXmlfa|(`Bot|`Top)asx->printXmlfxendtypev=Var.ttyped=Dom.tletgetG=function|`Lifted1x->x|`Bot->S.G.bot()|`Top->failwith"EqConstrSysFromGlobConstrSys.getG: global variable has top value"|`Lifted2_->failwith"EqConstrSysFromGlobConstrSys.getG: global variable has local value"letgetL=function|`Lifted2x->x|`Bot->S.D.bot()|`Top->failwith"EqConstrSysFromGlobConstrSys.getL: local variable has top value"|`Lifted1_->failwith"EqConstrSysFromGlobConstrSys.getL: local variable has global value"letl,g=(funx->`Lx),(funx->`Gx)letlD,gD=(funx->`Lifted2x),(funx->`Lifted1x)letconvfgetset=f(getL%get%l)(funxv->set(lx)(lDv))(getG%get%g)(funxv->set(gx)(gDv))|>lDletsystem=function|`G_->None|`Lx->Option.mapconv(S.systemx)letsys_changeget=S.sys_change(getL%get%l)(getG%get%g)end(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)moduleGlobConstrSolFromEqConstrSolBase(S:GlobConstrSys)(LH:Hashtbl.Swithtypekey=S.LVar.t)(GH:Hashtbl.Swithtypekey=S.GVar.t)(VH:Hashtbl.Swithtypekey=Var2(S.LVar)(S.GVar).t)=structletsplit_solutionhm=letl'=LH.create113inletg'=GH.create113inletsplit_varsxd=matchxwith|`Lx->beginmatchdwith|`Lifted2d->LH.replacel'xd(* | `Bot -> () *)(* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)|`Bot->LH.replacel'x(S.D.bot())|`Top->failwith"GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"|`Lifted1_->failwith"GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"end|`Gx->beginmatchdwith|`Lifted1d->GH.replaceg'xd|`Bot->()|`Top->failwith"GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value"|`Lifted2_->failwith"GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value"endinVH.itersplit_varshm;(l',g')end(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *)moduleGlobConstrSolFromEqConstrSol(S:GlobConstrSys)(LH:Hashtbl.Swithtypekey=S.LVar.t)(GH:Hashtbl.Swithtypekey=S.GVar.t)=structmoduleS2=EqConstrSysFromGlobConstrSys(S)moduleVH=Hashtbl.Make(S2.Var)includeGlobConstrSolFromEqConstrSolBase(S)(LH)(GH)(VH)end(** Transforms a [GenericEqIncrSolver] into a [GenericGlobSolver]. *)moduleGlobSolverFromEqSolver(Sol:GenericEqIncrSolverBase)=functor(S:GlobConstrSys)->functor(LH:Hashtbl.Swithtypekey=S.LVar.t)->functor(GH:Hashtbl.Swithtypekey=S.GVar.t)->structmoduleEqSys=EqConstrSysFromGlobConstrSys(S)moduleVH:Hashtbl.Swithtypekey=EqSys.v=Hashtbl.Make(EqSys.Var)moduleSol'=Sol(EqSys)(VH)moduleSplitter=GlobConstrSolFromEqConstrSolBase(S)(LH)(GH)(VH)(* reuse EqSys and VH *)typemarshal=Sol'.marshalletcopy_marshal=Sol'.copy_marshalletrelift_marshal=Sol'.relift_marshalletsolvelsgslold_data=letvs=List.map(fun(x,v)->`Lx,`Lifted2v)ls@List.map(fun(x,v)->`Gx,`Lifted1v)gsinletsv=List.map(funx->`Lx)linlethm,solver_data=Sol'.solvevssvold_datainSplitter.split_solutionhm,solver_dataend(** [EqConstrSys] where [current_var] indicates the variable whose right-hand side is currently being evaluated. *)moduleCurrentVarEqConstrSys(S:EqConstrSys)=structletcurrent_var=refNonemoduleS=structincludeSletsystemx=matchS.systemxwith|None->None|Somef->letf'getset=letold_current_var=!current_varincurrent_var:=Somex;Fun.protect~finally:(fun()->current_var:=old_current_var)(fun()->fgetset)inSomef'endend