diff --git a/lib/goblint/runtime/src/dune b/lib/goblint/runtime/src/dune
index 0586704839..12e0e2ab9c 100644
--- a/lib/goblint/runtime/src/dune
+++ b/lib/goblint/runtime/src/dune
@@ -2,4 +2,5 @@
(archive_name goblint)
(language c)
(names goblint)
+ (flags :standard -std=c11) ; workaround for https://github.com/goblint/analyzer/issues/1779
(include_dirs ../include))
diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml
index 7857d5a543..36f0af107f 100644
--- a/src/constraint/constrSys.ml
+++ b/src/constraint/constrSys.ml
@@ -107,6 +107,18 @@ sig
val postmortem: LVar.t -> LVar.t list
end
+(** A side-effecting system with globals. *)
+module type FwdGlobConstrSys =
+sig
+ module LVar : VarType
+ module GVar : VarType
+
+ module D : Lattice.S
+ module G : Lattice.S
+ val system : LVar.t -> (D.t -> (LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> unit) option
+end
+
+
(** A side-effecting system with globals that supports [demand] calls *)
module type DemandGlobConstrSys =
sig
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index c249052271..c543f229bc 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -84,6 +84,22 @@ struct
| `Right _ -> true
end
+module GVarFCNW (V:SpecSysVar) (C:Printable.S) =
+struct
+ include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (V) (Printable.Prod (CilType.Fundec) (C))
+ let name () = "FromSpec"
+ let spec x = `Left x
+ let return (x, c) = `Right (x, c)
+
+ (* from Basetype.Variables *)
+ let var_id = show
+ let node _ = MyCFG.Function Cil.dummyFunDec
+ let pretty_trace = pretty
+ let is_write_only = function
+ | `Left x -> V.is_write_only x
+ | `Right _ -> false
+end
+
module GVarG (G: Lattice.S) (C: Printable.S) =
struct
module CSet =
@@ -116,6 +132,28 @@ struct
| x -> BatPrintf.fprintf f "%a" printXml x
end
+module GVarL (G: Lattice.S) (L: Lattice.S) =
+struct
+ include Lattice.Lift2 (G) (L)
+
+ let spec = function
+ | `Bot -> G.bot ()
+ | `Lifted1 x -> x
+ | _ -> failwith "GVarG.spec"
+ let return = function
+ | `Bot -> L.bot ()
+ | `Lifted2 x -> x
+ | _ -> failwith "GVarG.return"
+ let create_spec spec = `Lifted1 spec
+ let create_return return = `Lifted2 return
+
+ let printXml f = function
+ | `Lifted1 x -> G.printXml f x
+ | `Lifted2 x -> L.printXml f x
+ | x -> BatPrintf.fprintf f "%a" printXml x
+end
+
+
exception Deadcode
diff --git a/src/framework/bu.ml b/src/framework/bu.ml
new file mode 100644
index 0000000000..27e858829c
--- /dev/null
+++ b/src/framework/bu.ml
@@ -0,0 +1,392 @@
+open Goblint_constraint.ConstrSys
+(*
+ rhs should not query locals!
+*)
+open Messages
+
+module FwdBuSolver (System: FwdGlobConstrSys) = struct
+
+ module D = System.D
+ module G = System.G
+
+ module LS = Set.Make (System.LVar)
+
+ module GM = Hashtbl.Make(System.GVar)
+ module LM = Hashtbl.Make(System.LVar)
+
+(*
+ module OM = LM
+ let source x = x
+*)
+
+ module OM = Hashtbl.Make(Node)
+ let source = System.LVar.node
+ let gas_default = ref (10,3)
+
+ let lwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if D.equal a b then (a,delay,gas,narrow)
+ else if D.leq b a then
+ (
+ if tracing then trace "bunarrow" "Narrowing: %b" narrow;
+ if narrow then (D.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (D.narrow a b, delay,gas-1,true)
+ )
+ else if narrow then (D.join a b,delay0,gas,false)
+ else if delay <= 0 then (D.widen a (D.join a b),0,gas,false)
+ else (D.join a b, delay-1,gas,false)
+
+ let gwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if G.equal a b then (a,delay,gas,narrow)
+ else if G.leq b a then
+ if narrow then (G.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (G.narrow a b, delay,gas-1,true)
+ else if narrow then (G.join a b,delay0,gas,false)
+ else if delay <= 0 then (G.widen a (G.join a b),0,gas,false)
+ else (G.join a b, delay-1,gas,false)
+
+
+(*
+ work list just for checking ...
+*)
+
+ let work = ref (([] : System.LVar.t list), LS.empty)
+
+ let add_work x = let (l,s) = !work in
+ if LS.mem x s then ()
+ else work := (x::l, LS.add x s)
+
+ let rem_work () = let (l,s) = !work in
+ match l with
+ | [] -> None
+ | x::xs ->
+ let s = LS.remove x s in
+ let _ = work := (xs,s) in
+ Some x
+
+ type glob = {value : G.t; init : G.t; infl : LS.t ; last: G.t LM.t;
+ from : (G.t * int * int * bool * LS.t) OM.t}
+
+ let glob: glob GM.t = GM.create 100
+
+ (* auxiliary functions for globals *)
+
+ let get_global_ref g =
+ try GM.find glob g
+ with _ ->
+ (
+ if tracing then trace "unknownsize" "Number of globals so far: %d" (GM.length glob);
+ let rglob = {value = G.bot (); init = G.bot (); infl = LS.empty; last = LM.create 10; from = OM.create 10} in
+ GM.add glob g rglob;
+ rglob
+ )
+
+ let init_global (g, d) =
+ GM.add glob g {
+ value = d;
+ init = d;
+ infl = LS.empty;
+ last = LM.create 10;
+ from = OM.create 10
+ }
+
+ let get_global_value init from = OM.fold (fun _ (b,_,_,_,_) a -> G.join a b) from init
+
+ let get_old_global_value orig from =
+ try OM.find from orig
+ with _ ->
+ let (delay,gas) = !gas_default in
+ OM.add from orig (G.bot (),delay,gas,false,LS.empty);
+ (G.bot (),delay,gas,false,LS.empty)
+
+ let get_last_contrib orig set last =
+ LS.fold (fun x d -> G.join d (LM.find last x)) set (G.bot())
+
+ (* determine the join of all last contribs of unknowns with same orig *)
+
+ (* now the getters for globals *)
+
+ let get_global x g =
+ let rglob = get_global_ref g in
+ GM.replace glob g { rglob with infl = LS.add x rglob.infl }; (* ensure the global is in the hashtable *)
+ rglob.value
+
+ type loc = {loc_value : D.t; loc_init : D.t;
+ called: bool ref; aborted: bool ref;
+ loc_from : (D.t * int * int * bool) LM.t}
+(*
+ init may contain some initial value not provided by separate origin;
+ perhaps, dynamic tracking of dependencies required for certain locals?
+*)
+
+ let loc: loc LM.t = LM.create 100
+
+ (* auxiliary functions for locals *)
+
+
+ let get_local_ref x =
+ try LM.find loc x
+ with _ ->
+ (
+ if tracing then trace "unknownsize" "Number of locals so far: %d" (LM.length loc);
+ let rloc = {loc_value = D.bot (); loc_init = D.bot ();
+ called = ref false; aborted = ref false;
+ loc_from = LM.create 10} in
+ LM.add loc x rloc;
+ rloc)
+
+ let init_local (x, d) =
+ LM.add loc x {
+ loc_value = d;
+ loc_init = d;
+ called = ref false;
+ aborted = ref false;
+ loc_from = LM.create 10
+ }
+
+ let get_local_value init from = LM.fold (fun _ (b,_,_,_) a -> D.join a b) from init
+
+ let get_old_local_value x from =
+ try LM.find from x
+ with _ -> let (delay,gas) = !gas_default in
+ LM.add from x (D.bot (),delay,gas,false);
+ (D.bot (),delay,gas,false)
+
+ (*
+ Now the main solving consisting of the mutual recursive functions
+ set_globals, set_locals, and iterate
+*)
+
+ let rec set_global x g d =
+ let sx = source x
+(*
+ replaces old contribution with the new one;
+ reconstructs value of g from contributions;
+ propagates infl and updates value - if value has changed
+*)
+ in
+ (* if tracing then trace "set_global" "set_global: \n From: %a \nOn:%a \n Value: %a" System.LVar.pretty_trace x System.GVar.pretty_trace g G.pretty d; *)
+ let {value;init;infl;last;from} = get_global_ref g in
+ let (old_xg,delay,gas,narrow,set) = get_old_global_value sx from in
+ let () = LM.add last x d in
+ let set = LS.add x set in
+ let d_new = get_last_contrib sx set last in
+ let (new_xg,delay,gas,narrow) = gwarrow (old_xg,delay,gas,narrow) d_new in
+ let () = OM.replace from sx (new_xg,delay,gas,narrow,set) in
+ if G.equal new_xg old_xg then (
+ if tracing then trace "set_globalc" "no change!";
+ )
+ else
+ begin
+ if tracing then trace "set_globalc" "new contribution registered!";
+ let new_g = get_global_value init from in
+ if G.equal value new_g then
+ ()
+ else
+ let () = GM.replace glob g {value = new_g; init = init; infl = LS.empty;last;from} in
+ let work = infl in
+ let _ = GM.replace glob g {value = new_g; init = init; infl = LS.empty; last; from} in
+ let doit x =
+ let r = get_local_ref x in
+ if !(r.called) then r.aborted := true
+ else (
+ if tracing then trace "iter" "set_global caused iter\n By: %a\nLocal:%a" System.GVar.pretty_trace g System.LVar.pretty_trace x;
+ iterate x
+ )
+ in
+(*
+ if tracing then trace "iter" "Size of work: %d" (LS.seq_of work |> Seq.length);
+*)
+ LS.iter doit work
+ end
+
+ and set_local x y d =
+ (*
+ Contribution from x to y with d
+ replaces old contribution with the new one;
+ reconstructs value of y from contributions;
+ propagates infl together with y and updates value - if value has changed
+ *)
+ if tracing then trace "set_local" "set_local %a from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ if tracing then trace "set_local" "value: %a" D.pretty d;
+ let {loc_value;loc_init;called;aborted;loc_from} as y_record = get_local_ref y in
+ let (old_xy,delay,gas,narrow) = get_old_local_value x loc_from in
+ let (new_xy,delay,gas,narrow) =
+ if !called then lwarrow (old_xy,delay,gas,narrow) d
+ else (d,delay,gas,narrow) in
+ if D.equal new_xy old_xy then (
+ (* If value of x has not changed, nothing to do *)
+ if tracing then trace "set_localc" "no change";
+ )
+ else (
+ if tracing then trace "set_localc" "new contribution";
+ LM.replace loc_from x (new_xy,delay,gas,narrow);
+ let new_y = get_local_value loc_init loc_from in
+ if tracing then trace "set_local" "new value for %a is %a" System.LVar.pretty_trace y D.pretty new_y;
+ if D.equal loc_value new_y then (
+ if tracing then trace "set_local" "no change in local %a after updating from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ )
+ else (
+ let y_record = {y_record with loc_value = new_y} in
+ LM.replace loc y y_record;
+ if !called then (
+ aborted := true;
+ if tracing then trace "set_local" "aborting local %a update from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ )
+ else (
+ if tracing then trace "set_local" "starting iteration on %a" System.LVar.pretty_trace y;
+ if tracing then trace "iter" "set_local caused iter";
+ iterate y
+ )
+ )
+ )
+
+(*
+ wrapper around propagation function to collect multiple contributions to same unknowns;
+ contributions are delayed until the very end
+*)
+
+ and wrap (x,f) d =
+ let sigma = LM.create 10 in
+ let tau = GM.create 10 in
+ let add_sigma x d =
+ let d = try D.join d (LM.find sigma x) with _ -> d in
+ LM.replace sigma x d in
+ let add_tau g d =
+ let d = try G.join d (GM.find tau g) with _ -> d in
+ GM.replace tau g d in
+ let _ = f d (fun _ -> raise (Failure "Locals queried in rhs??"))
+ add_sigma (get_global x) add_tau in
+ let _ = GM.iter (set_global x) tau in
+ let _ = LM.iter (set_local x) sigma in
+ ()
+
+(*
+ now the actual propagation!
+*)
+
+ and iterate x =
+ (* if tracing then trace "iter" "iterate %a" System.LVar.pretty_trace x; *)
+ let rloc = get_local_ref x in
+ (* if tracing then trace "iter" "current value: %a" D.pretty rloc.loc_value; *)
+ match System.system x with
+ | None -> ()
+ | Some f ->
+ let _ = rloc.called := true in
+ let _ = rloc.aborted := false in
+ let _ = wrap (x,f) rloc.loc_value in
+ let _ = rloc.called := false in
+ if !(rloc.aborted) then (
+ if tracing then trace "iter" "re-iter";
+ iterate x;
+ )
+ else (
+ (* if tracing then trace "iter" "done iterating"; *)
+ )
+
+ (* ... now the main solver loop ... *)
+
+ let solve localinit globalinit xs =
+ if tracing then trace "solver" "Starting bottom-up fixpoint iteration";
+ List.iter init_local localinit;
+ List.iter init_global globalinit;
+ let toplevel_iterate x =
+ if tracing then trace "iter" "Toplevel iterate on %a" System.LVar.pretty_trace x;
+ iterate x in
+ List.iter toplevel_iterate xs;
+ let sigma = LM.to_seq loc |> Seq.map (fun (k,l) -> (k,l.loc_value)) in
+ let tau = GM.to_seq glob |> Seq.map (fun (k,l) -> (k,l.value)) in
+ (sigma,tau)
+
+ (* ... now the checker! *)
+
+ let check localinit globalinit xs =
+
+ let sigma_out = LM.create 100 in
+ let tau_out = GM.create 100 in
+
+ let get_local x = try (LM.find loc x).loc_value with _ -> D.bot () in
+
+ let check_local x d = if D.leq d (D.bot ()) then ()
+ else let {loc_value:D.t;loc_init;called;aborted;loc_from} = get_local_ref x in
+ if D.leq d loc_value then
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x
+ )
+ else (
+ Logs.error "Fixpoint not reached for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false;
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x
+ )
+ ) in
+
+ let get_global g = try (GM.find glob g).value with _ -> G.bot () in
+
+ let check_global x g d =
+ if G.leq d (G.bot ()) then
+ ()
+ else if System.GVar.is_write_only g then
+ GM.replace tau_out g (G.join (GM.find_opt tau_out g |> BatOption.default (G.bot ())) d)
+ else
+ let {value;infl;_} = get_global_ref g in
+ if G.leq d value then
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ else (
+ Logs.error "Fixpoint not reached for global %a\n Side from %a is %a \n Solver Computed %a\n Diff is %a" System.GVar.pretty_trace g System.LVar.pretty_trace x G.pretty d G.pretty value G.pretty_diff (d,value);
+ AnalysisState.verified := Some false;
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ ) in
+
+ let rec doit () =
+ match rem_work () with
+ | None -> (LM.to_seq sigma_out, GM.to_seq tau_out)
+ | Some x -> (match System.system x with
+ | None -> doit ()
+ | Some f -> (
+ f (get_local x)
+ get_local check_local
+ get_global (check_global x);
+ doit ()
+ )
+ ) in
+
+ List.iter (fun (x,_) -> let value = get_local x in LM.add sigma_out x value) localinit;
+ List.iter (fun (g, _) -> let value = get_global g in GM.add tau_out g value) globalinit;
+ List.iter add_work xs;
+ doit ()
+
+ let check localinit globalinit xs =
+ let check_local (x,d) =
+ if D.leq d (get_local_ref x).loc_value then ()
+ else (
+ Logs.error "initialization not subsumed for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false)
+ in
+ let check_global (g,d) =
+ if G.leq d (get_global_ref g).value then ()
+ else (
+ Logs.error "initialization not subsumed for global %a" System.GVar.pretty_trace g;
+ AnalysisState.verified := Some false;
+ ) in
+
+ let _ = List.iter check_local localinit in
+ let _ = List.iter check_global globalinit in
+
+ check localinit globalinit xs
+end
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 7deeb60058..1630e5b587 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1,5 +1,5 @@
(** Construction of a {{!Goblint_constraint} constraint system} from an {{!Analyses.Spec} analysis specification} and {{!MyCFG.CfgBackward} CFGs}.
- Transformatons of analysis specifications as functors. *)
+ Transformations of analysis specifications as functors. *)
open Batteries
open GoblintCil
diff --git a/src/framework/fwdConstraints.ml b/src/framework/fwdConstraints.ml
new file mode 100644
index 0000000000..60d45c0e03
--- /dev/null
+++ b/src/framework/fwdConstraints.ml
@@ -0,0 +1,408 @@
+(** Construction of a {{!Goblint_constraint} constraint system} from an {{!Analyses.Spec} analysis specification} and
+ {{!MyCFG.CfgForward} CFGs}.
+ Transformations of analysis specifications as functors. *)
+
+open Batteries
+open GoblintCil
+open MyCFG
+open Analyses
+open Goblint_constraint.ConstrSys
+open GobConfig
+
+
+module type Increment =
+sig
+ val increment: increment_data option
+end
+
+
+(** The main point of this file---generating a [FwdGlobConstrSys] from a [Spec]. *)
+module FromSpec (S:Spec) (Cfg:CfgForward) (I: Increment)
+ : sig
+ include FwdGlobConstrSys with module LVar = VarF (S.C)
+ and module GVar = GVarFCNW (S.V)(S.C)
+ and module D = S.D
+ and module G = GVarL (S.G) (S.D)
+ end
+=
+struct
+ type lv = MyCFG.node * S.C.t
+ (* type gv = varinfo *)
+ type ld = S.D.t
+ (* type gd = S.G.t *)
+ module LVar = VarF (S.C)
+ module GVar = GVarFCNW (S.V)(S.C)
+ module D = S.D
+ module G = GVarL (S.G) (S.D)
+
+ (* Two global invariants:
+ 1. S.V -> S.G -- used for Spec
+ 2. fundec -> set of S.C -- used for IterSysVars Node *)
+
+ let sync man =
+ match man.prev_node with
+ | FunctionEntry f -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *)
+ S.sync man (`JoinCall f)
+ | _ -> S.sync man `Join
+
+ let common_man' var edge target_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
+ let r = ref [] in
+ let spawns = ref [] in
+ (* now watch this ... *)
+ let rec man =
+ { ask = (fun (type a) (q: a Queries.t) -> S.query man q)
+ ; emit = (fun _ -> failwith "emit outside MCP")
+ ; node = target_node
+ ; prev_node = fst var
+ ; control_context = (fun () -> snd var |> Obj.obj)
+ ; context = (fun () -> snd var |> Obj.obj)
+ ; edge = edge
+ ; local = pval
+ ; global = (fun g -> G.spec (getg (GVar.spec g)))
+ ; spawn = spawn
+ ; split = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r)
+ ; sideg = (fun g d -> sideg (GVar.spec g) (G.create_spec d))
+ }
+ and spawn ?(multiple=false) lval f args =
+ (* TODO: adjust man node/edge? *)
+ (* TODO: don't repeat for all paths that spawn same *)
+ let ds = S.threadenter ~multiple man lval f args in
+ List.iter (fun d ->
+ spawns := (lval, f, args, d, multiple) :: !spawns;
+ match Cilfacade.find_varinfo_fundec f with
+ | fd ->
+ let c = S.context man fd d in
+ sidel (FunctionEntry fd, c) d
+ | exception Not_found ->
+ (* unknown function *)
+ M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
+ (* actual implementation (e.g. invalidation) is done by threadenter *)
+ (* must still sync for side effects, e.g., old sync-based none privatization soundness in 02-base/51-spawn-special *)
+ let rec sync_man =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_man q);
+ local = d;
+ prev_node = Function dummyFunDec;
+ }
+ in
+ (* TODO: more accurate man? *)
+ ignore (sync sync_man)
+ ) ds
+ in
+ (* ... nice, right! *)
+ let pval = sync man in
+ { man with local = pval }, r, spawns
+
+ let rec bigsqcup = function
+ | [] -> D.bot ()
+ | [x] -> x
+ | x::xs -> D.join x (bigsqcup xs)
+
+ let thread_spawns man d spawns =
+ if List.is_empty spawns then
+ d
+ else
+ let rec man' =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query man' q)
+ ; local = d
+ }
+ in
+ (* TODO: don't forget path dependencies *)
+ let one_spawn (lval, f, args, fd, multiple) =
+ let rec fman =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query fman q)
+ ; local = fd
+ }
+ in
+ S.threadspawn man' ~multiple lval f args fman
+ in
+ bigsqcup (List.map one_spawn spawns)
+
+ let common_join man d splits spawns =
+ thread_spawns man (bigsqcup (d :: splits)) spawns
+
+ let common_joins man ds splits spawns = common_join man (bigsqcup ds) splits spawns
+
+ let tf_assign var edge target_node lv e getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.assign man lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let tf_vdecl var edge target_node v getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.vdecl man v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let normal_return r fd man sideg =
+ let spawning_return = S.return man r fd in
+ let nval = S.sync { man with local = spawning_return } `Return in
+ nval
+
+ let toplevel_kernel_return r fd man sideg =
+ let st = if fd.svar.vname = MyCFG.dummy_func.svar.vname then man.local else S.return man r fd in
+ let spawning_return = S.return {man with local = st} None MyCFG.dummy_func in
+ let nval = S.sync { man with local = spawning_return } `Return in
+ nval
+
+ let tf_ret var edge target_node ret fd getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ if (CilType.Fundec.equal fd MyCFG.dummy_func ||
+ List.mem fd.svar.vname (get_string_list "mainfun")) &&
+ get_bool "kernel"
+ then toplevel_kernel_return ret fd man sideg
+ else normal_return ret fd man sideg
+ in
+ common_join man d !r !spawns
+
+ let tf_entry var edge target_node fd getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.body man fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let tf_test var edge target_node e tv getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.branch man e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let tf_normal_call man lv e (f:fundec) args getl sidel getg sideg =
+ let combine (cd, fc, fd) =
+ if M.tracing then M.traceli "combine" "local: %a" S.D.pretty cd;
+ if M.tracing then M.trace "combine" "function: %a" S.D.pretty fd;
+ let rec cd_man =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query cd_man q);
+ local = cd;
+ }
+ in
+ let fd_man =
+ (* Inner scope to prevent unsynced fd_man from being used. *)
+ (* Extra sync in case function has multiple returns.
+ Each `Return sync is done before joining, so joined value may be unsound.
+ Since sync is normally done before tf (in common_man), simulate it here for fd. *)
+ (* TODO: don't do this extra sync here *)
+ let rec sync_man =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_man q);
+ local = fd;
+ prev_node = Function f;
+ }
+ in
+ (* TODO: more accurate man? *)
+ let synced = sync sync_man in
+ let rec fd_man =
+ { sync_man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query fd_man q);
+ local = synced;
+ }
+ in
+ fd_man
+ in
+ let r = List.fold_left (fun acc fd1 ->
+ let rec fd1_man =
+ { fd_man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query fd1_man q);
+ local = fd1;
+ }
+ in
+ let combine_enved = S.combine_env cd_man lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man) in
+ let rec combine_assign_man =
+ { cd_man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query combine_assign_man q);
+ local = combine_enved;
+ }
+ in
+ S.D.join acc (S.combine_assign combine_assign_man lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man))
+ ) (S.D.bot ()) (S.paths_as_set fd_man)
+ in
+ if M.tracing then M.traceu "combine" "combined local: %a" S.D.pretty r;
+ r
+ in
+ let paths = S.enter man lv f args in
+ let paths = List.map (fun (c,v) -> (c, S.context man f v, v)) paths in
+ List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) paths;
+ let paths = List.map (fun (c,fc,v) ->
+ let endvar = (GVar.return (f,fc)) in
+ (c, fc, if S.D.is_bot v then v else G.return @@ getg endvar)) paths in
+ (* Don't filter bot paths, otherwise LongjmpLifter is not called. *)
+ (* let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in *)
+ let paths = List.map (Tuple3.map2 Option.some) paths in
+ if M.tracing then M.traceli "combine" "combining";
+ let paths = List.map combine paths in
+ let r = List.fold_left D.join (D.bot ()) paths in
+ if M.tracing then M.traceu "combine" "combined: %a" S.D.pretty r;
+ r
+
+
+ let rec tf_proc var edge target_node lv e args getl sidel getg sideg d =
+ let tf_special_call man f =
+ let once once_control init_routine =
+ (* Executes leave event for new local state d if it is not bottom *)
+ let leave_once d =
+ if not (S.D.is_bot d) then
+ let rec man' =
+ { man with
+ ask = (fun (type a) (q: a Queries.t) -> S.query man' q);
+ local = d;
+ }
+ in
+ S.event man' (Events.LeaveOnce { once_control }) man'
+ else
+ S.D.bot ()
+ in
+ let first_call =
+ let d' = S.event man (Events.EnterOnce { once_control; ran = false }) man in
+ tf_proc var edge target_node None init_routine [] getl sidel getg sideg d'
+ in
+ let later_call = S.event man (Events.EnterOnce { once_control; ran = true }) man in
+ D.join (leave_once first_call) (leave_once later_call)
+ in
+ let is_once = LibraryFunctions.find ~nowarn:true f in
+ (* If the prototpye for a library function is wrong, this will throw an exception. Such exceptions are usually unrelated to pthread_once, it is just that the call to `is_once.special` raises here *)
+ match is_once.special args with
+ | Once { once_control; init_routine } -> once once_control init_routine
+ | _ -> S.special man lv f args
+ in
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let functions =
+ match e with
+ | Lval (Var v, NoOffset) ->
+ (* Handle statically known function call directly.
+ Allows deactivating base. *)
+ [v]
+ | _ ->
+ (* Depends on base for query. *)
+ let ad = man.ask (Queries.EvalFunvar e) in
+ Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
+ in
+ let one_function f =
+ match Cil.unrollType f.vtype with
+ | TFun (_, params, var_arg, _) ->
+ let arg_length = List.length args in
+ let p_length = Option.map_default List.length 0 params in
+ (* Check whether number of arguments fits. *)
+ (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *)
+ if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then
+ let d =
+ (match Cilfacade.find_varinfo_fundec f with
+ | fd when LibraryFunctions.use_special f.vname ->
+ M.info ~category:Analyzer "Using special for defined function %s" f.vname;
+ tf_special_call man f
+ | fd ->
+ tf_normal_call man lv e fd args getl sidel getg sideg
+ | exception Not_found ->
+ tf_special_call man f)
+ in
+ Some d
+ else begin
+ let geq = if var_arg then ">=" else "" in
+ M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
+ None
+ end
+ | _ ->
+ M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
+ None
+ in
+ let funs = List.filter_map one_function functions in
+ if [] = funs && not (S.D.is_bot man.local) then begin
+ M.msg_final Warning ~category:Unsound ~tags:[Category Call] "No suitable function to call";
+ M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
+ d (* because LevelSliceLifter *)
+ end else
+ common_joins man funs !r !spawns
+
+ let tf_asm var edge target_node getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.asm man in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let tf_skip var edge target_node getl sidel getg sideg d =
+ let man, r, spawns = common_man' var edge target_node d getl sidel getg sideg in
+ let d = S.skip man in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+ common_join man d !r !spawns
+
+ let tf ((n,c) as var) getl sidel getg sideg target_node edge d =
+ begin match edge with
+ | Assign (lv,rv) ->
+ let r = tf_assign var edge target_node lv rv getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | VDecl (v) ->
+ let r = tf_vdecl var edge target_node v getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | Proc (r,f,ars) ->
+ let r = tf_proc var edge target_node r f ars getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | Entry f ->
+ let r = tf_entry var edge target_node f getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | Ret (r,fd) ->
+ let r = tf_ret var edge target_node r fd getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r;
+ sideg (GVar.return (fd,Obj.obj c)) (G.create_return r)
+ | Test (p,b) ->
+ let r = tf_test var edge target_node p b getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | ASM (_, _, _) ->
+ let r = tf_asm var edge target_node getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ | Skip ->
+ let r = tf_skip var edge target_node getl sidel getg sideg d in
+ sidel (target_node, Obj.obj c) r
+ end
+
+ type Goblint_backtrace.mark += TfLocation of location
+
+ let () = Goblint_backtrace.register_mark_printer (function
+ | TfLocation loc ->
+ Some ("transfer function at " ^ CilType.Location.show loc)
+ | _ -> None (* for other marks *)
+ )
+
+ let tf var getl sidel getg sideg target_node (_,edge) d (f,t):unit =
+ let old_loc = !Goblint_tracing.current_loc in
+ let old_loc2 = !Goblint_tracing.next_loc in
+ Goblint_tracing.current_loc := f;
+ Goblint_tracing.next_loc := t;
+ Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () ->
+ Goblint_tracing.current_loc := old_loc;
+ Goblint_tracing.next_loc := old_loc2
+ ) (fun () ->
+ tf var getl sidel getg sideg target_node edge d
+ )
+
+ let tf_fwd value (v,c) (edges, u) getl sidel getg sideg:unit =
+ let pval = value in
+ let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in
+ let es = List.map (tf (v,Obj.repr c) getl sidel getg sideg u) edges in
+ List.iter2 (fun e l -> e pval l) es locs
+
+ let tf value (v,c) (e,u) getl sidel getg sideg =
+ let old_node = !current_node in
+ let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
+ let new_fd = Node.find_fundec v in
+ if not (CilType.Fundec.equal old_fd new_fd) then
+ Timing.Program.enter new_fd.svar.vname;
+ let old_context = !M.current_context in
+ current_node := Some v;
+ M.current_context := Some (Obj.magic c); (* magic is fine because Spec is top-level Control Spec *)
+ Fun.protect ~finally:(fun () ->
+ current_node := old_node;
+ M.current_context := old_context;
+ if not (CilType.Fundec.equal old_fd new_fd) then
+ Timing.Program.exit new_fd.svar.vname
+ ) (fun () ->
+ tf_fwd value (v,c) (e,u) getl sidel getg sideg
+ )
+
+ let system (v,c) =
+ let tf value getl sidel getg sideg =
+ let tf' eu = tf value (v,c) eu getl sidel getg sideg in
+ let xs = Cfg.next v in
+ List.iter (fun eu -> tf' eu) xs
+ in
+ Some tf
+
+
+end
diff --git a/src/framework/fwdControl.ml b/src/framework/fwdControl.ml
new file mode 100644
index 0000000000..3a81a06f46
--- /dev/null
+++ b/src/framework/fwdControl.ml
@@ -0,0 +1,635 @@
+(** Main internal functionality: analysis of the program by abstract interpretation via constraint solving. *)
+
+(** An analyzer that takes the CFG from [MyCFG], a solver from [Selector], constraints from [Constraints] (using the specification from [MCP]) *)
+
+open Batteries
+open GoblintCil
+open MyCFG
+open Analyses
+open Goblint_constraint.ConstrSys
+open Goblint_constraint.Translators
+open Goblint_constraint.SolverTypes
+open GobConfig
+open Constraints
+open SpecLifters
+
+module type S2S = Spec2Spec
+
+(* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
+let spec_module: (module Spec) Lazy.t = lazy (
+ GobConfig.building_spec := true;
+ let arg_enabled = get_bool "exp.arg.enabled" in
+ let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
+ (* apply functor F on module X if opt is true *)
+ let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
+ let module S1 =
+ (val
+ (module MCP.MCP2 : Spec)
+ |> lift (get_int "ana.context.gas_value" >= 0) (ContextGasLifter.get_gas_lifter ())
+ |> lift true (module WidenContextLifterSide) (* option checked in functor *)
+ |> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter)
+ (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
+ |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
+ |> lift (get_bool "ana.opt.hashcached") (module HashCachedContextLifter)
+ |> lift arg_enabled (module HashconsLifter)
+ |> lift arg_enabled (module ArgConstraints.PathSensitive3)
+ |> lift (not arg_enabled) (module PathSensitive2)
+ |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
+ |> lift true (module DeadCodeLifter)
+ |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
+ |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
+ |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
+ (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
+ Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
+ |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)
+ |> lift true (module LongjmpLifter.Lifter)
+ |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
+ |> lift (get_int "ana.widen.delay.global" > 0) (module WideningDelay.GLifter)
+ )
+ in
+ GobConfig.building_spec := false;
+ ControlSpecC.control_spec_c := (module S1.C);
+ (module S1)
+)
+
+(** gets Spec for current options *)
+let get_spec (): (module Spec) =
+ Lazy.force spec_module
+
+let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ -> None)
+
+let current_varquery_global_state_json: (Goblint_constraint.VarQuery.t option -> Yojson.Safe.t) ref = ref (fun _ -> `Null)
+
+(** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
+module AnalyzeCFG (Cfg:CfgBidirSkip) (Spec:Spec) (Inc:Increment) =
+struct
+
+ module SpecSys =
+ struct
+ (* Must be created in module, because cannot be wrapped in a module later. *)
+ module Spec = Spec
+
+ (* The Equation system *)
+ module EQSys = FwdConstraints.FromSpec (Spec) (Cfg) (Inc)
+
+ (* Hashtbl for locals *)
+ module LHT = BatHashtbl.Make (EQSys.LVar)
+ (* Hashtbl for globals *)
+ module GHT = BatHashtbl.Make (EQSys.GVar)
+ end
+
+ open SpecSys
+
+ (* The solver *)
+ module PostSolverArg =
+ struct
+ let should_prune = true
+ let should_verify = get_bool "verify"
+ let should_warn = get_string "warn_at" <> "never"
+ let should_save_run =
+ (* copied from solve_and_postprocess *)
+ let gobview = get_bool "gobview" in
+ let save_run = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
+ save_run <> ""
+ end
+
+ module Sys = FwdConstraints.FromSpec (Spec) (Cfg) (Inc)
+ module FwdSlvr = FwdSolver.FwdSolver (Sys)
+ module BuSolver = Bu.FwdBuSolver (Sys)
+ module WBuSolver = Wbu.FwdWBuSolver (Sys)
+ (* module Slvr2 = BuSlvr *)
+ module GHT = BatHashtbl.Make (Sys.GVar)
+
+
+ (* Triple of the function, context, and the local value. *)
+ module RT = AnalysisResult.ResultType2 (Spec)
+ (* Set of triples [RT] *)
+ module LT = SetDomain.HeadlessSet (RT)
+ (* Analysis result structure---a hashtable from program points to [LT] *)
+ module Result = AnalysisResult.Result (LT) (struct let result_name = "analysis" end)
+
+
+ (* print out information about dead code *)
+ let print_dead_code (xs:Result.t) uncalled_fn_loc =
+ let module NH = Hashtbl.Make (Node) in
+ let live_nodes : unit NH.t = NH.create 10 in
+ let count = ref 0 in (* Is only populated if "ana.dead-code.lines" or "ana.dead-code.branches" is true *)
+ let module StringMap = BatMap.Make (String) in
+ let live_lines = ref StringMap.empty in
+ let dead_lines = ref StringMap.empty in
+ let module FunSet = Hashtbl.Make (CilType.Fundec) in
+ let live_funs: unit FunSet.t = FunSet.create 13 in
+ let add_one n v =
+ match n with
+ | Statement s when Cilfacade.(StmtH.mem pseudo_return_to_fun s) ->
+ (* Exclude pseudo returns from dead lines counting. No user code at "}". *)
+ ()
+ | _ ->
+ (* Not using Node.location here to have updated locations in incremental analysis.
+ See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
+ let l = UpdateCil.getLoc n in
+ let f = Node.find_fundec n in
+ FunSet.replace live_funs f ();
+ let add_fun = BatISet.add l.line in
+ let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in
+ let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in
+ if is_dead then (
+ dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines
+ ) else (
+ live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines;
+ NH.add live_nodes n ()
+ );
+ in
+ Result.iter add_one xs;
+ let live_count = StringMap.fold (fun _ file_lines acc ->
+ StringMap.fold (fun _ fun_lines acc ->
+ acc + ISet.cardinal fun_lines
+ ) file_lines acc
+ ) !live_lines 0
+ in
+ let live file fn =
+ try StringMap.find fn (StringMap.find file !live_lines)
+ with Not_found -> BatISet.empty
+ in
+ if List.mem "termination" @@ get_string_list "ana.activated" then (
+ (* check if we have upjumping gotos *)
+ let open Cilfacade in
+ let warn_for_upjumps fundec gotos =
+ if FunSet.mem live_funs fundec then (
+ (* set nortermiantion flag *)
+ AnalysisState.svcomp_may_not_terminate := true;
+ (* iterate through locations to produce warnings *)
+ LocSet.iter (fun l _ ->
+ M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)"
+ ) gotos
+ )
+ in
+ FunLocH.iter warn_for_upjumps funs_with_upjumping_gotos
+ );
+ dead_lines := StringMap.mapi (fun fi -> StringMap.mapi (fun fu ded -> BatISet.diff ded (live fi fu))) !dead_lines;
+ dead_lines := StringMap.map (StringMap.filter (fun _ x -> not (BatISet.is_empty x))) !dead_lines;
+ dead_lines := StringMap.filter (fun _ x -> not (StringMap.is_empty x)) !dead_lines;
+ let warn_func file f xs =
+ let warn_range b e =
+ count := !count + (e - b + 1); (* for total count below *)
+ let doc =
+ if b = e then
+ Pretty.dprintf "on line %d" b
+ else
+ Pretty.dprintf "on lines %d..%d" b e
+ in
+ let loc: Cil.location = {
+ file;
+ line = b;
+ column = -1; (* not shown *)
+ byte = 0; (* wrong, but not shown *)
+ endLine = e;
+ endColumn = -1; (* not shown *)
+ endByte = 0; (* wrong, but not shown *)
+ synthetic = false;
+ }
+ in
+ (doc, Some (Messages.Location.CilLocation loc)) (* CilLocation is fine because always printed from scratch *)
+ in
+ let msgs =
+ BatISet.fold_range (fun b e acc ->
+ warn_range b e :: acc
+ ) xs []
+ in
+ let msgs = List.rev msgs in (* lines in ascending order *)
+ M.msg_group Warning ~category:Deadcode "Function '%s' has dead code" f msgs (* TODO: function location for group *)
+ in
+ let warn_file f = StringMap.iter (warn_func f) in
+ if get_bool "ana.dead-code.lines" then (
+ StringMap.iter warn_file !dead_lines; (* populates count by side-effect *)
+ let severity: M.Severity.t = if StringMap.is_empty !dead_lines then Info else Warning in
+ let dead_total = !count + uncalled_fn_loc in
+ let total = live_count + dead_total in (* We can only give total LoC if we counted dead code *)
+ M.msg_group severity ~category:Deadcode "Logical lines of code (LLoC) summary" [
+ (Pretty.dprintf "live: %d" live_count, None);
+ (Pretty.dprintf "dead: %d%s" dead_total (if uncalled_fn_loc > 0 then Printf.sprintf " (%d in uncalled functions)" uncalled_fn_loc else ""), None);
+ (Pretty.dprintf "total lines: %d" total, None);
+ ]
+ );
+ NH.mem live_nodes
+
+ (* convert result that can be out-put *)
+ let solver2source_result h : Result.t =
+ (* processed result *)
+ let res = Result.create 113 in
+
+ (* Adding the state at each system variable to the final result *)
+ let add_local_var (n,es) state =
+ (* Not using Node.location here to have updated locations in incremental analysis.
+ See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
+ let loc = UpdateCil.getLoc n in
+ if loc <> locUnknown then try
+ let fundec = Node.find_fundec n in
+ if Result.mem res n then
+ (* If this source location has been added before, we look it up
+ * and add another node to it information to it. *)
+ let prev = Result.find res n in
+ Result.replace res n (LT.add (es,state,fundec) prev)
+ else
+ Result.add res n (LT.singleton (es,state,fundec))
+ (* If the function is not defined, and yet has been included to the
+ * analysis result, we generate a warning. *)
+ with Not_found ->
+ Messages.debug ~category:Analyzer ~loc:(CilLocation loc) "Calculated state for undefined function: unexpected node %a" Node.pretty_trace n
+ in
+ LHT.iter add_local_var h;
+ res
+
+ (** The main function to preform the selected analyses. *)
+ let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) =
+ let module FileCfg: FileCfg =
+ struct
+ let file = file
+ module Cfg = Cfg
+ end
+ in
+
+ AnalysisState.should_warn := false; (* reset for server mode *)
+
+ (* exctract global xml from result *)
+ let make_global_fast_xml f g =
+ let open Printf in
+ let print_globals k v =
+ fprintf f "\n%s%a" (XmlUtil.escape (EQSys.GVar.show k)) EQSys.G.printXml v;
+ in
+ GHT.iter print_globals g
+ in
+
+ (* add extern variables to local state *)
+ let do_extern_inits man (file : file) : Spec.D.t =
+ let module VS = Set.Make (Basetype.Variables) in
+ let add_glob s = function
+ GVar (v,_,_) -> VS.add v s
+ | _ -> s
+ in
+ let vars = foldGlobals file add_glob VS.empty in
+ let set_bad v st =
+ Spec.assign {man with local = st} (var v) MyCFG.unknown_exp
+ in
+ let is_std = function
+ | {vname = ("__tzname" | "__daylight" | "__timezone"); _} (* unix time.h *)
+ | {vname = ("tzname" | "daylight" | "timezone"); _} (* unix time.h *)
+ | {vname = "getdate_err"; _} (* unix time.h, but somehow always in MacOS even without include *)
+ | {vname = ("stdin" | "stdout" | "stderr"); _} (* standard stdio.h *)
+ | {vname = ("optarg" | "optind" | "opterr" | "optopt" ); _} (* unix unistd.h *)
+ | {vname = ("__environ"); _} -> (* Linux Standard Base Core Specification *)
+ true
+ | _ -> false
+ in
+ let add_externs s = function
+ | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) && not (get_bool "exp.hide-std-globals" && is_std v) -> set_bad v s
+ | _ -> s
+ in
+ foldGlobals file add_externs (Spec.startstate MyCFG.dummy_func.svar)
+ in
+
+ (* Simulate globals before analysis. *)
+ (* TODO: make extern/global inits part of constraint system so all of this would be unnecessary. *)
+ let gh = GHT.create 13 in
+ let getg v = GHT.find_default gh v (EQSys.G.bot ()) in
+ let sideg v d =
+ if M.tracing then M.trace "global_inits" "sideg %a = %a" EQSys.GVar.pretty v EQSys.G.pretty d;
+ GHT.replace gh v (EQSys.G.join (getg v) d)
+ in
+ (* Old-style global function for context.
+ * This indirectly prevents global initializers from depending on each others' global side effects, which would require proper solving. *)
+ let getg v = EQSys.G.bot () in
+
+ (* analyze cil's global-inits function to get a starting state *)
+ let do_global_inits (file: file) : Spec.D.t * fundec list =
+ let man =
+ { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+ ; emit = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
+ ; node = MyCFG.dummy_node
+ ; prev_node = MyCFG.dummy_node
+ ; control_context = (fun () -> man_failwith "Global initializers have no context.")
+ ; context = (fun () -> man_failwith "Global initializers have no context.")
+ ; edge = MyCFG.Skip
+ ; local = Spec.D.top ()
+ ; global = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
+ ; spawn = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+ ; split = (fun _ -> failwith "Global initializers trying to split paths.")
+ ; sideg = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
+ }
+ in
+ let edges = CfgTools.getGlobalInits file in
+ Logs.debug "Executing %d assigns." (List.length edges);
+ let funs = ref [] in
+ (*let count = ref 0 in*)
+ let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t =
+ if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pretty loc;
+ (*incr count;
+ if (get_bool "dbg.verbose")&& (!count mod 1000 = 0) then Printf.printf "%d %!" !count; *)
+ Goblint_tracing.current_loc := loc;
+ match edge with
+ | MyCFG.Entry func ->
+ if M.tracing then M.trace "global_inits" "Entry %a" d_lval (var func.svar);
+ Spec.body {man with local = st} func
+ | MyCFG.Assign (lval,exp) ->
+ if M.tracing then M.trace "global_inits" "Assign %a = %a" d_lval lval d_exp exp;
+ begin match lval, exp with
+ | (Var v,o), (AddrOf (Var f,NoOffset))
+ when v.vstorage <> Static && isFunctionType f.vtype ->
+ (try funs := Cilfacade.find_varinfo_fundec f :: !funs with Not_found -> ())
+ | _ -> ()
+ end;
+ let res = Spec.assign {man with local = st} lval exp in
+ (* Needed for privatizations (e.g. None) that do not side immediately *)
+ let res' = Spec.sync {man with local = res} `Normal in
+ if M.tracing then M.trace "global_inits" "\t\t -> state:%a" Spec.D.pretty res;
+ res'
+ | _ -> failwith "Unsupported global initializer edge"
+ in
+ let with_externs = do_extern_inits man file in
+ (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges); *)
+ let old_loc = !Goblint_tracing.current_loc in
+ let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
+ Goblint_tracing.current_loc := old_loc;
+ if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pretty result;
+ result, !funs
+ in
+
+ let print_globals glob =
+ let out = M.get_out (Spec.name ()) !M.out in
+ let print_one v st =
+ ignore (Pretty.fprintf out "%a -> %a\n" EQSys.GVar.pretty_trace v EQSys.G.pretty st)
+ in
+ GHT.iter print_one glob
+ in
+
+ (* real beginning of the [analyze] function *)
+ if get_bool "ana.sv-comp.enabled" then
+ Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *)
+ YamlWitness.init ();
+
+ AnalysisState.global_initialization := true;
+ GobConfig.earlyglobs := get_bool "exp.earlyglobs";
+ let marshal: Spec.marshal option = None in
+
+ (* Some happen in init, so enable this temporarily (if required by option). *)
+ AnalysisState.should_warn := PostSolverArg.should_warn;
+ Spec.init marshal;
+ Access.init file;
+ AnalysisState.should_warn := false;
+
+ let startstate, more_funs =
+ Logs.debug "Initializing %d globals." (CfgTools.numGlobals file);
+ Timing.wrap "global_inits" do_global_inits file
+ in
+
+ let otherfuns = if get_bool "kernel" then otherfuns @ more_funs else otherfuns in
+
+ let enter_with st fd =
+ let st = st fd.svar in
+ let man =
+ { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+ ; emit = (fun _ -> failwith "Cannot \"emit\" in enter_with context.")
+ ; node = MyCFG.dummy_node
+ ; prev_node = MyCFG.dummy_node
+ ; control_context = (fun () -> man_failwith "enter_with has no control_context.")
+ ; context = Spec.startcontext
+ ; edge = MyCFG.Skip
+ ; local = st
+ ; global = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
+ ; spawn = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+ ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
+ ; sideg = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
+ }
+ in
+ let args = List.map (fun x -> MyCFG.unknown_exp) fd.sformals in
+ let ents = Spec.enter man None fd args in
+ List.map (fun (_,s) -> fd, s) ents
+ in
+
+ (try MyCFG.dummy_func.svar.vdecl <- (List.hd otherfuns).svar.vdecl with Failure _ -> ());
+
+ let startvars =
+ if startfuns = []
+ then [[MyCFG.dummy_func, startstate]]
+ else
+ let morph f = Spec.morphstate f startstate in
+ List.map (enter_with morph) startfuns
+ in
+
+ let exitvars = List.map (enter_with Spec.exitstate) exitfuns in
+ let otherstate st v =
+ let man =
+ { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+ ; emit = (fun _ -> failwith "Cannot \"emit\" in otherstate context.")
+ ; node = MyCFG.dummy_node
+ ; prev_node = MyCFG.dummy_node
+ ; control_context = (fun () -> man_failwith "enter_func has no context.")
+ ; context = (fun () -> man_failwith "enter_func has no context.")
+ ; edge = MyCFG.Skip
+ ; local = st
+ ; global = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
+ ; spawn = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+ ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
+ ; sideg = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
+ }
+ in
+ (* TODO: don't hd *)
+ List.hd (Spec.threadenter man ~multiple:false None v [])
+ (* TODO: do threadspawn to mainfuns? *)
+ in
+ let prestartstate = Spec.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *)
+ let othervars = List.map (enter_with (otherstate prestartstate)) otherfuns in
+ let startvars = List.concat (startvars @ exitvars @ othervars) in
+ if startvars = [] then
+ failwith "BUG: Empty set of start variables; may happen if enter_func of any analysis returns an empty list.";
+
+ AnalysisState.global_initialization := false;
+
+ let man e =
+ { ask = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)
+ ; emit = (fun _ -> failwith "Cannot \"emit\" in enter_with context.")
+ ; node = MyCFG.dummy_node
+ ; prev_node = MyCFG.dummy_node
+ ; control_context = (fun () -> man_failwith "enter_with has no control_context.")
+ ; context = Spec.startcontext
+ ; edge = MyCFG.Skip
+ ; local = e
+ ; global = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
+ ; spawn = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+ ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
+ ; sideg = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
+ }
+ in
+ let startvars' = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (man e) n e)) startvars in
+
+ let entrystates = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (man e) n e), e) startvars in
+ let entrystates_global = GHT.to_list gh in
+
+ let uncalled_dead = ref 0 in
+
+ let solve_and_postprocess () =
+ (* handle save_run/load_run *)
+ let solver_file = "solver.marshalled" in
+ let load_run = get_string "load_run" in
+ let compare_runs = get_string_list "compare_runs" in
+ let gobview = get_bool "gobview" in
+ let save_run_str = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
+ let solve = if (get_string "solver" = "bu") then BuSolver.solve else
+ if (get_string "solver" = "wbu") then WBuSolver.solve else FwdSlvr.solve in
+ let check = if (get_string "solver" = "bu") then BuSolver.check else
+ if (get_string "solver" = "wbu") then WBuSolver.solve else FwdSlvr.check in
+ let _ = solve entrystates entrystates_global startvars' in
+
+ AnalysisState.should_warn := true; (* reset for postsolver *)
+ AnalysisState.postsolving := true;
+ (* postsolver *)
+
+ let rho,tau = check entrystates entrystates_global startvars' in
+ let lh, gh = LHT.of_seq rho, GHT.of_seq tau in
+
+ (* Most warnings happen before during postsolver, but some happen later (e.g. in finalize), so enable this for the rest (if required by option). *)
+ AnalysisState.should_warn := PostSolverArg.should_warn;
+ let insrt k _ s = match k with
+ | (MyCFG.FunctionEntry fn,_) -> Set.Int.add fn.svar.vid s
+ | _ -> s
+ in
+ (* set of ids of called functions *)
+ let calledFuns = LHT.fold insrt lh Set.Int.empty in
+ let is_bad_uncalled fn loc =
+ not (Set.Int.mem fn.vid calledFuns) &&
+ not (Str.last_chars loc.file 2 = ".h") &&
+ not (LibraryFunctions.is_safe_uncalled fn.vname) &&
+ not (Cil.hasAttribute "goblint_stub" fn.vattr)
+ in
+ let print_and_calculate_uncalled = function
+ | GFun (fn, loc) when is_bad_uncalled fn.svar loc->
+ let cnt = Cilfacade.countLoc fn in
+ uncalled_dead := !uncalled_dead + cnt;
+ if get_bool "ana.dead-code.functions" then
+ M.warn ~loc:(CilLocation loc) ~category:Deadcode "Function '%a' is uncalled: %d LLoC" CilType.Fundec.pretty fn cnt (* CilLocation is fine because always printed from scratch *)
+ | _ -> ()
+ in
+ List.iter print_and_calculate_uncalled file.globals;
+
+ (* check for dead code at the last state: *)
+ let main_sol = try LHT.find lh (List.hd startvars') with Not_found -> Spec.D.bot () in
+ if Spec.D.is_bot main_sol then
+ M.warn_noloc ~category:Deadcode "Function 'main' does not return";
+
+ if get_bool "dump_globs" then
+ print_globals gh;
+
+ lh, gh
+ in
+
+ (* Use "normal" constraint solving *)
+ let timeout_reached () =
+ M.error "Timeout reached!";
+ (* let module S = Generic.SolverStats (EQSys) (LHT) in *)
+ (* Can't call Generic.SolverStats...print_stats :(
+ print_stats is triggered by dbg.solver-signal, so we send that signal to ourself in maingoblint before re-raising Timeout.
+ The alternative would be to catch the below Timeout, print_stats and re-raise in each solver (or include it in some functor above them). *)
+ raise Timeout.Timeout
+ in
+ let timeout = get_string "dbg.timeout" |> TimeUtil.seconds_of_duration_string in
+ let lh, gh = Timeout.wrap solve_and_postprocess () (float_of_int timeout) timeout_reached in
+ let module Query = struct
+ let ask_global (gh: EQSys.G.t GHT.t) =
+ (* copied from Control for WarnGlobal *)
+ (* build a man for using the query system *)
+ let rec man =
+ { ask = (fun (type a) (q: a Queries.t) -> Spec.query man q)
+ ; emit = (fun _ -> failwith "Cannot \"emit\" in query context.")
+ ; node = MyCFG.dummy_node (* TODO maybe ask should take a node (which could be used here) instead of a location *)
+ ; prev_node = MyCFG.dummy_node
+ ; control_context = (fun () -> man_failwith "No context in query context.")
+ ; context = (fun () -> man_failwith "No context in query context.")
+ ; edge = MyCFG.Skip
+ ; local = Spec.startstate GoblintCil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *) (* TODO: is this startstate bad? *)
+ ; global = (fun v -> EQSys.G.spec (try GHT.find gh (EQSys.GVar.spec v) with Not_found -> EQSys.G.bot ())) (* TODO: how can be missing? *)
+ ; spawn = (fun ?(multiple=false) v d -> failwith "Cannot \"spawn\" in query context.")
+ ; split = (fun d es -> failwith "Cannot \"split\" in query context.")
+ ; sideg = (fun v g -> failwith "Cannot \"split\" in query context.")
+ }
+ in
+ Spec.query man
+ end
+ in
+
+ let local_xml = solver2source_result lh in
+ current_node_state_json := (fun node -> Option.map LT.to_yojson (Result.find_option local_xml node));
+
+
+ let liveness =
+ if get_bool "ana.dead-code.lines" || get_bool "ana.dead-code.branches" then
+ print_dead_code local_xml !uncalled_dead
+ else
+ fun _ -> true (* TODO: warn about conflicting options *)
+ in
+
+ if get_bool "exp.cfgdot" then
+ CfgTools.dead_code_cfg (module FileCfg) liveness;
+
+
+ let warn_global g v =
+ (* Logs.debug "warn_global %a %a" EQSys.GVar.pretty_trace g EQSys.G.pretty v; *)
+ match g with
+ | `Left g -> (* Spec global *)
+ Query.ask_global gh (WarnGlobal (Obj.repr g))
+ | `Right _ -> (* contexts global *)
+ ()
+ in
+ Timing.wrap "warn_global" (GHT.iter warn_global) gh;
+
+
+ if get_bool "exp.arg.enabled" then ( failwith "no_arg" );
+
+ (* Before SV-COMP, so result can depend on YAML witness validation. *)
+ let yaml_validate_result =
+
+ None
+ in
+
+
+ let marshal = Spec.finalize () in
+ (* copied from solve_and_postprocess *)
+ let gobview = get_bool "gobview" in
+ let save_run = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
+ if save_run <> "" then (
+ Serialize.marshal marshal Fpath.(v save_run / "spec_marshal")
+ );
+ if get_bool "incremental.save" then (
+ Serialize.Cache.(update_data AnalysisData marshal);
+ if not (get_bool "server.enabled") then
+ Serialize.Cache.store_data ()
+ );
+ if get_string "result" <> "none" then Logs.debug "Generating output: %s" (get_string "result");
+
+ Messages.finalize ();
+ Timing.wrap "result output" (Result.output (lazy local_xml) gh make_global_fast_xml) file
+end
+
+(* This function was originally a part of the [AnalyzeCFG] module, but
+ now that [AnalyzeCFG] takes [Spec] as a functor parameter,
+ [analyze_loop] cannot reside in it anymore since each invocation of
+ [get_spec] in the loop might/should return a different module, and we
+ cannot swap the functor parameter from inside [AnalyzeCFG]. *)
+let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info =
+ try
+ let (module Spec) = get_spec () in
+ let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in
+ GobConfig.with_immutable_conf (fun () -> A.analyze file fs)
+ with Refinement.RestartAnalysis ->
+ (* Tail-recursively restart the analysis again, when requested.
+ All solving starts from scratch.
+ Whoever raised the exception should've modified some global state
+ to do a more precise analysis next time. *)
+ (* TODO: do some more incremental refinement and reuse parts of solution *)
+ analyze_loop (module CFG) file fs change_info
+
+(** The main function to perform the selected analyses. *)
+let analyze change_info (file: file) fs =
+ Logs.debug "Generating the control flow graph.";
+ let (module CFG) = CfgTools.compute_cfg file in
+ MyCFG.current_cfg := (module CFG);
+ analyze_loop (module CFG) file fs change_info
diff --git a/src/framework/fwdSolver.ml b/src/framework/fwdSolver.ml
new file mode 100644
index 0000000000..15424db92b
--- /dev/null
+++ b/src/framework/fwdSolver.ml
@@ -0,0 +1,324 @@
+open Goblint_constraint.ConstrSys
+
+module FwdSolver (System: FwdGlobConstrSys) = struct
+
+ module D = System.D
+ module G = System.G
+
+ module LS = Set.Make (System.LVar)
+
+ module GM = Hashtbl.Make(System.GVar)
+ module LM = Hashtbl.Make(System.LVar)
+ module OM = LM
+
+ let source x = x
+
+(*
+ module OM = Hashtbl.Make(Node)
+ let source = System.LVar.node
+*)
+
+ let gas_default = ref (10,3)
+
+ let lwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if D.equal a b then (a,delay,gas,narrow)
+ else if D.leq b a then
+ if narrow then (D.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (D.narrow a b, delay,gas-1,true)
+ else if narrow then (D.join a b,delay0,gas,false)
+ else if delay <= 0 then (D.widen a (D.join a b),0,gas,false)
+ else (D.join a b, delay-1,gas,false)
+
+ let gwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if G.equal a b then (a,delay,gas,narrow)
+ else if G.leq b a then
+ if narrow then (G.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (G.narrow a b, delay,gas-1,true)
+ else if narrow then (G.join a b,delay0,gas,false)
+ else if delay <= 0 then (G.widen a (G.join a b),0,gas,false)
+ else (G.join a b, delay-1,gas,false)
+
+ let work = ref (([] : System.LVar.t list), LS.empty)
+
+ let add_work x = let (l,s) = !work in
+ if LS.mem x s then ()
+ else work := (x::l, LS.add x s)
+
+ let rem_work () = let (l,s) = !work in
+ match l with
+ | [] -> None
+ | x::xs ->
+ let s = LS.remove x s in
+ let _ = work := (xs,s) in
+ Some x
+
+ type glob = {value : G.t; init : G.t; infl : LS.t; from : (G.t * int * int * bool) OM.t}
+ (*
+ now table from with widening delay and narrowing gas to ensure termination
+ *)
+
+ let glob: glob GM.t = GM.create 100
+
+ (* auxiliary functions for globals *)
+
+ let get_global_ref g =
+ try GM.find glob g
+ with _ ->
+ (let rglob = {value = G.bot (); init = G.bot (); infl = LS.empty; from = OM.create 10} in
+ GM.add glob g rglob;
+ rglob
+ )
+
+ let init_global (g, d) =
+ GM.add glob g {
+ value = d;
+ init = d;
+ infl = LS.empty;
+ from = OM.create 10
+ }
+
+ let get_global_value init from = OM.fold (fun _ (b,_,_,_) a -> G.join a b) from init
+
+ let get_old_global_value x from =
+ let sx = source x in
+ try OM.find from sx
+ with _ ->
+ let (delay,gas) = !gas_default in
+ OM.add from sx (G.bot (),delay,gas,false);
+ (G. bot (),delay,gas,false)
+
+ (* now the getters and setters for globals, setters with warrowing per origin *)
+
+ let get_global x g =
+ let rglob = get_global_ref g in
+ GM.replace glob g { rglob with infl = LS.add x rglob.infl };
+ (* ensure the global is in the hashtable *)
+ rglob.value
+
+ let set_global x g d =
+ let sx = source x in
+ (*
+ replaces old contribution with the new one;
+ reconstructs value of g from contributions;
+ propagates infl and updates value - if value has changed
+ *)
+ let {value;init;infl;from} = get_global_ref g in
+ let (old_xg,delay,gas,narrow) = get_old_global_value x from in
+ let (new_xg,delay,gas,narrow) = gwarrow (old_xg,delay,gas,narrow) d in
+ if G.equal new_xg old_xg then ()
+ else
+ let _ = OM.replace from sx (new_xg,delay,gas,narrow) in
+ let new_g = get_global_value init from in
+ if G.equal value new_g then
+ ()
+ else
+ let _ = LS.iter add_work infl in
+ GM.replace glob g {value = new_g; init = init; infl = LS.empty; from}
+
+ type loc = {loc_value : D.t; loc_init : D.t; loc_infl: System.LVar.t list; loc_from : (D.t * int * int * bool) LM.t}
+ (*
+ init may contain some initial value not provided by separate origin;
+ perhaps, dynamic tracking of dependencies required for certain locals?
+
+ One might additionally maintain in table loc the set of previous contribs
+ for rewoking vacuous previous contributions - important if large values
+ are prematurely propagated which later become obsolete (no contrib from that
+ origin anymore ...
+ *)
+
+ let loc: loc LM.t = LM.create 100
+
+ (* auxiliary functions for locals *)
+
+
+ let get_local_ref x =
+ try LM.find loc x
+ with _ ->
+ (let rloc = {loc_value = D.bot (); loc_init = D.bot (); loc_infl = []; loc_from = LM.create 10} in
+ LM.add loc x rloc;
+ rloc)
+
+ let init_local (x, d) =
+ LM.add loc x {
+ loc_value = d;
+ loc_init = d;
+ loc_infl = [];
+ loc_from = LM.create 10
+ }
+
+ let get_local_value init from = LM.fold (fun _ (b,_,_,_) a -> D.join a b) from init
+
+ let get_old_local_value x from =
+ try LM.find from x
+ with _ -> let (delay,gas) = !gas_default in
+ LM.add from x (D.bot (),delay,gas,false);
+ (D.bot (),delay,gas,false)
+
+ (* now the getters and setters for locals, setters with warrowing per origin *)
+
+ let get_local x y =
+ let rloc = get_local_ref y in
+ LM.replace loc y {rloc with loc_infl = x :: rloc.loc_infl};
+ rloc.loc_value
+
+ let set_local x y d =
+ (*
+ replaces old contribution with the new one;
+ reconstructs value of y from contributions;
+ propagates infl together with y and updates value - if value has changed
+ *)
+ let {loc_value;loc_init;loc_infl;loc_from} = get_local_ref y in
+ let (old_xy,delay,gas,narrow) = get_old_local_value x loc_from in
+ let (new_xy,delay,gas,narrow) = lwarrow (old_xy,delay,gas,narrow) d in
+ if D.equal new_xy old_xy then ()
+ else
+ let _ = LM.replace loc_from x (new_xy,delay,gas,narrow) in
+ let new_y = get_local_value loc_init loc_from in
+ if D.equal loc_value new_y then
+ ()
+ else let _ = add_work y in
+ let _ = List.iter add_work loc_infl in
+ LM.replace loc y {loc_value = new_y; loc_init; loc_infl = []; loc_from}
+
+(*
+ wrapper around propagation function to collect multiple contributions to same unknowns;
+ contributions are delayed until the very end
+*)
+
+ let wrap (x,f) d =
+ let sigma = LM.create 10 in
+ let tau = GM.create 10 in
+ let add_sigma x d =
+ let d = try D.join d (LM.find sigma x) with _ -> d in
+ LM.replace sigma x d in
+ let add_tau g d =
+ let d = try G.join d (GM.find tau g) with _ -> d in
+ GM.replace tau g d in
+ let _ = f d (get_local x) add_sigma (get_global x) add_tau in
+ let _ = GM.iter (set_global x) tau in
+ let _ = LM.iter (set_local x) sigma in
+ ()
+
+ (* ... now the main solver loop ... *)
+
+ let solve xs =
+ let _ = List.iter add_work xs in
+ let rec doit () = match rem_work () with
+ | None -> ()
+ | Some x -> (
+ match System.system x with
+ | None -> doit ()
+ | Some f ->
+ (let rloc = get_local_ref x in
+ wrap (x,f) rloc.loc_value;
+ doit ())
+ ) in
+ let _ = doit () in
+ let sigma = LM.to_seq loc |> Seq.map (fun (k,l) -> (k,l.loc_value)) in
+ let tau = GM.to_seq glob |> Seq.map (fun (k,l) -> (k,l.value)) in
+ (sigma, tau)
+
+
+ let solve localinit globalinit startvars =
+ let _ = List.iter init_local localinit in
+ let _ = List.iter init_global globalinit in
+(*
+ ignore (solve startvars);
+*)
+ solve startvars
+
+ (* ... now the checker! *)
+
+ let check localinit globalinit xs =
+
+ let sigma_out = LM.create 100 in
+ let tau_out = GM.create 100 in
+
+ let get_local x = try (LM.find loc x).loc_value with _ -> D.bot () in
+
+ let check_local x d = if D.leq d (D.bot ()) then ()
+ else let {loc_value:D.t;loc_init;loc_infl;loc_from} = get_local_ref x in
+ if D.leq d loc_value then
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x;
+ List.iter add_work loc_infl
+ )
+ else (
+ Logs.error "Fixpoint not reached for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false;
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x;
+ List.iter add_work loc_infl
+ )
+ ) in
+
+ let get_global g = try (GM.find glob g).value with _ -> G.bot () in
+
+ let check_global x g d =
+ if G.leq d (G.bot ()) then
+ ()
+ else if System.GVar.is_write_only g then
+ GM.replace tau_out g (G.join (GM.find_opt tau_out g |> BatOption.default (G.bot ())) d)
+ else
+ let {value;infl;_} = get_global_ref g in
+ if G.leq d value then
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ else (
+ Logs.error "Fixpoint not reached for global %a\n Side from %a is %a \n Solver Computed %a\n Diff is %a" System.GVar.pretty_trace g System.LVar.pretty_trace x G.pretty d G.pretty value G.pretty_diff (d,value);
+ AnalysisState.verified := Some false;
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ ) in
+
+ let rec doit () =
+ match rem_work () with
+ | None -> (LM.to_seq sigma_out, GM.to_seq tau_out)
+ | Some x -> (match System.system x with
+ | None -> doit ()
+ | Some f -> (
+ f (get_local x)
+ get_local check_local
+ get_global (check_global x);
+ doit ()
+ )
+ ) in
+
+ List.iter (fun (x,_) -> let value = get_local x in LM.add sigma_out x value) localinit;
+ List.iter (fun (g, _) -> let value = get_global g in GM.add tau_out g value) globalinit;
+ List.iter add_work xs;
+ doit ()
+
+ let check localinit globalinit xs =
+ let check_local (x,d) =
+ if D.leq d (get_local_ref x).loc_value then ()
+ else (
+ Logs.error "initialization not subsumed for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false)
+ in
+ let check_global (g,d) =
+ if G.leq d (get_global_ref g).value then ()
+ else (
+ Logs.error "initialization not subsumed for global %a" System.GVar.pretty_trace g;
+ AnalysisState.verified := Some false;
+ ) in
+
+ let _ = List.iter check_local localinit in
+ let _ = List.iter check_global globalinit in
+
+ check localinit globalinit xs
+end
diff --git a/src/framework/wbu.ml b/src/framework/wbu.ml
new file mode 100644
index 0000000000..79feac4a1c
--- /dev/null
+++ b/src/framework/wbu.ml
@@ -0,0 +1,435 @@
+open Goblint_constraint.ConstrSys
+(*
+ rhs should not query locals!
+*)
+open Messages
+
+module FwdWBuSolver (System: FwdGlobConstrSys) = struct
+
+ module D = System.D
+ module G = System.G
+
+ module LS = Set.Make (System.LVar)
+
+ module GM = Hashtbl.Make(System.GVar)
+ module LM = Hashtbl.Make(System.LVar)
+
+(*
+ module OM = LM
+ let source x = x
+*)
+ module OM = Hashtbl.Make(Node)
+ let source = System.LVar.node
+
+ let gas_default = ref (10,3)
+
+ let lwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if D.equal a b then (a,delay,gas,narrow)
+ else if D.leq b a then
+ (
+ if tracing then trace "bunarrow" "Narrowing: %b" narrow;
+ if narrow then (D.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (D.narrow a b, delay,gas-1,true)
+ )
+ else if narrow then (D.join a b,delay0,gas,false)
+ else if delay <= 0 then (D.widen a (D.join a b),0,gas,false)
+ else (D.join a b, delay-1,gas,false)
+
+ let gwarrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if G.equal a b then (a,delay,gas,narrow)
+ else if G.leq b a then
+ (
+ if narrow then (G.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (G.narrow a b, delay,gas-1,true)
+ )
+ else if narrow then (G.join a b,delay0,gas,false)
+ else if delay <= 0 then (G.widen a (G.join a b),0,gas,false)
+ else (G.join a b, delay-1,gas,false)
+
+
+(*
+ work list just for checking ...
+*)
+
+ let work = ref (([] : System.LVar.t list), LS.empty)
+ let set = ref LS.empty
+
+ let add_work x = let (l,s) = !work in
+ if LS.mem x s then ()
+ else work := (x::l, LS.add x s)
+
+ let add_set x =
+ set := (LS.add x !set)
+
+ let in_work x = let (_,s) = !work in
+ LS.mem x s
+
+ let in_set x =
+ LS.mem x !set
+
+ let rem_work () = let (l,s) = !work in
+ match l with
+ | [] -> None
+ | x::xs ->
+ let s = LS.remove x s in
+ let _ = work := (xs,s) in
+ Some x
+
+ let rem_set x =
+ set := LS.remove x !set
+
+ let extract () =
+ match LS.choose_opt !set with
+ | None -> None
+ | Some x -> (
+ set := LS.remove x !set;
+ Some x
+ )
+
+ type glob = {value : G.t; init : G.t; infl : LS.t ; last: G.t LM.t;
+ from : (G.t * int * int * bool * LS.t) OM.t}
+
+
+ let glob: glob GM.t = GM.create 100
+
+ (* auxiliary functions for globals *)
+
+ let get_global_ref g =
+ try GM.find glob g
+ with _ ->
+ (
+ if tracing then trace "unknownsize" "Number of globals so far: %d" (GM.length glob);
+ let rglob = {value = G.bot (); init = G.bot (); infl = LS.empty; last = LM.create 10; from = OM.create 10} in
+ GM.add glob g rglob;
+ rglob
+ )
+
+ let init_global (g, d) =
+ GM.add glob g {
+ value = d;
+ init = d;
+ infl = LS.empty;
+ last = LM.create 10;
+ from = OM.create 10
+ }
+
+ let get_global_value init from = OM.fold (fun _ (b,_,_,_,_) a -> G.join a b) from init
+
+ let get_old_global_value x from =
+ try OM.find from x
+ with _ ->
+ let (delay,gas) = !gas_default in
+ OM.add from x (G.bot (),delay,gas,false,LS.empty);
+ (G. bot (),delay,gas,false,LS.empty)
+
+ let get_last_contrib orig set last =
+ LS.fold (fun x d -> G.join d (LM.find last x)) set (G.bot())
+
+ (* determine the join of all last contribs of unknowns with same orig *)
+
+ (* now the getters for globals *)
+
+ let get_global x g =
+ let rglob = get_global_ref g in
+ GM.replace glob g { rglob with infl = LS.add x rglob.infl }; (* ensure the global is in the hashtable *)
+ rglob.value
+
+ type loc = {loc_value : D.t; loc_init : D.t;
+ called: bool ref; aborted: bool ref;
+ loc_from : (D.t * int * int * bool) LM.t}
+(*
+ init may contain some initial value not provided by separate origin;
+ perhaps, dynamic tracking of dependencies required for certain locals?
+*)
+
+ let loc: loc LM.t = LM.create 100
+
+ (* auxiliary functions for locals *)
+
+
+ let get_local_ref x =
+ try LM.find loc x
+ with _ ->
+ (
+ if tracing then trace "unknownsize" "Number of locals so far: %d" (LM.length loc);
+ let rloc = {loc_value = D.bot (); loc_init = D.bot ();
+ called = ref false; aborted = ref false;
+ loc_from = LM.create 10} in
+ LM.add loc x rloc;
+ rloc)
+
+ let init_local (x, d) =
+ LM.add loc x {
+ loc_value = d;
+ loc_init = d;
+ called = ref false;
+ aborted = ref false;
+ loc_from = LM.create 10
+ }
+
+ let get_local_value init from = LM.fold (fun _ (b,_,_,_) a -> D.join a b) from init
+
+ let get_old_local_value x from =
+ try LM.find from x
+ with _ -> let (delay,gas) = !gas_default in
+ LM.add from x (D.bot (),delay,gas,false);
+ (D.bot (),delay,gas,false)
+
+ (*
+ Now the main solving consisting of the mutual recursive functions
+ set_globals, set_locals, and iterate
+*)
+
+ let rec set_global x g d =
+ let sx = source x
+(*
+ replaces old contribution with the new one;
+ reconstructs value of g from contributions;
+ propagates infl and updates value - if value has changed
+*)
+ in
+ (* if tracing then trace "set_global" "set_global: \n From: %a \nOn:%a \n Value: %a" System.LVar.pretty_trace x System.GVar.pretty_trace g G.pretty d; *)
+ let {value;init;infl;last;from} = get_global_ref g in
+ let (old_xg,delay,gas,narrow,set) = get_old_global_value sx from in
+ let () = LM.add last x d in
+ let set = LS.add x set in
+ let d_new = get_last_contrib sx set last in
+ let (new_xg,delay,gas,narrow) = gwarrow (old_xg,delay,gas,narrow) d_new in
+ let () = OM.replace from sx (new_xg,delay,gas,narrow,set) in
+ if G.equal new_xg old_xg then (
+ if tracing then trace "set_globalc" "no change!"
+ )
+ else
+ begin
+ if tracing then trace "set_globalc" "new contribution registered!";
+ let new_g = get_global_value init from in
+ if G.equal value new_g then
+ ()
+ else
+ let work = infl in
+ let _ = GM.replace glob g {value = new_g; init = init; infl = LS.empty; last; from} in
+ let doit x =
+ let r = get_local_ref x in
+ if !(r.called) then r.aborted := true
+ else (
+ if tracing then trace "iter" "set_global caused iter\n By: %a\nLocal:%a" System.GVar.pretty_trace g System.LVar.pretty_trace x;
+ add_set x
+ )
+ in
+(*
+ if tracing then trace "iter" "Size of work: %d" (LS.seq_of work |> Seq.length);
+*)
+ LS.iter doit work
+ end
+
+ and set_local x y d =
+ (*
+ Contribution from x to y with d
+ replaces old contribution with the new one;
+ reconstructs value of y from contributions;
+ propagates infl together with y and updates value - if value has changed
+ *)
+ if tracing then trace "set_local" "set_local %a from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ if tracing then trace "set_local" "value: %a" D.pretty d;
+ let {loc_value;loc_init;called;aborted;loc_from} as y_record = get_local_ref y in
+ let (old_xy,delay,gas,narrow) = get_old_local_value x loc_from in
+ let (new_xy,delay,gas,narrow) =
+ if !called then lwarrow (old_xy,delay,gas,narrow) d
+ else (d,delay,gas,narrow) in
+ if D.equal new_xy old_xy then (
+ (* If value of x has not changed, nothing to do *)
+ if tracing then trace "set_localc" "no change";
+ if in_set y then (
+ rem_set y; iterate y
+ )
+ else ()
+ )
+ else (
+ if tracing then trace "set_localc" "new contribution";
+ LM.replace loc_from x (new_xy,delay,gas,narrow);
+ let new_y = get_local_value loc_init loc_from in
+ if tracing then trace "set_local" "new value for %a is %a" System.LVar.pretty_trace y D.pretty new_y;
+ if D.equal loc_value new_y then (
+ if tracing then trace "set_local" "no change in local %a after updating from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ if in_set y then (
+ rem_set y; iterate y
+ )
+ else ()
+ )
+ else (
+ let y_record = {y_record with loc_value = new_y} in
+ LM.replace loc y y_record;
+ if !called then (
+ aborted := true;
+ if tracing then trace "set_local" "aborting local %a update from %a" System.LVar.pretty_trace y System.LVar.pretty_trace x;
+ )
+ else (
+ if tracing then trace "set_local" "starting iteration on %a" System.LVar.pretty_trace y;
+ if tracing then trace "iter" "set_local caused iter";
+ rem_set y;
+ iterate y
+ )
+ )
+ )
+
+(*
+ wrapper around propagation function to collect multiple contributions to same unknowns;
+ contributions are delayed until the very end
+*)
+
+ and wrap (x,f) d =
+ let sigma = LM.create 10 in
+ let tau = GM.create 10 in
+ let add_sigma x d =
+ let d = try D.join d (LM.find sigma x) with _ -> d in
+ LM.replace sigma x d in
+ let add_tau g d =
+ let d = try G.join d (GM.find tau g) with _ -> d in
+ GM.replace tau g d in
+ let _ = f d (fun _ -> raise (Failure "Locals queried in rhs??"))
+ add_sigma (get_global x) add_tau in
+ let _ = GM.iter (set_global x) tau in
+ let _ = LM.iter (set_local x) sigma in
+ ()
+
+(*
+ now the actual propagation!
+*)
+
+ and iterate x =
+ (* if tracing then trace "iter" "iterate %a" System.LVar.pretty_trace x; *)
+ let rloc = get_local_ref x in
+ (* if tracing then trace "iter" "current value: %a" D.pretty rloc.loc_value; *)
+ match System.system x with
+ | None -> ()
+ | Some f ->
+ let _ = rloc.called := true in
+ let _ = rloc.aborted := false in
+ let _ = wrap (x,f) rloc.loc_value in
+ let _ = rloc.called := false in
+ if !(rloc.aborted) then (
+ if tracing then trace "iter" "re-iter";
+ iterate x;
+ )
+ else (
+ (* if tracing then trace "iter" "done iterating"; *)
+ )
+
+ (* ... now the main solver loop ... *)
+
+ let solve localinit globalinit xs =
+
+ let toplevel_iterate x =
+ if tracing then trace "iter" "Toplevel iterate on %a" System.LVar.pretty_trace x;
+ iterate x in
+
+ let rec doit () =
+ match extract () with
+ | None -> ()
+ | Some x -> (
+ toplevel_iterate x;
+ doit ()
+ ) in
+
+ if tracing then trace "solver" "Starting bottom-up fixpoint iteration";
+ List.iter init_local localinit;
+ List.iter init_global globalinit;
+ List.iter add_set xs;
+ doit ();
+ let sigma = LM.to_seq loc |> Seq.map (fun (k,l) -> (k,l.loc_value)) in
+ let tau = GM.to_seq glob |> Seq.map (fun (k,l) -> (k,l.value)) in
+ (sigma,tau)
+
+ (* ... now the checker! *)
+
+ let check localinit globalinit xs =
+
+ let sigma_out = LM.create 100 in
+ let tau_out = GM.create 100 in
+
+ let get_local x = try (LM.find loc x).loc_value with _ -> D.bot () in
+
+ let check_local x d = if D.leq d (D.bot ()) then ()
+ else let {loc_value:D.t;loc_init;called;aborted;loc_from} = get_local_ref x in
+ if D.leq d loc_value then
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x
+ )
+ else (
+ Logs.error "Fixpoint not reached for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false;
+ if LM.mem sigma_out x then ()
+ else (
+ LM.add sigma_out x loc_value;
+ add_work x
+ )
+ ) in
+
+ let get_global g = try (GM.find glob g).value with _ -> G.bot () in
+
+ let check_global x g d =
+ if G.leq d (G.bot ()) then
+ ()
+ else if System.GVar.is_write_only g then
+ GM.replace tau_out g (G.join (GM.find_opt tau_out g |> BatOption.default (G.bot ())) d)
+ else
+ let {value;infl;_} = get_global_ref g in
+ if G.leq d value then
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ else (
+ Logs.error "Fixpoint not reached for global %a\n Side from %a is %a \n Solver Computed %a\n Diff is %a" System.GVar.pretty_trace g System.LVar.pretty_trace x G.pretty d G.pretty value G.pretty_diff (d,value);
+ AnalysisState.verified := Some false;
+ if GM.mem tau_out g then ()
+ else (
+ GM.add tau_out g value;
+ LS.iter add_work infl
+ )
+ ) in
+
+ let rec doit () =
+ match rem_work () with
+ | None -> (LM.to_seq sigma_out, GM.to_seq tau_out)
+ | Some x -> (match System.system x with
+ | None -> doit ()
+ | Some f -> (
+ f (get_local x)
+ get_local check_local
+ get_global (check_global x);
+ doit ()
+ )
+ ) in
+
+ List.iter (fun (x,_) -> let value = get_local x in LM.add sigma_out x value) localinit;
+ List.iter (fun (g, _) -> let value = get_global g in GM.add tau_out g value) globalinit;
+ List.iter add_work xs;
+ doit ()
+
+ let check localinit globalinit xs =
+ let check_local (x,d) =
+ if D.leq d (get_local_ref x).loc_value then ()
+ else (
+ Logs.error "initialization not subsumed for local %a" System.LVar.pretty_trace x;
+ AnalysisState.verified := Some false)
+ in
+ let check_global (g,d) =
+ if G.leq d (get_global_ref g).value then ()
+ else (
+ Logs.error "initialization not subsumed for global %a" System.GVar.pretty_trace g;
+ AnalysisState.verified := Some false;
+ ) in
+
+ let _ = List.iter check_local localinit in
+ let _ = List.iter check_global globalinit in
+
+ check localinit globalinit xs
+end
diff --git a/src/goblint.ml b/src/goblint.ml
index 2a0ab3ce0f..ded43c3352 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -56,7 +56,7 @@ let main () =
else
None
in
- (* This is run independant of the autotuner being enabled or not to be sound for programs with longjmp *)
+ (* This is run independent of the autotuner being enabled or not to be sound for programs with longjmp *)
AutoSoundConfig.activateLongjmpAnalysesWhenRequired ();
if get_string "ana.specification" <> "" then AutoSoundConfig.enableAnalysesForSpecification ();
if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 60dd07f68d..74862719bb 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -4,6 +4,8 @@
module Maingoblint = Maingoblint
module Control = Control
+module FwdControl = FwdControl
+module FwdSolver = FwdSolver
module Server = Server
(** {2 CFG}
@@ -22,6 +24,7 @@ module CfgTools = CfgTools
module Analyses = Analyses
module Constraints = Constraints
+module FwdConstraints = FwdConstraints
module CompareConstraints = CompareConstraints
module AnalysisState = AnalysisState
module AnalysisStateUtil = AnalysisStateUtil
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 861f51ad5a..6a51a12325 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -550,7 +550,11 @@ let do_analyze change_info merged_AST =
let at = String.concat ", " @@ get_string_list "trans.activated" in
Logs.debug "Activated analyses: %s" aa;
Logs.debug "Activated transformations: %s" at;
- try Control.analyze change_info ast funs
+ let analyze = if (get_string "solver" = "fwd" ||
+ get_string "solver" = "wbu" ||
+ get_string "solver" = "bu")
+ then FwdControl.analyze else Control.analyze in
+ try analyze change_info ast funs
with e ->
let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *)
AnalysisState.should_warn := true; (* such that the `about to crash` message gets printed *)
@@ -594,30 +598,30 @@ let do_html_output () =
let do_gobview cilfile =
let gobview = GobConfig.get_bool "gobview" in
if gobview then (
- let save_run = GobConfig.get_string "save_run" in
- let run_dir = Fpath.v(if save_run <> "" then save_run else "run") in
- (* copy relevant c files to gobview directory *)
- let file_dir = Fpath.(run_dir / "files") in
- GobSys.mkdir_or_exists file_dir;
- let file_loc = Hashtbl.create 113 in
- let copy (path, i) =
- let name, ext = Fpath.split_ext (Fpath.base path) in
- let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int i) name) in
- let dest = Fpath.(file_dir // unique_name) in
- let gobview_path = match Fpath.relativize ~root:run_dir dest with
- | Some p -> Fpath.to_string p
- | None -> failwith "The gobview directory should be a prefix of the paths of c files copied to the gobview directory" in
- Hashtbl.add file_loc (Fpath.to_string path) gobview_path;
- FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest)
- in
- let source_paths = Preprocessor.FpathH.to_list Preprocessor.dependencies |> List.concat_map (fun (_, m) -> Fpath.Map.fold (fun p _ acc -> p::acc) m []) in
- let source_file_paths = List.filteri_map (fun i e -> if Fpath.is_file_path e then Some (e, i) else None) source_paths in
- List.iter copy source_file_paths;
- Serialize.marshal file_loc (Fpath.(run_dir / "file_loc.marshalled"));
- (* marshal timing statistics *)
- let stats = Fpath.(run_dir / "stats.marshalled") in
- Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats;
- )
+ let save_run = GobConfig.get_string "save_run" in
+ let run_dir = Fpath.v(if save_run <> "" then save_run else "run") in
+ (* copy relevant c files to gobview directory *)
+ let file_dir = Fpath.(run_dir / "files") in
+ GobSys.mkdir_or_exists file_dir;
+ let file_loc = Hashtbl.create 113 in
+ let copy (path, i) =
+ let name, ext = Fpath.split_ext (Fpath.base path) in
+ let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int i) name) in
+ let dest = Fpath.(file_dir // unique_name) in
+ let gobview_path = match Fpath.relativize ~root:run_dir dest with
+ | Some p -> Fpath.to_string p
+ | None -> failwith "The gobview directory should be a prefix of the paths of c files copied to the gobview directory" in
+ Hashtbl.add file_loc (Fpath.to_string path) gobview_path;
+ FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest)
+ in
+ let source_paths = Preprocessor.FpathH.to_list Preprocessor.dependencies |> List.concat_map (fun (_, m) -> Fpath.Map.fold (fun p _ acc -> p::acc) m []) in
+ let source_file_paths = List.filteri_map (fun i e -> if Fpath.is_file_path e then Some (e, i) else None) source_paths in
+ List.iter copy source_file_paths;
+ Serialize.marshal file_loc (Fpath.(run_dir / "file_loc.marshalled"));
+ (* marshal timing statistics *)
+ let stats = Fpath.(run_dir / "stats.marshalled") in
+ Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats;
+ )
let handle_extraspecials () =
let funs = get_string_list "exp.extraspecials" in
diff --git a/src/solver/td_simplified_ref_improved.ml b/src/solver/td_simplified_ref_improved.ml
new file mode 100644
index 0000000000..861b8d1337
--- /dev/null
+++ b/src/solver/td_simplified_ref_improved.ml
@@ -0,0 +1,288 @@
+(** Top-down solver with side effects. Baseline for comparisons with td_parallel solvers ([td_simplified_ref]).
+ This is the same as ([td_simplified]), but it uses records for solver that instead of multiple hashmaps.
+ Additionally, an origin hashmap is maintained to allow for narrowing on globals ...
+*)
+
+open Batteries
+open Goblint_constraint.ConstrSys
+open Goblint_constraint.SolverTypes
+open Messages
+
+module M = Messages
+
+module Base : GenericEqSolver =
+ functor (S:EqConstrSys) ->
+ functor (HM:Hashtbl.S with type key = S.v) ->
+ struct
+ open SolverBox.Warrow (S.Dom)
+ include Generic.SolverStats (S) (HM)
+ module VS = Set.Make (S.Var)
+
+ type var_data = {
+ infl: VS.t;
+ value: S.Dom.t;
+ wpoint: bool;
+ stable: bool;
+ called: bool;
+ }
+
+(*
+ module OM = HM
+ let source x = x
+*)
+
+ module OM = Hashtbl.Make(Node)
+ let source = S.Var.node
+
+ type origin = {
+ init: S.Dom.t;
+ from: (S.Dom.t * int * int * bool * VS.t) OM.t;
+ last: S.Dom.t HM.t
+ }
+
+ let gas_default = ref (10,3)
+
+ let warrow (a,delay,gas,narrow) b =
+ let (delay0,_) = !gas_default in
+ if S.Dom.equal a b then (a,delay,gas,narrow)
+ else if S.Dom.leq b a then
+ if narrow then (S.Dom.narrow a b,delay,gas,true)
+ else if gas<=0 then (a,delay,gas,false)
+ else (S.Dom.narrow a b, delay,gas-1,true)
+ else if narrow then (S.Dom.join a b,delay0,gas,false)
+ else if delay <= 0 then (S.Dom.widen a (S.Dom.join a b),0,gas,false)
+ else (S.Dom.join a b, delay-1,gas,false)
+
+ let get_global_value init from = OM.fold (fun _ (b,_,_,_,_) a -> S.Dom.join a b) from init
+
+ let is_global y = (S.system y = None)
+
+ let solve st vs =
+ let (data : var_data ref HM.t) = HM.create 10 in
+ let (origin : origin HM.t) = HM.create 10 in
+
+ let () = print_solver_stats := fun () ->
+ Logs.debug "|data|=%d" (HM.length data);
+ in
+
+ let add_infl y x =
+ if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
+ let y_ref = HM.find data y in
+ y_ref := { !y_ref with infl = VS.add x !y_ref.infl }
+ in
+
+ let init (x : S.v): var_data ref =
+ let x_ref = HM.find_option data x in
+ match x_ref with
+ | Some r -> r
+ | None ->
+ begin
+ new_var_event x;
+ if tracing then trace "init" "init %a" S.Var.pretty_trace x;
+ let data_x = ref {
+ infl = VS.empty;
+ value = S.Dom.bot ();
+ wpoint = false;
+ stable = false;
+ called = false
+ } in
+ HM.replace data x data_x;
+ let orig_x = {
+ init = S.Dom.bot();
+ from = OM.create 10;
+ last = HM.create 10
+ } in
+ HM.add origin x orig_x;
+ data_x
+ end
+ in
+
+(*
+introduce wrapper to make sure that there is at most one contrib per origin ...
+alternatively, distinguish contribs by session number?
+*)
+ let eq x get set =
+ if tracing then trace "eq" "eq %a" S.Var.pretty_trace x;
+ match S.system x with
+ | None -> S.Dom.bot ()
+ | Some f -> f get set
+ in
+
+ let rec destabilize x =
+ if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x;
+ let x_ref = HM.find data x in
+ let w = !x_ref.infl in
+ x_ref := { !x_ref with infl = VS.empty };
+ VS.iter (fun y ->
+ if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y;
+ let y_ref = HM.find data y in
+ y_ref := { !y_ref with stable = false };
+ if !y_ref.called then ()
+ else destabilize y
+ ) w
+ in
+
+ let rec query x y =
+ let y_ref = init y in
+ if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (!y_ref.stable) (!y_ref.called);
+ get_var_event y;
+ if not (!y_ref.called) then (
+ if is_global y then (
+ y_ref := { !y_ref with stable = true };
+ ) else (
+ y_ref := { !y_ref with called = true };
+ if tracing then trace "iter" "iterate called from query";
+ iterate y;
+ y_ref := { !y_ref with called = false };)
+ ) else (
+ if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y;
+ y_ref := { !y_ref with wpoint = true };
+ );
+ let tmp = !y_ref.value in
+ add_infl y x;
+ if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp;
+ tmp
+
+ and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
+ assert (is_global y);
+ let sx = source x in
+ let y_ref = init y in
+ if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty d;
+ let {init;last;from} = HM.find origin y in
+ let (old_xy,delay,gas,narrow,set) = try OM.find from sx
+ with _ ->
+ let (delay,gas) = !gas_default in
+ let tuple = (S.Dom.bot (),delay,gas,false,VS.empty) in
+ let () = OM.add from sx tuple in
+ tuple in
+ let () = HM.add last x d in
+ let set = VS.add x set in
+ let d = VS.fold (fun x d -> S.Dom.join d (HM.find last x)) set d in
+ let (new_xy,delay,gas,narrow) =
+ if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y;
+ warrow (old_xy,delay,gas,narrow) d in
+ OM.replace from sx (new_xy,delay,gas,narrow,set);
+ if S.Dom.equal new_xy old_xy then ()
+ else (
+ let new_y = get_global_value init from in
+ if S.Dom.equal new_y !y_ref.value then ()
+ else (
+ y_ref := { !y_ref with value = new_y };
+ destabilize y
+ )
+ )
+
+ and wrap_eq x =
+ match S.system x with
+ | None -> S.Dom.bot ()
+ | Some f ->
+ let sigma = HM.create 10 in
+ let add_sigma y d =
+ let d = try S.Dom.join d (HM.find sigma y) with _ -> d in
+ HM.replace sigma y d;
+ side x y d in
+ f (query x) add_sigma
+
+
+ and iterate x = (* ~(inner) solve in td3 *)
+
+ (* begining of iterate*)
+ let x_ref = init x in
+ if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint);
+ assert (S.system x <> None);
+ if not (!x_ref.stable) then (
+ x_ref := { !x_ref with stable = true };
+ let wp = !x_ref.wpoint in (* if x becomes a wpoint during eq, checking this will delay widening until next iterate *)
+ let eqd =
+ wrap_eq x in
+ (*
+ eq x (query x) (side x) in (* d from equation/rhs *)
+ *)
+ let old = !x_ref.value in (* d from older iterate *)
+ let wpd = (* d after widen/narrow (if wp) *)
+ if not wp then eqd
+ else (
+ if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
+ box old eqd)
+ in
+ if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
+ (* old != wpd *)
+ if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
+ update_var_event x old wpd;
+ x_ref := { !x_ref with value = wpd };
+ destabilize x;
+ if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x;
+ (iterate[@tailcall]) x
+ ) else (
+ (* old == wpd *)
+ if not (!x_ref.stable) then (
+ (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
+ if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
+ (iterate[@tailcall]) x
+ ) else (
+ (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *)
+ if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x;
+ x_ref := { !x_ref with wpoint = false };
+ )
+ )
+ )
+ in
+
+ let set_start (x,d) =
+ let x_ref = init x in
+ x_ref := { !x_ref with value = d; stable = true };
+ if is_global x then HM.replace origin x { init = d; from = OM.create 10; last = HM.create 10 }
+ in
+
+ (* beginning of main solve *)
+ start_event ();
+
+ List.iter set_start st;
+
+ List.iter (fun x -> ignore @@ init x) vs;
+ (* If we have multiple start variables vs, we might solve v1, then while solving v2 we side some global which v1 depends on with a new value. Then v1 is no longer stable and we have to solve it again. *)
+ let i = ref 0 in
+ let rec solver () = (* as while loop in paper *)
+ incr i;
+ let unstable_vs = List.filter (neg (fun x -> !(HM.find data x).stable)) vs in
+ if unstable_vs <> [] then (
+ if Logs.Level.should_log Debug then (
+ if !i = 1 then Logs.newline ();
+ Logs.debug "Unstable solver start vars in %d. phase:" !i;
+ List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs;
+ Logs.newline ();
+ flush_all ();
+ );
+ List.iter (fun x ->
+ let x_ref = HM.find data x in
+ x_ref := { !x_ref with called = true };
+ if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
+ iterate x;
+ x_ref := { !x_ref with called = false }
+ ) unstable_vs;
+ solver ();
+ )
+ in
+ solver ();
+ (* After termination, only those variables are stable which are
+ * - reachable from any of the queried variables vs, or
+ * - effected by side-effects and have no constraints on their own (this should be the case for all of our analyses). *)
+
+ stop_event ();
+ if Logs.Level.should_log Debug then (
+ Logs.debug "Data after iterate completed";
+ Logs.debug "|data|=%d" (HM.length data);
+ );
+
+ if GobConfig.get_bool "dbg.print_wpoints" then (
+ Logs.newline ();
+ Logs.debug "Widening points:";
+ HM.filter (fun x_ref -> !x_ref.wpoint) data |> HM.iter (fun k x_ref ->
+ Logs.debug "%a" S.Var.pretty_trace k)
+ );
+
+ HM.map (fun x x_ref -> !x_ref.value) data
+ end
+
+let () =
+ Selector.add_solver ("td_simplified_ref_improved", (module PostSolver.DemandEqIncrSolverFromEqSolver (Base)));
diff --git a/test.c b/test.c
new file mode 100644
index 0000000000..a795306e3f
--- /dev/null
+++ b/test.c
@@ -0,0 +1,14 @@
+//PARAM: --disable ana.int.def_exc --enable ana.int.interval
+#include
+
+
+int main() {
+ int x;
+
+ for(x=0; x < 50; x++){
+ }
+ // HERE
+ __goblint_check(x == 50); // NOWARN (unreachable)
+ return x;
+}
+