From e2665917defba583ee069cb2f70fc4b0e87c5ccc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Apr 2026 10:08:47 +0800 Subject: [PATCH 01/18] Simplified Interface --- src/framework/simplifiedAnalysis.ml | 72 +++++++++++++++++++ src/framework/simplifiedLifter.ml | 103 ++++++++++++++++++++++++++++ 2 files changed, 175 insertions(+) create mode 100644 src/framework/simplifiedAnalysis.ml create mode 100644 src/framework/simplifiedLifter.ml diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml new file mode 100644 index 0000000000..097fc44dcb --- /dev/null +++ b/src/framework/simplifiedAnalysis.ml @@ -0,0 +1,72 @@ +open GoblintCil +open Pretty +open Analyses + + +(** Man(ager) is passed to transfer functions and allows accessing the + context, read values from globals, side-effect values to globals, + and query information from other analyses *) +type ('g,'c,'v) man = + { ask : 'a. 'a Queries.t -> 'a Queries.result + (* To communicate with other analyses *) + ; edge : MyCFG.edge + ; orig_node : MyCFG.node + ; dest_node : MyCFG.node + ; context : 'c + ; global : 'v -> 'g + ; sideg : 'v -> 'g -> unit + } + + + +module type SimplifiedSpec = sig + module type UnknownSet = Printable.S + + module V : UnknownSet (** Set of globals. *) + + module G : Lattice.S (** Domain for globals. *) + module D : Lattice.S (** Domain for locals. *) + + module C : Printable.S (** Context information. *) + + val name : string (** Name of the analysis. *) + + val startstate : D.t (** Initial local state for main. *) + val startcontext: C.t (** Initial context for main. *) + + val query : (G.t, C.t, V.t) man -> D.t -> 'a Queries.t -> 'a Queries.result + + (** A transfer function which handles the assignment of a rval to a lval, i.e., + it handles program points of the form "lval = rval;" *) + val assign: (G.t, C.t, V.t) man -> D.t -> lval -> exp -> D.t + + (** A transfer function which handles conditional branching yielding the + truth value passed as a boolean argument *) + val branch: (G.t, C.t, V.t) man -> D.t -> exp -> bool -> D.t + + (** A transfer function which handles the return statement, i.e., + "return exp" or "return" in the passed function (fundec) *) + val return: (G.t, C.t, V.t) man -> D.t -> exp option -> fundec -> D.t + + (** A transfer function which handles going from the start node of a function (fundec) into + its function body. Meant to handle, e.g., initialization of local variables *) + val body: (G.t, C.t, V.t) man -> D.t -> fundec -> D.t + + (** For a function call "lval = f(args)" or "f(args)", + enter returns the initial state of the callee. *) + val enter : (G.t, C.t, V.t) man -> D.t -> lval option -> fundec -> exp list -> D.t + + (** Combines the states before and after the call. *) + val combine: (G.t, C.t, V.t) man -> D.t -> D.t -> lval option -> fundec -> exp list -> D.t + + (** A transfer function which, for a call to a {e special} function f "lval = f(args)" or "f(args)", + computes the caller state after the function call *) + val special : (G.t, C.t, V.t) man -> D.t -> lval option -> varinfo -> exp list -> D.t + + (** Compute the context for a function call, given the local state and context at the caller, + the called function and the local state inside the callee *) + val context: (G.t, C.t, V.t) man -> (D.t * C.t) -> fundec -> D.t -> C.t + + (** Compute the start state of a new thread starting with the function given by fundec *) + val threadenter: (G.t, C.t, V.t) man -> D.t -> fundec -> exp list -> D.t +end diff --git a/src/framework/simplifiedLifter.ml b/src/framework/simplifiedLifter.ml new file mode 100644 index 0000000000..9297d4d02e --- /dev/null +++ b/src/framework/simplifiedLifter.ml @@ -0,0 +1,103 @@ +open Analyses +open SimplifiedAnalysis + +(** Lift a {!SimplifiedAnalysis.SimplifiedSpec} to a regular {!Analyses.Spec}. + + The simplified interface keeps the current local state as an explicit + argument to transfer functions and has a single [combine] hook. This + adapter reconstructs the regular manager shape and supplies the regular + spec hooks which are identity functions for simplified analyses. *) +module FromSimplifiedSpec (S: SimplifiedSpec): Spec = +struct + module D = S.D + module G = S.G + module C = S.C + module V = + struct + include S.V + let is_write_only _ = false + end + module P = UnitP + + type marshal = unit + + let init _ = () + let finalize () = () + + let name () = S.name + + let startstate _ = S.startstate + let exitstate _ = S.startstate + let morphstate _ d = d + + let startcontext () = S.startcontext + + let simplified_context (man: (D.t, G.t, C.t, V.t) Analyses.man) = + try man.context () with + | Man_failure _ -> S.startcontext + + let conv (man: (D.t, G.t, C.t, V.t) Analyses.man): (G.t, C.t, V.t) SimplifiedAnalysis.man = + { ask = man.ask + ; edge = man.edge + ; orig_node = man.prev_node + ; dest_node = man.node + ; context = simplified_context man + ; global = man.global + ; sideg = man.sideg + } + + let context man fd d = + S.context (conv man) (man.local, simplified_context man) fd d + + let sync man _ = man.local + + let query man = + S.query (conv man) man.local + + let assign man lv e = + S.assign (conv man) man.local lv e + + let vdecl man _ = + man.local + + let branch man e tv = + S.branch (conv man) man.local e tv + + let body man fundec = + S.body (conv man) man.local fundec + + let return man e fundec = + S.return (conv man) man.local e fundec + + let asm man = + man.local + + let skip man = + man.local + + let enter man lval f args = + [man.local, S.enter (conv man) man.local lval f args] + + let special man lval f args = + S.special (conv man) man.local lval f args + + let combine_env man _ _ _ _ _ _ _ = + man.local + + let combine_assign man lval _ f args _ fd _ = + S.combine (conv man) man.local fd lval f args + + let paths_as_set man = + [man.local] + + let threadenter man ~multiple:_ _ f args = + match Cilfacade.find_varinfo_fundec f with + | fd -> [S.threadenter (conv man) man.local fd args] + | exception Not_found -> [man.local] + + let threadspawn man ~multiple:_ _ _ _ _ = + man.local + + let event man _ _ = + man.local +end From 2ade673638f739cd05237deb7ee290d3032e3b38 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Apr 2026 10:18:00 +0800 Subject: [PATCH 02/18] Provide interface to register simplified analysis --- src/analyses/mCPRegistry.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml index 05519dbb62..a7e444268a 100644 --- a/src/analyses/mCPRegistry.ml +++ b/src/analyses/mCPRegistry.ml @@ -49,6 +49,15 @@ let register_analysis = Hashtbl.replace registered_name n !count; incr count +let registered_simplified_analysis (module S:SimplifiedAnalysis.SimplifiedSpec) = + let module S':MCPSpec = struct + include SimplifiedLifter.FromSimplifiedSpec(S) + module A = UnitA + let access _ _ = () + end + in + register_analysis (module S') + let find_spec = Hashtbl.find registered let find_spec_name n = (find_spec n).name let find_id = Hashtbl.find registered_name From 97e4e57c27864f1f9f6776bcc82238fe297422c9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Apr 2026 12:21:37 +0800 Subject: [PATCH 03/18] Progress on analysis Co-authored-by: Copilot --- src/analyses/tutorials/gStoreWidening.ml | 197 +++++++++++++++++ .../tutorials/gStoreWideningHelper.ml | 34 +++ src/analyses/tutorials/gStoreWideningSol.ml | 205 ++++++++++++++++++ src/framework/simplifiedAnalysis.ml | 3 +- .../regression/99-tutorials/05-gstore-zero.c | 28 +++ .../99-tutorials/06-gstore-thread.c | 42 ++++ 6 files changed, 507 insertions(+), 2 deletions(-) create mode 100644 src/analyses/tutorials/gStoreWidening.ml create mode 100644 src/analyses/tutorials/gStoreWideningHelper.ml create mode 100644 src/analyses/tutorials/gStoreWideningSol.ml create mode 100644 tests/regression/99-tutorials/05-gstore-zero.c create mode 100644 tests/regression/99-tutorials/06-gstore-thread.c diff --git a/src/analyses/tutorials/gStoreWidening.ml b/src/analyses/tutorials/gStoreWidening.ml new file mode 100644 index 0000000000..47d2678ce1 --- /dev/null +++ b/src/analyses/tutorials/gStoreWidening.ml @@ -0,0 +1,197 @@ +open GoblintCil +open SimplifiedAnalysis +open GStoreWideningHelper + +(** + There are two regression tests for this analysis, which you can run by calling: + - ./regtest.sh 99 05 + - ./regtest.sh 99 06 + + Running these scripts also produces a visualization of the analysis results as a HTML file in the folder + result. + + You can access these by spinning up a HTTP server, e.g., by calling `python3 -m http.server` + + First fix the TODO: 1) to ensure unreachable code is marked as dead. + Then, tackle TODO: 2) to change this analysis so it tracks global variables + + After modifying things, don't forget to compile by running `make` +*) + + +module Analysis: SimplifiedSpec = struct + let name = "gStoreWidening" + + module I = GStoreWideningHelper.Intervals + + module D = MapDomain.MapBot (Basetype.Variables) (I) + module C = Printable.Unit + + (** TODO: 2) Modify so that we store values for globals instead of always assuming they are top *) + module V = Printable.Unit + module G = Lattice.Unit + + let startstate = D.bot () + let startcontext = () + + (* Evaluate a single variable given a local state *) + let eval_varinfo man state v = + if v.vglob then + (** TODO: 2) Modify so that we store values for globals *) + top_of_var v + else + D.find v state + + (* evaluate an expression given a local state, can remain unmodified *) + let rec eval man (state: D.t) (e: exp) = + try + match e with + | Const (CInt (i, ik, _)) -> + const_int ik i + | Lval (Var v, NoOffset) when GStoreWideningHelper.is_tracked_var v -> + eval_varinfo man state v + | CastE (_, t, e) -> + cast_to_typ t (eval man state e) + | UnOp (Neg, e, t) -> + I.neg (cast_to_typ t (eval man state e)) + | UnOp (BNot, e, t) -> + I.lognot (cast_to_typ t (eval man state e)) + | UnOp (LNot, e, t) -> + begin match I.to_bool (eval man state e) with + | Some b -> I.of_bool (ikind_of_typ t) (not b) + | None -> top_of_typ t + end + | BinOp (op, e1, e2, t) -> + eval_binop man state op e1 e2 t + | _ -> + top_of_exp e + with + | IntDomain.ArithmeticOnIntegerBot _ + | IntDomain.IncompatibleIKinds _ + | Cilfacade.TypeOfError _ -> + top_of_exp e + + (* evaluation of binary operators, can remain unmodified *) + and eval_binop man state op e1 e2 t = + let ik = ikind_of_typ t in + let v1 = cast_to_typ t (eval man state e1) in + let v2 = cast_to_typ t (eval man state e2) in + match op with + | PlusA | PlusPI | IndexPI -> + I.add v1 v2 + | MinusA | MinusPI | MinusPP -> + I.sub v1 v2 + | Mult -> + I.mul v1 v2 + | Div -> + I.div v1 v2 + | Mod -> + I.rem v1 v2 + | BAnd -> + I.logand v1 v2 + | BOr -> + I.logor v1 v2 + | BXor -> + I.logxor v1 v2 + | Shiftlt -> + I.shift_left v1 v2 + | Shiftrt -> + I.shift_right v1 v2 + | Lt | Gt | Le | Ge | Eq | Ne -> + let cmp = + match op with + | Lt -> I.lt v1 v2 + | Gt -> I.gt v1 v2 + | Le -> I.le v1 v2 + | Ge -> I.ge v1 v2 + | Eq -> I.eq v1 v2 + | Ne -> I.ne v1 v2 + | _ -> None + in + begin match cmp with + | Some b -> I.of_bool ik b + | None -> I.top_of ik + end + | LAnd | LOr -> + begin match I.to_bool v1, I.to_bool v2 with + | Some b1, Some b2 -> + let b = if op = LAnd then b1 && b2 else b1 || b2 in + I.of_bool ik b + | _ -> I.top_of ik + end + + let query man state (type a) (q: a Queries.t): a Queries.result = + match q with + | Queries.EvalInt e -> + let ik = ikind_of_exp e in + let v = eval man state e in + begin match I.minimal v, I.maximal v with + | Some l, Some u -> Queries.ID.of_interval ik (l, u) + | _ -> Queries.Result.top q + end + | _ -> + Queries.Result.top q + + let assign man state lval rval = + match is_tracked_lval lval with + | Some v -> + if not v.vglob then + D.add v (cast_to_typ v.vtype (eval man state rval)) state + else + (** TODO: 2) Modify so that we store values for globals *) + state + | None -> + state + + (** TODO: 1) raise Analyses.Deadcode if we branch on a condition that is known-to-be false *) + (* Returns the state resulting when the expression `e` evaluates to `tv` *) + let branch man state e tv = + let e_evaluated_to_bool = I.to_bool (eval man state e) in + state + + + (* Glue code, does not need to be modified for this tutorial *) + let set_lval_top state = function + | Some (Var v, NoOffset) when is_tracked_var v && not v.vglob -> + D.add v (I.top_of (ikind_of_typ v.vtype)) state + | _ -> state + + let return _ state _ _ = + state + + let body _ state f = + List.fold_left (fun acc v -> + if is_tracked_var v then + D.add v (I.top_of (ikind_of_typ v.vtype)) acc + else + acc + ) state f.slocals + + let enter man state _ f args = + List.fold_left2 (fun acc formal actual -> + if is_tracked_var formal then + D.add formal (cast_to_typ formal.vtype (eval man state actual)) acc + else + acc + ) (D.bot ()) f.sformals args + + let combine _ state _ lval _ _ = + set_lval_top state lval + + let special man state lval _ _ = + set_lval_top state lval + + let context _ (_, c) _ _ = + c + + let threadenter _ _ f _ = + List.fold_left (fun acc v -> + if is_tracked_var v then + D.add v (I.top_of (ikind_of_typ v.vtype)) acc + else + acc + ) (D.bot ()) f.sformals +end + +let _ = + MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec) diff --git a/src/analyses/tutorials/gStoreWideningHelper.ml b/src/analyses/tutorials/gStoreWideningHelper.ml new file mode 100644 index 0000000000..21c70713a5 --- /dev/null +++ b/src/analyses/tutorials/gStoreWideningHelper.ml @@ -0,0 +1,34 @@ +(** Contains some definitions that are helpful for the tutorial but out of scope *) +open GoblintCil + +(* Complicated definition for technical reasons relating to different int types *) +module Intervals = IntDomain.IntDomWithDefaultIkind(IntDomain.IntDomLifter (IntDomain.SOverflowUnlifter (IntDomain.Interval))) (IntDomain.PtrDiffIkind) + +let is_tracked_var v = + Cil.isIntegralType v.vtype && not v.vaddrof + +let is_tracked_lval = function + | Var v, NoOffset when is_tracked_var v -> Some v + | _ -> None + +let ikind_of_typ t = + Cilfacade.get_ikind t + +let ikind_of_exp e = + Cilfacade.get_ikind_exp e + +let top_of_typ t = + Intervals.top_of (ikind_of_typ t) + +let top_of_exp e = + Intervals.top_of (ikind_of_exp e) + +let top_of_var v = + top_of_exp (Lval (Var v, NoOffset)) + + +let cast_to_typ t x = + Intervals.cast_to ~kind:Internal (ikind_of_typ t) x + +let const_int ik i = + Intervals.of_int ik i diff --git a/src/analyses/tutorials/gStoreWideningSol.ml b/src/analyses/tutorials/gStoreWideningSol.ml new file mode 100644 index 0000000000..93e749a132 --- /dev/null +++ b/src/analyses/tutorials/gStoreWideningSol.ml @@ -0,0 +1,205 @@ +open GoblintCil +open SimplifiedAnalysis +open GStoreWideningHelper + +(** + + ********************************************************************************************************************** + ** THIS IS THE SOLUTION TO THIS TUTORIAL ANALYSIS, READING THIS BEFORE DOING THE TUTORIAL WILL SPOIL THE FUN. ** + ** YOU HAVE BEEN WARNED. ** + ********************************************************************************************************************** + + There are two regression tests for this analysis, which you can run by calling: + - ./regtest.sh 99 05 + - ./regtest.sh 99 06 + + Running these scripts also produces a visualization of the analysis results as a HTML file in the folder + result. + + You can access these by spinning up a HTTP server, e.g., by calling `python3 -m http.server` + + First fix the TODO: 1) to ensure unreachable code is marked as dead. + Then, tackle TODO: 2) to change this analysis so it tracks global variables + + After modifying things, don't forget to compile by running `make` +*) + + +module Analysis: SimplifiedSpec = struct + let name = "gStoreWideningSol" + + module I = GStoreWideningHelper.Intervals + + module D = MapDomain.MapBot (Basetype.Variables) (I) + module C = Printable.Unit + + (** TODO: 2) Modify so that we store values for globals instead of always assuming they are top *) + module V = Basetype.Variables + module G = I + + let startstate = D.bot () + let startcontext = () + + (* Evaluate a single variable given a local state *) + let eval_varinfo man state v = + if v.vglob then + man.global v + else + D.find v state + + (* evaluate an expression given a local state, can remain unmodified *) + let rec eval man (state: D.t) (e: exp) = + try + match e with + | Const (CInt (i, ik, _)) -> + const_int ik i + | Lval (Var v, NoOffset) when GStoreWideningHelper.is_tracked_var v -> + eval_varinfo man state v + | CastE (_, t, e) -> + cast_to_typ t (eval man state e) + | UnOp (Neg, e, t) -> + I.neg (cast_to_typ t (eval man state e)) + | UnOp (BNot, e, t) -> + I.lognot (cast_to_typ t (eval man state e)) + | UnOp (LNot, e, t) -> + begin match I.to_bool (eval man state e) with + | Some b -> I.of_bool (ikind_of_typ t) (not b) + | None -> top_of_typ t + end + | BinOp (op, e1, e2, t) -> + eval_binop man state op e1 e2 t + | _ -> + top_of_exp e + with + | IntDomain.ArithmeticOnIntegerBot _ + | IntDomain.IncompatibleIKinds _ + | Cilfacade.TypeOfError _ -> + top_of_exp e + + (* evaluation of binary operators, can remain unmodified *) + and eval_binop man state op e1 e2 t = + let ik = ikind_of_typ t in + let v1 = cast_to_typ t (eval man state e1) in + let v2 = cast_to_typ t (eval man state e2) in + match op with + | PlusA | PlusPI | IndexPI -> + I.add v1 v2 + | MinusA | MinusPI | MinusPP -> + I.sub v1 v2 + | Mult -> + I.mul v1 v2 + | Div -> + I.div v1 v2 + | Mod -> + I.rem v1 v2 + | BAnd -> + I.logand v1 v2 + | BOr -> + I.logor v1 v2 + | BXor -> + I.logxor v1 v2 + | Shiftlt -> + I.shift_left v1 v2 + | Shiftrt -> + I.shift_right v1 v2 + | Lt | Gt | Le | Ge | Eq | Ne -> + let cmp = + match op with + | Lt -> I.lt v1 v2 + | Gt -> I.gt v1 v2 + | Le -> I.le v1 v2 + | Ge -> I.ge v1 v2 + | Eq -> I.eq v1 v2 + | Ne -> I.ne v1 v2 + | _ -> None + in + begin match cmp with + | Some b -> I.of_bool ik b + | None -> I.top_of ik + end + | LAnd | LOr -> + begin match I.to_bool v1, I.to_bool v2 with + | Some b1, Some b2 -> + let b = if op = LAnd then b1 && b2 else b1 || b2 in + I.of_bool ik b + | _ -> I.top_of ik + end + + let query man state (type a) (q: a Queries.t): a Queries.result = + match q with + | Queries.EvalInt e -> + let ik = ikind_of_exp e in + let v = eval man state e in + begin match I.minimal v, I.maximal v with + | Some l, Some u -> Queries.ID.of_interval ik (l, u) + | _ -> Queries.Result.top q + end + | _ -> + Queries.Result.top q + + let assign man state lval rval = + match is_tracked_lval lval with + | Some v -> + if not v.vglob then + D.add v (cast_to_typ v.vtype (eval man state rval)) state + else + (** TODO: 2) Modify so that we store values for globals *) + (man.sideg v (cast_to_typ v.vtype (eval man state rval)); + state) + | None -> + state + + (** TODO: 1) raise Analyses.Deadcode if we branch on a condition that is known-to-be false *) + (* Returns the state resulting when the expression `e` evaluates to `tv` *) + let branch man state e tv = + let e_evaluated_to_bool = I.to_bool (eval man state e) in + match e_evaluated_to_bool with + | Some e when e <> tv -> raise Analyses.Deadcode + | _ -> state + + + (* Glue code, does not need to be modified for this tutorial *) + let set_lval_top state = function + | Some (Var v, NoOffset) when is_tracked_var v && not v.vglob -> + D.add v (I.top_of (ikind_of_typ v.vtype)) state + | _ -> state + + let return _ state _ _ = + state + + let body _ state f = + List.fold_left (fun acc v -> + if is_tracked_var v then + D.add v (I.top_of (ikind_of_typ v.vtype)) acc + else + acc + ) state f.slocals + + let enter man state _ f args = + List.fold_left2 (fun acc formal actual -> + if is_tracked_var formal then + D.add formal (cast_to_typ formal.vtype (eval man state actual)) acc + else + acc + ) (D.bot ()) f.sformals args + + let combine _ state _ lval _ _ = + set_lval_top state lval + + let special man state lval _ _ = + set_lval_top state lval + + let context _ (_, c) _ _ = + c + + let threadenter _ _ f _ = + List.fold_left (fun acc v -> + if is_tracked_var v then + D.add v (I.top_of (ikind_of_typ v.vtype)) acc + else + acc + ) (D.bot ()) f.sformals +end + +let _ = + MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec) diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml index 097fc44dcb..cb9580c4cf 100644 --- a/src/framework/simplifiedAnalysis.ml +++ b/src/framework/simplifiedAnalysis.ml @@ -17,10 +17,9 @@ type ('g,'c,'v) man = ; sideg : 'v -> 'g -> unit } - +module type UnknownSet = Printable.S module type SimplifiedSpec = sig - module type UnknownSet = Printable.S module V : UnknownSet (** Set of globals. *) diff --git a/tests/regression/99-tutorials/05-gstore-zero.c b/tests/regression/99-tutorials/05-gstore-zero.c new file mode 100644 index 0000000000..9fb26c26e0 --- /dev/null +++ b/tests/regression/99-tutorials/05-gstore-zero.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated '["gStoreWidening","assert"]' +#include + +int main() { + int x; + int unknown; + + if (unknown) { + x = -5; + } else { + x = -7; + } + + // The above code branches on an uninitialized variable. + // The value of x could be either -5 or -7. + + __goblint_check(x < 0); + + if(x > 8) { + // This is unreachable + x = 10; + } + + // This assert should also hold, as the assignment to 10 is unreachable. + __goblint_check(x < 0); + + return 0; +} diff --git a/tests/regression/99-tutorials/06-gstore-thread.c b/tests/regression/99-tutorials/06-gstore-thread.c new file mode 100644 index 0000000000..76613ed67c --- /dev/null +++ b/tests/regression/99-tutorials/06-gstore-thread.c @@ -0,0 +1,42 @@ +// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","base","mallocWrapper"]' --set ana.base.privatization none --enable exp.globs_are_top +// Additional analyses are activated so framework can handle thread creation +#include +#include +int global = 0; + +void* thread(void* arg) { + + if(global < 0) { + global = -58; + } else { + global = 1; + } + + return NULL; +} + +int main() { + int x = 11; + + pthread_t t; + pthread_create(&t, NULL, &thread, NULL); + + global = x*x; + + if(global > 200) { + global = -12; + } + + __goblint_check(global < 200); + __goblint_check(global >= 0); + + + pthread_join(t, NULL); + + global = 42; + + // This is out of reach here + __goblint_check(global == 42); + + return 0; +} From 6fa5d4f92685bdbc71b257e50f971a13f34979cd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Apr 2026 12:28:58 +0800 Subject: [PATCH 04/18] Progress --- src/goblint_lib.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 92fa69c3b4..10140e0728 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -153,6 +153,13 @@ module Signs = Signs module Taint = Taint module UnitAnalysis = UnitAnalysis +module GStoreWidening = GStoreWidening +module GStoreWideningHelper = GStoreWideningHelper +module GStoreWideningSol = GStoreWideningSol + +module SimplifiedAnalysis = SimplifiedAnalysis +module SimplifiedLifter = SimplifiedLifter + (** {2 Other} *) module Assert = Assert From 23015e6b58bcdb4f4296aa294fe78047d70c9533 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 14 Dec 2022 22:17:44 +0200 Subject: [PATCH 05/18] Move devcontainer setup into Dockerfile for prebuilding --- .devcontainer/Dockerfile | 7 +++++++ .devcontainer/devcontainer.json | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 1d8778e5e5..325fcdd62a 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -1,6 +1,9 @@ # just -opam tag because make setup will install ocaml compiler FROM ocaml/opam:ubuntu-22.04-opam AS dev +# copy only files for make setup to cache docker layers without code changes +COPY --chown=opam Makefile make.sh goblint.opam goblint.opam.locked /home/opam/docker/analyzer/ + # TODO: use opam depext RUN sudo apt-get update \ && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl @@ -16,3 +19,7 @@ ENV LC_ALL=C.UTF-8 RUN cd /home/opam/opam-repository \ && git pull origin master \ && opam update + +RUN cd /home/opam/docker/analyzer \ + && make setup \ + && make dev diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 2bf28b3c6f..486bb555a0 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -8,7 +8,7 @@ "context": ".." }, "remoteUser": "opam", - "postCreateCommand": "make setup; make dev", + "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", "runArgs": ["--init", "--env-file", ".devcontainer/devcontainer.env"], // TODO: why --init added by default? From 921a98c4c88a24b44688ad4caa30537264865d26 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 14 Dec 2022 22:37:27 +0200 Subject: [PATCH 06/18] Inline make dev into devcontainer Avoids error when setting up pre-commit hook. --- .devcontainer/Dockerfile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 325fcdd62a..85113c3547 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -22,4 +22,6 @@ RUN cd /home/opam/opam-repository \ RUN cd /home/opam/docker/analyzer \ && make setup \ - && make dev + && eval $(opam env) \ + && opam install -y utop ocaml-lsp-server ocp-indent \ + && sudo gem install parallel From eb107d38da5c4f1cfc41b9a39ae5da54d5006b45 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Sat, 25 Apr 2026 11:06:41 +0300 Subject: [PATCH 07/18] Remove unused opens in assert analysis --- src/analyses/assert.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 1d500f7f31..966215f784 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -1,9 +1,7 @@ (** Analysis of [assert] results ([assert]). *) -open Batteries open GoblintCil open Analyses -open GobConfig module Spec : Analyses.MCPSpec = struct From 0f04b3b0d16639dafbfd81df17db0d5733d665cf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Sat, 25 Apr 2026 11:07:42 +0300 Subject: [PATCH 08/18] Remove unused interval_to_bool in IntervalSetDomain --- src/cdomain/value/cdomains/int/intervalSetDomain.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml index 3fe5ebfb1e..08b5c27aa3 100644 --- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml +++ b/src/cdomain/value/cdomains/int/intervalSetDomain.ml @@ -301,7 +301,6 @@ struct let ne ik x y = not_bool @@ eq ik x y let interval_to_int i = Interval.to_int (Some i) - let interval_to_bool i = Interval.to_bool (Some i) let bit f ik (i1, i2) = From 111f47948fddb8a10661eb4b8d39191146fb930b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 5 May 2026 14:46:26 +0300 Subject: [PATCH 09/18] Remove unused opens from SimplifiedAnalysis Avoids warnings on build. --- src/framework/simplifiedAnalysis.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml index cb9580c4cf..d798c99b5b 100644 --- a/src/framework/simplifiedAnalysis.ml +++ b/src/framework/simplifiedAnalysis.ml @@ -1,6 +1,4 @@ open GoblintCil -open Pretty -open Analyses (** Man(ager) is passed to transfer functions and allows accessing the From 7f5278113d5fbe9a369c8111af0c1ad01bc6ee67 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 5 May 2026 14:47:25 +0300 Subject: [PATCH 10/18] Use prebuilt ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial image for devcontainer --- .devcontainer/devcontainer.json | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 486bb555a0..e054c51857 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -3,10 +3,11 @@ { "name": "Goblint", - "build": { - "dockerfile": "./Dockerfile", - "context": ".." - }, + // "build": { + // "dockerfile": "./Dockerfile", + // "context": ".." + // }, + "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", "remoteUser": "opam", "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", From e7d79876a94e716ac8ddd4ae6b895b9109a436c2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 9 May 2026 15:19:20 +0100 Subject: [PATCH 11/18] Notes on TODOs --- src/analyses/tutorials/gStoreWidening.ml | 45 +++++++++++++++++++----- 1 file changed, 37 insertions(+), 8 deletions(-) diff --git a/src/analyses/tutorials/gStoreWidening.ml b/src/analyses/tutorials/gStoreWidening.ml index 47d2678ce1..9ee713d2d1 100644 --- a/src/analyses/tutorials/gStoreWidening.ml +++ b/src/analyses/tutorials/gStoreWidening.ml @@ -3,19 +3,48 @@ open SimplifiedAnalysis open GStoreWideningHelper (** - There are two regression tests for this analysis, which you can run by calling: + This analysis proceeds in steps, with the steps building on each other. + + For the sake of this analysis, we are assuming that all variables are of integer type. + This allows us to keep the analysis simple in the beginning. + + + 1) First, a simple interval analysis is implemented which tracks intervals + for local variables only. + + The majority of the code is already provided, there is one place where + changes need to be made, namely the handling of branches. + It is marked with TODO: 1). + + 2) Then the analysis is extended to also track values for globals via global store widening + + To this end, one should fix which set of globals to track, and their domain. + Then, assignment and evaluation functions should be changed appropriately. + These are marked with TODO: 2). + + + + + + After modifying things, don't forget to compile by running `make` + + There are regression tests for this analysis, which you can run by calling: - ./regtest.sh 99 05 - ./regtest.sh 99 06 - Running these scripts also produces a visualization of the analysis results as a HTML file in the folder - result. + After fixing the TODO: 1), the first regression test should pass. + After fixing the TODO: 2), both the first and the second tests should pass. + + Running a regression test also produces a visualization of the analysis results as a HTML file in the folder + result. - You can access these by spinning up a HTTP server, e.g., by calling `python3 -m http.server` + You can access these by spinning up a HTTP server for the result directory, + e.g., by calling `python3 -m http.server --directory result`. + Then open `index.xml` in your browser. - First fix the TODO: 1) to ensure unreachable code is marked as dead. - Then, tackle TODO: 2) to change this analysis so it tracks global variables + (When using devcontainer, VSCode will automatically detect the server and + provide a link to open the visualization in your browser.) - After modifying things, don't forget to compile by running `make` *) @@ -150,7 +179,7 @@ module Analysis: SimplifiedSpec = struct state - (* Glue code, does not need to be modified for this tutorial *) + (* The code below does not need to be modified *) let set_lval_top state = function | Some (Var v, NoOffset) when is_tracked_var v && not v.vglob -> D.add v (I.top_of (ikind_of_typ v.vtype)) state From 12c45f28a62902df4c062ffb582e2e36ea7149c0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 9 May 2026 15:47:13 +0100 Subject: [PATCH 12/18] Progress --- src/analyses/tutorials/gStoreWidening.ml | 77 ++++++++++++++++++++++-- src/domains/queries.ml | 6 ++ src/framework/simplifiedAnalysis.ml | 5 ++ 3 files changed, 84 insertions(+), 4 deletions(-) diff --git a/src/analyses/tutorials/gStoreWidening.ml b/src/analyses/tutorials/gStoreWidening.ml index 9ee713d2d1..aee1ce8979 100644 --- a/src/analyses/tutorials/gStoreWidening.ml +++ b/src/analyses/tutorials/gStoreWidening.ml @@ -22,9 +22,23 @@ open GStoreWideningHelper Then, assignment and evaluation functions should be changed appropriately. These are marked with TODO: 2). + 3) Define a helper analysis which tracks for each variable which thread ids are used to write to it, + and use this information to determine whether a variable is effectively local + (i.e., only written by one thread). + + This requires modifying the domain to store thread ids, and modifying the assign function + to record thread ids for global variables. + Then, the query function should be modified to check whether there is only one thread + accessing this variable, and whether it is the current one. + These are marked with TODO: 3). - - + 4) Modify the first analysis to exploit the information from the helper analysis to + track the values of effectively local variables more precisely in the thread that + owns them, while keeping applying global store widening to obtain the perspective + of other threads. + + This will amount to modifying some of the places changed in step 2) + After modifying things, don't forget to compile by running `make` @@ -48,7 +62,7 @@ open GStoreWideningHelper *) -module Analysis: SimplifiedSpec = struct +module GStoreWideningAnalysis: SimplifiedSpec = struct let name = "gStoreWidening" module I = GStoreWideningHelper.Intervals @@ -222,5 +236,60 @@ module Analysis: SimplifiedSpec = struct ) (D.bot ()) f.sformals end +module ThreadSet = ConcDomain.ThreadSet + +module EffectivelyLocalAnalysis:SimplifiedSpec = struct + let name = "effectivelyLocal" + + module D = Lattice.Unit + module C = Printable.Unit + + (** TODO: 3) Modify so we store for each variable which thread ids are used to write to it *) + module V = Printable.Unit + module G = Lattice.Unit + + let startstate = () + let startcontext = () + + let assign man state lval rval = + let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in + let singleton_set = ThreadSet.singleton tid in + match is_tracked_lval lval with + | Some v -> + (* TODO: 3) check if this is a global variable and if it is, record the thread id *) + state + | None -> + state + + let query man state (type a) (q: a Queries.t): a Queries.result = + match q with + | Queries.TutorialEffectivelyLocal v -> + (* TODO: 3) Get the current thread id, and check whether there is only one thread + accessing this variable, and whether it is the current one *) + Queries.Result.top q + | _ -> Queries.Result.top q + + let branch man state e tv = state + + let return _ state _ _ = + state + + let body _ state f = () + + let enter man state _ f args = () + + let combine _ state _ lval _ _ = () + let special man state lval _ _ = () + + let context _ (_, c) _ _ = + c + + let threadenter _ _ f _ = () +end + + + + let _ = - MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec) + MCPRegistry.registered_simplified_analysis (module GStoreWideningAnalysis:SimplifiedSpec); + MCPRegistry.registered_simplified_analysis (module EffectivelyLocalAnalysis:SimplifiedSpec) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 1e42b64b23..835bb1832b 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -147,6 +147,7 @@ type _ t = | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *) | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t + | TutorialEffectivelyLocal: varinfo -> MustBool.t t (** Used in tutorial for effectively local variables. *) type 'a result = 'a @@ -223,6 +224,7 @@ struct | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) | DescendantThreads _ -> (module ConcDomain.ThreadSet) + | TutorialEffectivelyLocal _ -> (module MustBool) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -298,6 +300,7 @@ struct | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () | DescendantThreads _ -> ConcDomain.ThreadSet.top () + | TutorialEffectivelyLocal _ -> MustBool.top () end (* The type any_query can't be directly defined in Any as t, @@ -370,6 +373,7 @@ struct | Any (GhostVarAvailable _) -> 62 | Any InvariantGlobalNodes -> 63 | Any (DescendantThreads _) -> 64 + | Any (TutorialEffectivelyLocal _) -> 65 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -430,6 +434,7 @@ struct | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2 | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2 | Any (DescendantThreads t1), Any (DescendantThreads t2) -> ThreadIdDomain.Thread.compare t1 t2 + | Any (TutorialEffectivelyLocal v1), Any (TutorialEffectivelyLocal v2) -> CilType.Varinfo.compare v1 v2 (* only argumentless queries should remain *) | _, _ -> Stdlib.compare (order a) (order b) @@ -547,6 +552,7 @@ struct | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t + | Any (TutorialEffectivelyLocal v) -> Pretty.dprintf "TutorialEffectivelyLocal %a" CilType.Varinfo.pretty v end let to_value_domain_ask (ask: ask) = diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml index d798c99b5b..3b716371c3 100644 --- a/src/framework/simplifiedAnalysis.ml +++ b/src/framework/simplifiedAnalysis.ml @@ -15,6 +15,11 @@ type ('g,'c,'v) man = ; sideg : 'v -> 'g -> unit } +(** Convert [man] to [Queries.ask]. *) +let ask_of_man man: Queries.ask = { Queries.f = man.ask } + + + module type UnknownSet = Printable.S module type SimplifiedSpec = sig From 2ea57e67c28db7407c6746d1fdfbab5e77d1ed19 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 11 May 2026 14:01:34 +0800 Subject: [PATCH 13/18] Complete tutorial --- src/analyses/tutorials/gStoreWidening.ml | 78 ++++++++-------- src/analyses/tutorials/gStoreWideningSol.ml | 89 +++++++++++++++---- .../regression/99-tutorials/05-gstore-zero.c | 2 +- .../99-tutorials/06-gstore-thread.c | 3 +- .../regression/99-tutorials/07-gstore-mixed.c | 51 +++++++++++ 5 files changed, 168 insertions(+), 55 deletions(-) create mode 100644 tests/regression/99-tutorials/07-gstore-mixed.c diff --git a/src/analyses/tutorials/gStoreWidening.ml b/src/analyses/tutorials/gStoreWidening.ml index aee1ce8979..8990590e5b 100644 --- a/src/analyses/tutorials/gStoreWidening.ml +++ b/src/analyses/tutorials/gStoreWidening.ml @@ -3,61 +3,63 @@ open SimplifiedAnalysis open GStoreWideningHelper (** - This analysis proceeds in steps, with the steps building on each other. + This analysis proceeds in steps, with the steps building on each other. - For the sake of this analysis, we are assuming that all variables are of integer type. - This allows us to keep the analysis simple in the beginning. + For the sake of this analysis, we are assuming that all variables are of integer type. + This allows us to keep the analysis simple in the beginning. - 1) First, a simple interval analysis is implemented which tracks intervals - for local variables only. + 1) First, a simple interval analysis is implemented which tracks intervals + for local variables only. The majority of the code is already provided, there is one place where - changes need to be made, namely the handling of branches. + changes need to be made, namely the handling of branches. It is marked with TODO: 1). - 2) Then the analysis is extended to also track values for globals via global store widening + 2) Then the analysis is extended to also track values for globals via global store widening To this end, one should fix which set of globals to track, and their domain. Then, assignment and evaluation functions should be changed appropriately. These are marked with TODO: 2). - - 3) Define a helper analysis which tracks for each variable which thread ids are used to write to it, + + 3) Define a helper analysis which tracks for each variable which thread ids are used to write to it, and use this information to determine whether a variable is effectively local (i.e., only written by one thread). - This requires modifying the domain to store thread ids, and modifying the assign function - to record thread ids for global variables. + This requires modifying the domain to store thread ids, and modifying the assign function + to record thread ids for global variables. Then, the query function should be modified to check whether there is only one thread - accessing this variable, and whether it is the current one. + accessing this variable, and whether it is the current one. These are marked with TODO: 3). - - 4) Modify the first analysis to exploit the information from the helper analysis to + + 4) Modify the first analysis to exploit the information from the helper analysis to track the values of effectively local variables more precisely in the thread that owns them, while keeping applying global store widening to obtain the perspective of other threads. This will amount to modifying some of the places changed in step 2) - - After modifying things, don't forget to compile by running `make` + + After modifying things, don't forget to compile by running `make` There are regression tests for this analysis, which you can run by calling: - ./regtest.sh 99 05 - ./regtest.sh 99 06 + - ./regtest.sh 99 07 - After fixing the TODO: 1), the first regression test should pass. - After fixing the TODO: 2), both the first and the second tests should pass. + After fixing the TODO: 1), the first regression test should pass. + After fixing the TODO: 2), both the first and the second tests should pass. + After fixing the last TODO:, all three tests should pass - Running a regression test also produces a visualization of the analysis results as a HTML file in the folder - result. + Running a regression test also produces a visualization of the analysis results as a HTML file in the folder + result. - You can access these by spinning up a HTTP server for the result directory, - e.g., by calling `python3 -m http.server --directory result`. - Then open `index.xml` in your browser. + You can access these by spinning up a HTTP server for the result directory, + e.g., by calling `python3 -m http.server --directory result`. + Then open `index.xml` in your browser. - (When using devcontainer, VSCode will automatically detect the server and - provide a link to open the visualization in your browser.) + (When using devcontainer, VSCode will automatically detect the server and + provide a link to open the visualization in your browser.) *) @@ -80,7 +82,7 @@ module GStoreWideningAnalysis: SimplifiedSpec = struct (* Evaluate a single variable given a local state *) let eval_varinfo man state v = if v.vglob then - (** TODO: 2) Modify so that we store values for globals *) + (* TODO: 2) Modify so that we get values for globals *) top_of_var v else D.find v state @@ -236,7 +238,7 @@ module GStoreWideningAnalysis: SimplifiedSpec = struct ) (D.bot ()) f.sformals end -module ThreadSet = ConcDomain.ThreadSet +module ThreadSet = ConcDomain.ThreadSet module EffectivelyLocalAnalysis:SimplifiedSpec = struct let name = "effectivelyLocal" @@ -252,20 +254,24 @@ module EffectivelyLocalAnalysis:SimplifiedSpec = struct let startcontext = () let assign man state lval rval = - let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in - let singleton_set = ThreadSet.singleton tid in - match is_tracked_lval lval with - | Some v -> - (* TODO: 3) check if this is a global variable and if it is, record the thread id *) + (* When the global initializers are evaluated, no threads exists yet *) + if !AnalysisState.global_initialization then state - | None -> - state - + else + let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in + let singleton_set = ThreadSet.singleton tid in + match is_tracked_lval lval with + | Some v -> + (* TODO: 3) check if this is a global variable and if it is, record the thread id *) + state + | None -> + state + let query man state (type a) (q: a Queries.t): a Queries.result = match q with | Queries.TutorialEffectivelyLocal v -> (* TODO: 3) Get the current thread id, and check whether there is only one thread - accessing this variable, and whether it is the current one *) + accessing this variable, and whether it is the current one *) Queries.Result.top q | _ -> Queries.Result.top q diff --git a/src/analyses/tutorials/gStoreWideningSol.ml b/src/analyses/tutorials/gStoreWideningSol.ml index 93e749a132..3252e1f499 100644 --- a/src/analyses/tutorials/gStoreWideningSol.ml +++ b/src/analyses/tutorials/gStoreWideningSol.ml @@ -8,20 +8,6 @@ open GStoreWideningHelper ** THIS IS THE SOLUTION TO THIS TUTORIAL ANALYSIS, READING THIS BEFORE DOING THE TUTORIAL WILL SPOIL THE FUN. ** ** YOU HAVE BEEN WARNED. ** ********************************************************************************************************************** - - There are two regression tests for this analysis, which you can run by calling: - - ./regtest.sh 99 05 - - ./regtest.sh 99 06 - - Running these scripts also produces a visualization of the analysis results as a HTML file in the folder - result. - - You can access these by spinning up a HTTP server, e.g., by calling `python3 -m http.server` - - First fix the TODO: 1) to ensure unreachable code is marked as dead. - Then, tackle TODO: 2) to change this analysis so it tracks global variables - - After modifying things, don't forget to compile by running `make` *) @@ -42,7 +28,8 @@ module Analysis: SimplifiedSpec = struct (* Evaluate a single variable given a local state *) let eval_varinfo man state v = - if v.vglob then + if v.vglob && not (man.ask (Queries.TutorialEffectivelyLocal v)) then + (* TODO: 2) Modify so that we get values for globals *) man.global v else D.find v state @@ -145,7 +132,10 @@ module Analysis: SimplifiedSpec = struct else (** TODO: 2) Modify so that we store values for globals *) (man.sideg v (cast_to_typ v.vtype (eval man state rval)); - state) + if man.ask (Queries.TutorialEffectivelyLocal v) then + D.add v (cast_to_typ v.vtype (eval man state rval)) state + else + state) | None -> state @@ -201,5 +191,70 @@ module Analysis: SimplifiedSpec = struct ) (D.bot ()) f.sformals end +module ThreadSet = ConcDomain.ThreadSet + +module EffectivelyLocalAnalysis:SimplifiedSpec = struct + let name = "effectivelyLocalSol" + + module D = Lattice.Unit + module C = Printable.Unit + + (** TODO: 3) Modify so we store for each variable which thread ids are used to write to it *) + module V = Basetype.Variables + module G = ThreadSet + + let startstate = () + let startcontext = () + + let assign man state lval rval = + (* When the global initializers are evaluated, no threads exists yet *) + if !AnalysisState.global_initialization then + state + else + let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in + let singleton_set = ThreadSet.singleton tid in + match is_tracked_lval lval with + | Some v -> + (* TODO: 3) check if this is a global variable and if it is, record the thread id *) + if v.vglob then + (man.sideg v singleton_set; state) + else + state + | None -> + state + + let query man state (type a) (q: a Queries.t): a Queries.result = + match q with + | Queries.TutorialEffectivelyLocal v when not !AnalysisState.global_initialization -> + (* TODO: 3) Get the current thread id, and check whether there is only one thread + accessing this variable, and whether it is the current one *) + let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in + let singleton_set = ThreadSet.singleton tid in + let writers = man.global v in + ThreadSet.equal singleton_set writers + | _ -> Queries.Result.top q + + let branch man state e tv = state + + let return _ state _ _ = + state + + let body _ state f = () + + let enter man state _ f args = () + + let combine _ state _ lval _ _ = () + let special man state lval _ _ = () + + let context _ (_, c) _ _ = + c + + let threadenter _ _ f _ = () +end + + + + let _ = - MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec) + MCPRegistry.registered_simplified_analysis (module Analysis:SimplifiedSpec); + MCPRegistry.registered_simplified_analysis (module EffectivelyLocalAnalysis:SimplifiedSpec) diff --git a/tests/regression/99-tutorials/05-gstore-zero.c b/tests/regression/99-tutorials/05-gstore-zero.c index 9fb26c26e0..b68036ea1d 100644 --- a/tests/regression/99-tutorials/05-gstore-zero.c +++ b/tests/regression/99-tutorials/05-gstore-zero.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated '["gStoreWidening","assert"]' +// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","escape"]' #include int main() { diff --git a/tests/regression/99-tutorials/06-gstore-thread.c b/tests/regression/99-tutorials/06-gstore-thread.c index 76613ed67c..397471ed8e 100644 --- a/tests/regression/99-tutorials/06-gstore-thread.c +++ b/tests/regression/99-tutorials/06-gstore-thread.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","base","mallocWrapper"]' --set ana.base.privatization none --enable exp.globs_are_top +// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","base","mallocWrapper","escape"]' --set ana.base.privatization none --enable exp.globs_are_top // Additional analyses are activated so framework can handle thread creation #include #include @@ -16,6 +16,7 @@ void* thread(void* arg) { } int main() { + global = 0; int x = 11; pthread_t t; diff --git a/tests/regression/99-tutorials/07-gstore-mixed.c b/tests/regression/99-tutorials/07-gstore-mixed.c new file mode 100644 index 0000000000..49ff3ed520 --- /dev/null +++ b/tests/regression/99-tutorials/07-gstore-mixed.c @@ -0,0 +1,51 @@ +// SKIP PARAM: --set ana.activated '["gStoreWidening","effectivelyLocal","assert","base","mallocWrapper","thread","threadid","escape"]' --set ana.base.privatization none --enable exp.globs_are_top +// Additional analyses are activated so framework can handle thread creation +#include +#include +int global = 0; +int thread_owned = 0; + +void* thread(void* arg) { + + thread_owned = 42; + __goblint_check(thread_owned == 42); + + if(global < 0) { + global = -58; + } else { + global = 1; + } + + thread_owned = 11; + __goblint_check(thread_owned == 11); + + return NULL; +} + +int main() { + int x = 11; + global = 0; + + pthread_t t; + pthread_create(&t, NULL, &thread, NULL); + + global = x*x; + + if(global > 200) { + global = -12; + } + + __goblint_check(global < 200); + __goblint_check(global >= 0); + __goblint_check(thread_owned >= 0); + + + pthread_join(t, NULL); + + global = 42; + + // This is out of reach here + __goblint_check(global == 42); + + return 0; +} From 9459b5be17e956062cac6fbbe813374572cd441c Mon Sep 17 00:00:00 2001 From: Ali Rasim Kocal Date: Wed, 13 May 2026 12:29:13 +0200 Subject: [PATCH 14/18] Fixes in Dockerfile and devcontainer --- .devcontainer/Dockerfile | 19 +++++++++++++------ .devcontainer/devcontainer.json | 4 ++-- 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 85113c3547..64c258cb02 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -1,13 +1,14 @@ # just -opam tag because make setup will install ocaml compiler FROM ocaml/opam:ubuntu-22.04-opam AS dev -# copy only files for make setup to cache docker layers without code changes -COPY --chown=opam Makefile make.sh goblint.opam goblint.opam.locked /home/opam/docker/analyzer/ - # TODO: use opam depext RUN sudo apt-get update \ && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl +# copy only files for make setup to cache docker layers without code changes +COPY --chown=opam Makefile make.sh goblint.opam goblint.opam.locked /home/opam/docker/analyzer/ + + # remove default Docker git credentials added by opam base image: https://github.com/avsm/ocaml-dockerfile/blob/f184554282a3836bf3f1c34d20e77d0530f8349d/src-opam/dockerfile_linux.ml#L24-L28 # this prevents devcontainer from using outside git credentials: https://code.visualstudio.com/docs/remote/containers#_sharing-git-credentials-with-your-container RUN rm ~/.gitconfig @@ -15,13 +16,19 @@ RUN rm ~/.gitconfig # otherwise perl (not ruby!) complains during regression testing ENV LC_ALL=C.UTF-8 +USER opam + # update local opam repository because base image may be outdated RUN cd /home/opam/opam-repository \ && git pull origin master \ && opam update RUN cd /home/opam/docker/analyzer \ - && make setup \ + && make setup + +RUN cd /home/opam/docker/analyzer \ && eval $(opam env) \ - && opam install -y utop ocaml-lsp-server ocp-indent \ - && sudo gem install parallel + && opam -y install ocaml-lsp-server ocamlformat \ + && sudo gem install parallel os + +RUN sudo apt-get install -y python3-pygments graphviz diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index e054c51857..54d59a149c 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -9,9 +9,9 @@ // }, "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", "remoteUser": "opam", - "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", + "updateRemoteUserUID": true, - "runArgs": ["--init", "--env-file", ".devcontainer/devcontainer.env"], // TODO: why --init added by default? + "postCreateCommand": "if [ ! -e _opam ] && [ ! -L _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi", "extensions": [ "ocamllabs.ocaml-platform", From 9179a770a35d24cc08a854dec9d6e8da3ec4d7b0 Mon Sep 17 00:00:00 2001 From: Ali Rasim Kocal Date: Wed, 13 May 2026 15:42:32 +0200 Subject: [PATCH 15/18] fm-tutorial: Some improvements to the devcontainer --- .devcontainer/Dockerfile | 8 ++++---- .devcontainer/devcontainer.json | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 64c258cb02..27bcfee631 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -3,7 +3,8 @@ FROM ocaml/opam:ubuntu-22.04-opam AS dev # TODO: use opam depext RUN sudo apt-get update \ - && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl + && sudo apt-get install -y libgmp-dev libmpfr-dev m4 autoconf gcc-multilib pkg-config ruby gem curl python3-pygments graphviz \ + && sudo rm -rf /var/lib/apt/lists/* # copy only files for make setup to cache docker layers without code changes COPY --chown=opam Makefile make.sh goblint.opam goblint.opam.locked /home/opam/docker/analyzer/ @@ -24,11 +25,10 @@ RUN cd /home/opam/opam-repository \ && opam update RUN cd /home/opam/docker/analyzer \ - && make setup + && make setup RUN cd /home/opam/docker/analyzer \ && eval $(opam env) \ - && opam -y install ocaml-lsp-server ocamlformat \ + && opam install -y ocaml-lsp-server ocamlformat dune=3.19.1 \ && sudo gem install parallel os -RUN sudo apt-get install -y python3-pygments graphviz diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 54d59a149c..f36b63bb24 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -9,10 +9,11 @@ // }, "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", "remoteUser": "opam", - "updateRemoteUserUID": true, "postCreateCommand": "if [ ! -e _opam ] && [ ! -L _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi", + "runArgs": ["--init", "--env-file", ".devcontainer/devcontainer.env"], // TODO: why --init added by default? + "extensions": [ "ocamllabs.ocaml-platform", "hackwaly.ocamlearlybird" From 9e03c23983c3d5f3feae655991c53e12054d1457 Mon Sep 17 00:00:00 2001 From: Ali Rasim Kocal Date: Wed, 13 May 2026 15:46:13 +0200 Subject: [PATCH 16/18] fm-tutorial: Handle existing _opam better --- .devcontainer/devcontainer.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index f36b63bb24..8938b12b7a 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -10,7 +10,7 @@ "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", "remoteUser": "opam", - "postCreateCommand": "if [ ! -e _opam ] && [ ! -L _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi", + "postCreateCommand": "if [ -e _opam ] && [ ! -L _opam ]; then echo 'ERROR: _opam already exists and is not a symlink. Delete it manually on the host and rebuild the container.' >&2; exit 1; elif [ ! -e _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi", "runArgs": ["--init", "--env-file", ".devcontainer/devcontainer.env"], // TODO: why --init added by default? From d63cca0c16200dc6ad87e90edcdecab411ef4413 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 May 2026 11:06:04 +0300 Subject: [PATCH 17/18] Install test dependencies in devcontainer --- .devcontainer/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 27bcfee631..b424b4d351 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -25,7 +25,7 @@ RUN cd /home/opam/opam-repository \ && opam update RUN cd /home/opam/docker/analyzer \ - && make setup + && OPAMWITHTEST=true make setup RUN cd /home/opam/docker/analyzer \ && eval $(opam env) \ From 26b52dbf8fcdce912e56d4deae05eaf3db03fa64 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 20 May 2026 17:47:14 +0300 Subject: [PATCH 18/18] Revert "Use prebuilt ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial image for devcontainer" This reverts commit 7f5278113d5fbe9a369c8111af0c1ad01bc6ee67. --- .devcontainer/devcontainer.json | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 8938b12b7a..aaceb9b08e 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -3,11 +3,10 @@ { "name": "Goblint", - // "build": { - // "dockerfile": "./Dockerfile", - // "context": ".." - // }, - "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", + "build": { + "dockerfile": "./Dockerfile", + "context": ".." + }, "remoteUser": "opam", "postCreateCommand": "if [ -e _opam ] && [ ! -L _opam ]; then echo 'ERROR: _opam already exists and is not a symlink. Delete it manually on the host and rebuild the container.' >&2; exit 1; elif [ ! -e _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi",