diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 1d8778e5e5..85113c3547 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,9 @@ 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 \ + && eval $(opam env) \ + && opam install -y utop ocaml-lsp-server ocp-indent \ + && sudo gem install parallel diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 2bf28b3c6f..e054c51857 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -3,12 +3,13 @@ { "name": "Goblint", - "build": { - "dockerfile": "./Dockerfile", - "context": ".." - }, + // "build": { + // "dockerfile": "./Dockerfile", + // "context": ".." + // }, + "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", "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? 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 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 diff --git a/src/analyses/tutorials/gStoreWidening.ml b/src/analyses/tutorials/gStoreWidening.ml new file mode 100644 index 0000000000..8990590e5b --- /dev/null +++ b/src/analyses/tutorials/gStoreWidening.ml @@ -0,0 +1,301 @@ +open GoblintCil +open SimplifiedAnalysis +open GStoreWideningHelper + +(** + 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). + + 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` + + 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 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. + + 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.) + +*) + + +module GStoreWideningAnalysis: 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 get 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 + + + (* 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 + | _ -> 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 + +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 = + (* 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 *) + 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 GStoreWideningAnalysis:SimplifiedSpec); + MCPRegistry.registered_simplified_analysis (module EffectivelyLocalAnalysis: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..3252e1f499 --- /dev/null +++ b/src/analyses/tutorials/gStoreWideningSol.ml @@ -0,0 +1,260 @@ +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. ** + ********************************************************************************************************************** +*) + + +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 && 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 + + (* 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)); + if man.ask (Queries.TutorialEffectivelyLocal v) then + D.add v (cast_to_typ v.vtype (eval man state rval)) state + else + 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 + +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 EffectivelyLocalAnalysis:SimplifiedSpec) 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) = 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/dune b/src/dune index deba41c852..5ba19c6f78 100644 --- a/src/dune +++ b/src/dune @@ -6,7 +6,7 @@ (library (name goblint_lib) (public_name goblint.lib) - (modules :standard \ goblint goblint_memtrace privPrecCompare apronPrecCompare messagesCompare) + (modules :standard \ goblint_memtrace goblint privPrecCompare apronPrecCompare messagesCompare) (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. diff --git a/src/framework/simplifiedAnalysis.ml b/src/framework/simplifiedAnalysis.ml new file mode 100644 index 0000000000..3b716371c3 --- /dev/null +++ b/src/framework/simplifiedAnalysis.ml @@ -0,0 +1,74 @@ +open GoblintCil + + +(** 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 + } + +(** 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 + + 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 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 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..b68036ea1d --- /dev/null +++ b/tests/regression/99-tutorials/05-gstore-zero.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated '["gStoreWidening","assert","escape"]' +#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..397471ed8e --- /dev/null +++ b/tests/regression/99-tutorials/06-gstore-thread.c @@ -0,0 +1,43 @@ +// 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 +int global = 0; + +void* thread(void* arg) { + + if(global < 0) { + global = -58; + } else { + global = 1; + } + + return NULL; +} + +int main() { + global = 0; + 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; +} 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; +}