diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json new file mode 100644 index 0000000000..d1b4171b2b --- /dev/null +++ b/conf/svcomp-ghost.json @@ -0,0 +1,139 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "mutexGhosts", + "pthreadMutexType" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + }, + "invariant": { + "local": false, + "global": true + } + }, + "relation": { + "invariant": { + "local": false, + "global": true, + "one-var": false + } + }, + "apron": { + "invariant": { + "diff-box": true + } + }, + "var_eq": { + "invariant": { + "enabled": false + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": false + }, + "yaml": { + "enabled": true, + "format-version": "2.1", + "entry-types": [ + "flow_insensitive_invariant", + "ghost_instrumentation" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true, + "accessed": false, + "exact": true, + "all-locals": false, + "flow_insensitive-as": "invariant_set-location_invariant" + } + }, + "pre": { + "enabled": false + } +} diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py index ba25a1403c..ef1729b65e 100755 --- a/scripts/goblint-lib-modules.py +++ b/scripts/goblint-lib-modules.py @@ -48,6 +48,7 @@ "MessageCategory", # included in Messages "PreValueDomain", # included in ValueDomain + "WitnessGhostVar", # included in WitnessGhost "ConfigVersion", "ConfigProfile", diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 28e365bd97..df3cf545c5 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -634,6 +634,15 @@ struct ) |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none + let query_invariant_global ctx g = + if GobConfig.get_bool "ana.relation.invariant.global" && ctx.ask (GhostVarAvailable Multithreaded) then ( + let var = WitnessGhost.to_varinfo Multithreaded in + let inv = Priv.invariant_global (Analyses.ask_of_ctx ctx) ctx.global g in + Invariant.(of_exp (UnOp (LNot, Lval (GoblintCil.var var), GoblintCil.intType)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) + else + Invariant.none + let query ctx (type a) (q: a Queries.t): a Queries.result = let open Queries in let st = ctx.local in @@ -655,6 +664,9 @@ struct let vf' x = vf (Obj.repr x) in Priv.iter_sys_vars ctx.global vq vf' | Queries.Invariant context -> query_invariant ctx context + | Queries.InvariantGlobal g -> + let g: V.t = Obj.obj g in + query_invariant_global ctx g | _ -> Result.top q diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 15df394d54..257bec24d8 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -46,6 +46,9 @@ module type S = val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> relation_components_t -> relation_components_t val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *) + val invariant_global: Q.ask -> (V.t -> G.t) -> V.t -> Invariant.t + (** Returns flow-insensitive invariant for global unknown. *) + val invariant_vars: Q.ask -> (V.t -> G.t) -> relation_components_t -> varinfo list (** Returns global variables which are privatized. *) @@ -137,6 +140,7 @@ struct {rel = RD.top (); priv = startstate ()} let iter_sys_vars getg vq vf = () + let invariant_global ask getg g = Invariant.none let invariant_vars ask getg st = [] let init () = () @@ -424,6 +428,7 @@ struct {rel = getg (); priv = startstate ()} let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *) + let invariant_global ask getg g = Invariant.none let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *) let finalize () = () @@ -708,6 +713,41 @@ struct let init () = () let finalize () = () + + let invariant_global (ask: Q.ask) (getg: V.t -> G.t): V.t -> Invariant.t = function + | `Left m' -> (* mutex *) + let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in + if atomic || ask.f (GhostVarAvailable (Locked m')) then ( + (* filters like query_invariant *) + let one_var = GobConfig.get_bool "ana.relation.invariant.one-var" in + let exact = GobConfig.get_bool "witness.invariant.exact" in + + let rel = keep_only_protected_globals ask m' (get_m_with_mutex_inits ask getg m') in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *) + let inv = + RD.invariant rel + |> List.enum + |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) -> + (* filter one-vars and exact *) + (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *) + if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then + RD.cil_exp_of_lincons1 lincons1 + |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp)) + else + None + ) + |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none + in + if atomic then + inv + else ( + let var = WitnessGhost.to_varinfo (Locked m') in + Invariant.(of_exp (Lval (GoblintCil.var var)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) + ) + else + Invariant.none + | g -> (* global *) + Invariant.none (* Could output unprotected one-variable (so non-relational) invariants, but probably not very useful. [BasePriv] does those anyway. *) end (** May written variables. *) @@ -1275,6 +1315,8 @@ struct | _ -> () let finalize () = () + + let invariant_global ask getg g = Invariant.none end module TracingPriv = functor (Priv: S) -> functor (RD: RelationDomain.RD) -> diff --git a/src/analyses/base.ml b/src/analyses/base.ml index cc0269d648..f6e41361a3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1181,6 +1181,9 @@ struct not is_alloc || (is_alloc && not (ctx.ask (Queries.IsHeapVar v))) let query_invariant ctx context = + let keep_local = GobConfig.get_bool "ana.base.invariant.local" in + let keep_global = GobConfig.get_bool "ana.base.invariant.global" in + let cpa = ctx.local.BaseDomain.cpa in let ask = Analyses.ask_of_ctx ctx in @@ -1193,6 +1196,13 @@ struct in let module I = ValueDomain.ValueInvariant (Arg) in + let var_filter v = + if is_global ask v then + keep_global + else + keep_local + in + let var_invariant ?offset v = if not (InvariantCil.var_is_heap v) then I.key_invariant v ?offset (Arg.find v) @@ -1203,14 +1213,23 @@ struct if Lval.Set.is_top context.Invariant.lvals then ( if !earlyglobs || ThreadFlag.has_ever_been_multi ask then ( let cpa_invariant = - CPA.fold (fun k v a -> - if not (is_global ask k) then - Invariant.(a && var_invariant k) - else - a - ) cpa Invariant.none + if keep_local then ( + CPA.fold (fun k v a -> + if not (is_global ask k) then + Invariant.(a && var_invariant k) + else + a + ) cpa Invariant.none + ) + else + Invariant.none + in + let priv_vars = + if keep_global then + Priv.invariant_vars ask (priv_getg ctx.global) ctx.local + else + [] in - let priv_vars = Priv.invariant_vars ask (priv_getg ctx.global) ctx.local in let priv_invariant = List.fold_left (fun acc v -> Invariant.(var_invariant v && acc) @@ -1220,7 +1239,10 @@ struct ) else ( CPA.fold (fun k v a -> - Invariant.(a && var_invariant k) + if var_filter k then + Invariant.(a && var_invariant k) + else + a ) cpa Invariant.none ) ) @@ -1228,7 +1250,7 @@ struct Lval.Set.fold (fun k a -> let i = match k with - | (Var v, offset) when not (InvariantCil.var_is_heap v) -> + | (Var v, offset) when var_filter v && not (InvariantCil.var_is_heap v) -> (try I.key_invariant_lval v ~offset ~lval:k (Arg.find v) with Not_found -> Invariant.none) | _ -> Invariant.none in @@ -1243,13 +1265,23 @@ struct Invariant.none let query_invariant_global ctx g = - if GobConfig.get_bool "ana.base.invariant.enabled" && get_bool "exp.earlyglobs" then ( + if GobConfig.get_bool "ana.base.invariant.enabled" && GobConfig.get_bool "ana.base.invariant.global" then ( (* Currently these global invariants are only sound with earlyglobs enabled for both single- and multi-threaded programs. - Otherwise, the values of globals in single-threaded mode are not accounted for. *) - (* TODO: account for single-threaded values without earlyglobs. *) + Otherwise, the values of globals in single-threaded mode are not accounted for. + They are also made sound without earlyglobs using the multithreaded mode ghost variable. *) match g with | `Left g' -> (* priv *) - Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g' + let inv = Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g' in + if get_bool "exp.earlyglobs" then + inv + else ( + if ctx.ask (GhostVarAvailable Multithreaded) then ( + let var = WitnessGhost.to_varinfo Multithreaded in + Invariant.(of_exp (UnOp (LNot, Lval (GoblintCil.var var), GoblintCil.intType)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) + else + Invariant.none + ) | `Right _ -> (* thread return *) Invariant.none ) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index e69757c7a8..3afd758daa 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -250,7 +250,7 @@ struct let invariant_global ask getg = function | `Right g' -> (* global *) - ValueDomain.invariant_global (read_unprotected_global getg) g' + ValueDomain.invariant_global (read_unprotected_global getg) g' (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *) | _ -> (* mutex *) Invariant.none @@ -339,6 +339,31 @@ module PerMutexMeetPrivBase = struct include PerMutexPrivBase + let invariant_global (ask: Q.ask) getg = function + | `Left m' -> (* mutex *) + let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in + if atomic || ask.f (GhostVarAvailable (Locked m')) then ( + let cpa = get_m_with_mutex_inits ask getg m' in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *) + let inv = CPA.fold (fun v _ acc -> + if ask.f (MustBeProtectedBy {mutex = m'; global = v; write = true; protection = Strong}) then + let inv = ValueDomain.invariant_global (fun g -> CPA.find g cpa) v in + Invariant.(acc && inv) + else + acc + ) cpa Invariant.none + in + if atomic then + inv + else ( + let var = WitnessGhost.to_varinfo (Locked m') in + Invariant.(of_exp (Lval (GoblintCil.var var)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) + ) + else + Invariant.none + | g -> (* global *) + invariant_global ask getg g + let invariant_vars ask getg (st: _ BaseDomain.basecomponents_t) = (* Mutex-meet local states contain precisely the protected global variables, so we can do fewer queries than {!protected_vars}. *) @@ -374,8 +399,11 @@ struct in if not invariant then ( if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; - sideg (V.global x) (CPA.singleton x v) - (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write. *) + let side_cpa = CPA.singleton x v in + sideg (V.global x) side_cpa; + if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then + sideg V.mutex_inits side_cpa (* Also side to inits because with earlyglobs enter_multithreaded does not side everything to inits *) + (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write. *) ); {st with cpa = cpa'} (* let write_global ask getg sideg cpa x v = @@ -676,7 +704,7 @@ struct let invariant_global ask getg = function | `Middle g -> (* global *) - ValueDomain.invariant_global (read_unprotected_global getg) g + ValueDomain.invariant_global (read_unprotected_global getg) g (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *) | `Left _ | `Right _ -> (* mutex or thread *) Invariant.none @@ -749,8 +777,8 @@ struct if not invariant then ( if not (Param.handle_atomic && ask.f MustBeAtomic) then sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *) - if !earlyglobs then (* earlyglobs workaround for 13/60 *) - sideg (V.protected x) v + if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then (* earlyglobs workaround for 13/60 *) + sideg (V.protected x) v (* Also side to protected because with earlyglobs enter_multithreaded does not side everything to protected *) (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *) ); if Param.handle_atomic && ask.f MustBeAtomic then @@ -851,13 +879,37 @@ struct vf (V.protected g); | _ -> () - let invariant_global ask getg g = + let invariant_global (ask: Q.ask) getg g = let getg = Wrapper.getg ask getg in match g with | `Left g' -> (* unprotected *) ValueDomain.invariant_global (fun g -> getg (V.unprotected g)) g' - | `Right g -> (* protected *) - Invariant.none + | `Right g' -> (* protected *) + let locks = ask.f (Q.MustProtectingLocks g') in + if LockDomain.MustLockset.is_all locks || LockDomain.MustLockset.is_empty locks then + Invariant.none + else if VD.equal (getg (V.protected g')) (getg (V.unprotected g')) then + Invariant.none (* don't output protected invariant because it's the same as unprotected *) + else ( + (* Only read g' as protected, everything else (e.g. pointed to variables) may be unprotected. + See 56-witness/69-ghost-ptr-protection and https://github.com/goblint/analyzer/pull/1394#discussion_r1698136411. *) + let read_global g = getg (if CilType.Varinfo.equal g g' then V.protected g else V.unprotected g) in + let inv = ValueDomain.invariant_global read_global g' in + (* Very conservative about multiple (write-)protecting mutexes: invariant is not claimed when any of them is held. + It should be possible to be more precise because writes only happen with all of them held, + but conjunction is unsound when one of the mutexes is temporarily unlocked. + Hypothetical read-protection is also somehow relevant. *) + LockDomain.MustLockset.fold (fun m acc -> + if LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) then + acc + else if ask.f (GhostVarAvailable (Locked m)) then ( + let var = WitnessGhost.to_varinfo (Locked m) in + Invariant.(of_exp (Lval (GoblintCil.var var)) || acc) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) + ) + else + Invariant.none + ) locks inv + ) let invariant_vars ask getg st = protected_vars ask end @@ -998,7 +1050,7 @@ struct (* sync: M -> (2^M -> (G -> D)) *) include AbstractLockCenteredBase (ThreadMap) (LockCenteredBase.CPA) - let global_init_thread = RichVarinfo.single ~name:"global_init" + let global_init_thread = RichVarinfo.single ~name:"global_init" ~typ:GoblintCil.voidType let current_thread (ask: Q.ask): Thread.t = if !AnalysisState.global_initialization then ThreadIdDomain.Thread.threadinit (global_init_thread ()) ~multiple:false @@ -1902,6 +1954,17 @@ struct if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; r + let invariant_global ask getg g = + if M.tracing then M.traceli "priv" "invariant_global %a" V.pretty g; + let getg x = + let r = getg x in + if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + r + in + let r = invariant_global ask getg g in + if M.tracing then M.traceu "priv" "-> %a" Invariant.pretty r; + r + end let priv_module: (module S) Lazy.t = diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 742e796fbd..f2f36b1360 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -303,6 +303,10 @@ struct (* InvariantGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *) let (n, g): V.t = Obj.obj g in f ~q:(InvariantGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local) + | Queries.YamlEntryGlobal (g, task) -> + (* YamlEntryGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *) + let (n, g): V.t = Obj.obj g in + f ~q:(YamlEntryGlobal (Obj.repr g, task)) (Result.top ()) (n, spec n, assoc n ctx.local) | Queries.PartAccess a -> Obj.repr (access ctx a) | Queries.IterSysVars (vq, fi) -> diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9b6aa4f4ca..bb50c96432 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -223,6 +223,8 @@ struct true else *) MustLockset.mem ml protecting + | Queries.MustProtectingLocks g -> + protecting ~write:true Strong g | Queries.MustLockset -> let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in held_locks diff --git a/src/analyses/mutexGhosts.ml b/src/analyses/mutexGhosts.ml new file mode 100644 index 0000000000..3deec3ef59 --- /dev/null +++ b/src/analyses/mutexGhosts.ml @@ -0,0 +1,191 @@ +(** Analysis for generating ghost variables corresponding to mutexes ([mutexGhosts]). *) + +open Analyses + +module NodeSet = Queries.NS + + +module Spec = +struct + include UnitAnalysis.Spec + let name () = "mutexGhosts" + + module V = + struct + include Printable.Either3 (Node) (LockDomain.MustLock) (BoolDomain.Bool) + let node x = `Left x + let lock x = `Middle x + let threadcreate = `Right false + let update = `Right true + let is_write_only = function + | `Left _ -> false + | `Middle _ -> true + | `Right false -> false + | `Right true -> true + end + + module Locked = + struct + include LockDomain.MayLocksetNoRW + let name () = "locked" + end + module Unlocked = + struct + include LockDomain.MayLocksetNoRW + let name () = "unlocked" + end + module MultiThread = + struct + include BoolDomain.MayBool + let name () = "multithread" + end + module G = + struct + include Lattice.Lift2 (Lattice.Prod3 (Locked) (Unlocked) (MultiThread)) (Lattice.Lift2 (BoolDomain.MayBool) (NodeSet)) + let node = function + | `Bot -> (Locked.bot (), Unlocked.bot (), MultiThread.bot ()) + | `Lifted1 x -> x + | _ -> failwith "MutexGhosts.node" + let lock = function + | `Bot -> BoolDomain.MayBool.bot () + | `Lifted2 (`Lifted1 x) -> x + | _ -> failwith "MutexGhosts.lock" + let threadcreate = function + | `Bot -> NodeSet.bot () + | `Lifted2 (`Lifted2 x) -> x + | _ -> failwith "MutexGhosts.threadcreate" + let update = threadcreate + let create_node node = `Lifted1 node + let create_lock lock = `Lifted2 (`Lifted1 lock) + let create_threadcreate threadcreate = `Lifted2 (`Lifted2 threadcreate) + let create_update = create_threadcreate + end + + let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option = + match addr with + | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) + | _ -> None + + let event ctx e octx = + let verifier_atomic_addr = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var in + begin match e with + | Events.Lock (l, _) when not (LockDomain.Addr.equal l verifier_atomic_addr) -> + ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.singleton l, Unlocked.bot (), MultiThread.bot ())); + if !AnalysisState.postsolving then ( + ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node)); + let (locked, _, _) = G.node (ctx.global (V.node ctx.prev_node)) in + if Locked.cardinal locked > 1 then ( + Locked.iter (fun lock -> + Option.iter (fun lock -> + ctx.sideg (V.lock lock) (G.create_lock true) + ) (mustlock_of_addr lock) + ) locked + ); + ) + | Events.Unlock l when not (LockDomain.Addr.equal l verifier_atomic_addr) -> + ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.bot (), Unlocked.singleton l, MultiThread.bot ())); + if !AnalysisState.postsolving then ( + ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node)); + let (_, unlocked, _) = G.node (ctx.global (V.node ctx.prev_node)) in + if Locked.cardinal unlocked > 1 then ( + Locked.iter (fun lock -> + Option.iter (fun lock -> + ctx.sideg (V.lock lock) (G.create_lock true) + ) (mustlock_of_addr lock) + ) unlocked + ); + ) + | Events.EnterMultiThreaded -> + ctx.sideg (V.node ctx.prev_node) (G.create_node (Locked.bot (), Unlocked.bot (), true)); + if !AnalysisState.postsolving then + ctx.sideg V.update (G.create_update (NodeSet.singleton ctx.prev_node)); + | _ -> () + end; + ctx.local + + let threadspawn ctx ~multiple lval f args octx = + ctx.sideg V.threadcreate (G.create_threadcreate (NodeSet.singleton ctx.node)); + ctx.local + + let ghost_var_available ctx = function + | WitnessGhost.Var.Locked ((v, o) as lock) -> not (Offset.Z.contains_index o) && not (G.lock (ctx.global (V.lock lock))) + | Multithreaded -> true + + let ghost_var_available ctx v = + WitnessGhost.enabled () && ghost_var_available ctx v + + module VariableSet = Set.Make (YamlWitnessType.GhostInstrumentation.Variable) + + let query ctx (type a) (q: a Queries.t): a Queries.result = + match q with + | GhostVarAvailable v -> ghost_var_available ctx v + | YamlEntryGlobal (g, task) -> + let g: V.t = Obj.obj g in + begin match g with + | `Right true when YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type -> + let nodes = G.update (ctx.global g) in + let (variables, location_updates) = NodeSet.fold (fun node (variables, location_updates) -> + let (locked, unlocked, multithread) = G.node (ctx.global (V.node node)) in + let variables' = + Locked.fold (fun l acc -> + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> + let variable = WitnessGhost.variable' (Locked l) in + VariableSet.add variable acc + | _ -> + acc + ) (Locked.union locked unlocked) variables + in + let updates = + Locked.fold (fun l acc -> + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> + let update = WitnessGhost.update' (Locked l) GoblintCil.one in + update :: acc + | _ -> + acc + ) locked [] + in + let updates = + Unlocked.fold (fun l acc -> + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> + let update = WitnessGhost.update' (Locked l) GoblintCil.zero in + update :: acc + | _ -> + acc + ) unlocked updates + in + let (variables', updates) = + if not (GobConfig.get_bool "exp.earlyglobs") && multithread then ( + if ghost_var_available ctx Multithreaded then ( + let variable = WitnessGhost.variable' Multithreaded in + let update = WitnessGhost.update' Multithreaded GoblintCil.one in + let variables' = VariableSet.add variable variables' in + (variables', update :: updates) + ) + else + (variables', updates) + ) + else + (variables', updates) + in + match updates with + | [] -> (variables', location_updates) (* don't add location_update with no updates *) + | _ -> + let location_update = WitnessGhost.location_update' ~node ~updates in + (variables', location_update :: location_updates) + ) nodes (VariableSet.empty, []) + in + let entry = WitnessGhost.instrumentation_entry ~task ~variables:(VariableSet.elements variables) ~location_updates in + Queries.YS.singleton entry + | `Left _ -> Queries.Result.top q + | `Middle _ -> Queries.Result.top q + | `Right _ -> Queries.Result.top q + end + | InvariantGlobalNodes -> (G.threadcreate (ctx.global V.threadcreate): NodeSet.t) + | _ -> Queries.Result.top q +end + +let _ = + MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 707e0f4820..1b430e651a 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -239,13 +239,13 @@ struct | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> M.info_noloc ~category:Witness "disabled entry of type %s" target_type | _ -> - M.info_noloc ~category:Witness "cannot unassume entry of type %s" target_type + M.warn_noloc ~category:Witness "cannot unassume entry of type %s" target_type in List.iter (fun yaml_entry -> match YamlWitnessType.Entry.of_yaml yaml_entry with | Ok entry -> unassume_entry entry - | Error (`Msg e) -> M.info_noloc ~category:Witness "couldn't parse entry: %s" e + | Error (`Msg e) -> M.error_noloc ~category:Witness "couldn't parse entry: %s" e ) yaml_entries let emit_unassume ctx = diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 78013ec21d..b220afc0d9 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -562,7 +562,7 @@ struct let r = eq_set_clos e ctx.local in if M.tracing then M.tracel "var_eq" "equalset %a = %a" d_plainexp e Queries.ES.pretty r; r - | Queries.Invariant context when GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *) + | Queries.Invariant context when GobConfig.get_bool "ana.var_eq.invariant.enabled" && GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *) let scope = Node.find_fundec ctx.node in D.invariant ~scope ctx.local | _ -> Queries.Result.top x diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index eb9ec6ce02..32ca234e70 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -144,6 +144,8 @@ module MallocWrapper : MCPSpec = struct Format.dprintf "@tid:%s" (ThreadLifted.show t) in Format.asprintf "(alloc@sid:%s%t%t)" (Node.show_id node) tid uniq_count + + let typ _ = GoblintCil.voidType end module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index f9f4b06ffb..b126d712bf 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -133,7 +133,7 @@ struct | _ -> false let is_mutex_type (t: typ): bool = match t with - | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" + | TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" || info.tname = "pthread_rwlock_t" | TInt (IInt, attr) -> hasAttribute "mutex" attr | _ -> false diff --git a/src/common/util/richVarinfo.ml b/src/common/util/richVarinfo.ml index d1918c40a6..6a27339eed 100644 --- a/src/common/util/richVarinfo.ml +++ b/src/common/util/richVarinfo.ml @@ -1,9 +1,9 @@ open GoblintCil -let create_var name = Cilfacade.create_var @@ makeGlobalVar name voidType +let create_var name typ = Cilfacade.create_var @@ makeGlobalVar name typ -let single ~name = - let vi = lazy (create_var name) in +let single ~name ~typ = + let vi = lazy (create_var name typ) in fun () -> Lazy.force vi @@ -21,6 +21,7 @@ module type G = sig include Hashtbl.HashedType val name_varinfo: t -> string + val typ: t -> typ end module type H = @@ -47,7 +48,7 @@ struct try XH.find !xh x with Not_found -> - let vi = create_var (X.name_varinfo x) in + let vi = create_var (X.name_varinfo x) (X.typ x) in store_f x vi; vi diff --git a/src/common/util/richVarinfo.mli b/src/common/util/richVarinfo.mli index 4e682734ee..d1c002bf84 100644 --- a/src/common/util/richVarinfo.mli +++ b/src/common/util/richVarinfo.mli @@ -2,7 +2,7 @@ open GoblintCil -val single: name:string -> (unit -> varinfo) +val single: name:string -> typ:typ -> (unit -> varinfo) module type VarinfoMap = sig @@ -18,6 +18,7 @@ module type G = sig include Hashtbl.HashedType val name_varinfo: t -> string + val typ: t -> typ end module type H = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 12edb5bcec..43e2ad1d59 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -797,6 +797,18 @@ "type": "boolean", "default": true }, + "local": { + "title": "ana.base.invariant.local", + "description": "Keep local variables in invariants", + "type": "boolean", + "default": true + }, + "global": { + "title": "ana.base.invariant.global", + "description": "Keep global variables in invariants", + "type": "boolean", + "default": true + }, "blobs": { "title": "ana.base.invariant.blobs", "description": "Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.", @@ -1166,6 +1178,26 @@ } }, "additionalProperties": false + }, + "var_eq": { + "title": "ana.var_eq", + "type": "object", + "properties": { + "invariant": { + "title": "ana.var_eq.invariant", + "type": "object", + "properties": { + "enabled": { + "title": "ana.var_eq.invariant.enabled", + "description": "Generate var_eq analysis invariants", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false } }, "additionalProperties": false @@ -2594,6 +2626,13 @@ "description": "Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.", "type": "boolean", "default": true + }, + "flow_insensitive-as": { + "title": "witness.invariant.flow_insensitive-as", + "description": "Emit flow-insensitive invariants as location invariants at certain locations.", + "type": "string", + "enum": ["flow_insensitive_invariant", "location_invariant", "invariant_set-location_invariant"], + "default": "flow_insensitive_invariant" } }, "additionalProperties": false @@ -2614,7 +2653,8 @@ "type": "string", "enum": [ "0.1", - "2.0" + "2.0", + "2.1" ], "default": "0.1" }, @@ -2632,7 +2672,8 @@ "loop_invariant_certificate", "precondition_loop_invariant_certificate", "invariant_set", - "violation_sequence" + "violation_sequence", + "ghost_instrumentation" ] }, "default": [ diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b0ede0cfbf..fee44a6b24 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -10,6 +10,7 @@ module LS = VDQ.LS module TS = SetDomain.ToppedSet (CilType.Typ) (struct let topname = "All" end) module ES = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Exp) (struct let topname = "All" end)) module VS = SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All" end) +module NS = SetDomain.ToppedSet (Node) (struct let topname = "All" end) module NFL = WrapperFunctionAnalysis0.NodeFlatLattice module TC = WrapperFunctionAnalysis0.ThreadCreateUniqueCount @@ -62,6 +63,8 @@ type invariant_context = Invariant.context = { } [@@deriving ord, hash] +module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end) + (** GADT for queries with specific result type. *) type _ t = @@ -114,6 +117,7 @@ type _ t = | MustJoinedThreads: ConcDomain.MustThreadSet.t t | ThreadsJoinedCleanly: MustBool.t t | MustProtectedVars: mustprotectedvars -> VS.t t + | MustProtectingLocks: CilType.Varinfo.t -> LockDomain.MustLockset.t t | Invariant: invariant_context -> Invariant.t t | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *) | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *) @@ -127,6 +131,9 @@ type _ t = | TmpSpecial: Mval.Exp.t -> ML.t t | MaySignedOverflow: exp -> MayBool.t t | GasExhausted: CilType.Fundec.t -> MustBool.t t + | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *) + | 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. *) type 'a result = 'a @@ -185,6 +192,7 @@ struct | MustJoinedThreads -> (module ConcDomain.MustThreadSet) | ThreadsJoinedCleanly -> (module MustBool) | MustProtectedVars _ -> (module VS) + | MustProtectingLocks _ -> (module LockDomain.MustLockset) | Invariant _ -> (module Invariant) | InvariantGlobal _ -> (module Invariant) | WarnGlobal _ -> (module Unit) @@ -198,6 +206,9 @@ struct | TmpSpecial _ -> (module ML) | MaySignedOverflow _ -> (module MayBool) | GasExhausted _ -> (module MustBool) + | YamlEntryGlobal _ -> (module YS) + | GhostVarAvailable _ -> (module MayBool) + | InvariantGlobalNodes -> (module NS) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -255,6 +266,7 @@ struct | MustJoinedThreads -> ConcDomain.MustThreadSet.top () | ThreadsJoinedCleanly -> MustBool.top () | MustProtectedVars _ -> VS.top () + | MustProtectingLocks _ -> LockDomain.MustLockset.top () | Invariant _ -> Invariant.top () | InvariantGlobal _ -> Invariant.top () | WarnGlobal _ -> Unit.top () @@ -268,6 +280,9 @@ struct | TmpSpecial _ -> ML.top () | MaySignedOverflow _ -> MayBool.top () | GasExhausted _ -> MustBool.top () + | YamlEntryGlobal _ -> YS.top () + | GhostVarAvailable _ -> MayBool.top () + | InvariantGlobalNodes -> NS.top () end (* The type any_query can't be directly defined in Any as t, @@ -335,6 +350,10 @@ struct | Any (IsAllocVar _) -> 57 | Any (MaySignedOverflow _) -> 58 | Any (GasExhausted _) -> 59 + | Any (YamlEntryGlobal _) -> 60 + | Any (MustProtectingLocks _) -> 61 + | Any (GhostVarAvailable _) -> 62 + | Any InvariantGlobalNodes -> 63 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -382,14 +401,17 @@ struct | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) | Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2 | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) + | Any (YamlEntryGlobal (vi1, task1)), Any (YamlEntryGlobal (vi2, task2)) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) (* TODO: compare task *) | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *) | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2 | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2 + | Any (MustProtectingLocks g1), Any (MustProtectingLocks g2) -> CilType.Varinfo.compare g1 g2 | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2 | Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2 | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2 | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2 | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2 + | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2 (* only argumentless queries should remain *) | _, _ -> Stdlib.compare (order a) (order b) @@ -427,12 +449,15 @@ struct | Any (Invariant i) -> hash_invariant_context i | Any (MutexType m) -> Mval.Unit.hash m | Any (InvariantGlobal vi) -> Hashtbl.hash vi + | Any (YamlEntryGlobal (vi, task)) -> Hashtbl.hash vi (* TODO: hash task *) | Any (MustProtectedVars m) -> hash_mustprotectedvars m + | Any (MustProtectingLocks g) -> CilType.Varinfo.hash g | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start | Any (TmpSpecial lv) -> Mval.Exp.hash lv | Any (MaySignedOverflow e) -> CilType.Exp.hash e | Any (GasExhausted f) -> CilType.Fundec.hash f + | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) @@ -481,10 +506,12 @@ struct | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads" | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly" | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _" + | Any (MustProtectingLocks g) -> Pretty.dprintf "MustProtectingLocks _" | Any (Invariant i) -> Pretty.dprintf "Invariant _" | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _" | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _" | Any (InvariantGlobal i) -> Pretty.dprintf "InvariantGlobal _" + | Any (YamlEntryGlobal (i, task)) -> Pretty.dprintf "YamlEntryGlobal _" | Any (MutexType (v,o)) -> Pretty.dprintf "MutexType _" | Any (EvalMutexAttr a) -> Pretty.dprintf "EvalMutexAttr _" | Any MayAccessed -> Pretty.dprintf "MayAccessed" @@ -497,6 +524,8 @@ struct | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f + | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v + | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" end let to_value_domain_ask (ask: ask) = diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index d8fd408151..415fb21605 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -109,6 +109,7 @@ module MutexAnalysis = MutexAnalysis module MayLocks = MayLocks module SymbLocks = SymbLocks module Deadlock = Deadlock +module MutexGhosts = MutexGhosts (** {3 Threads} @@ -351,6 +352,7 @@ module Graphml = Graphml module YamlWitness = YamlWitness module YamlWitnessType = YamlWitnessType +module WitnessGhost = WitnessGhost (** {3 Violation} diff --git a/src/lifters/longjmpLifter.ml b/src/lifters/longjmpLifter.ml index 1a28085abe..a093f8c703 100644 --- a/src/lifters/longjmpLifter.ml +++ b/src/lifters/longjmpLifter.ml @@ -66,6 +66,14 @@ struct | _ -> Queries.Result.top q end + | YamlEntryGlobal (g, task) -> + let g: V.t = Obj.obj g in + begin match g with + | `Left g -> + S.query (conv ctx) (YamlEntryGlobal (Obj.repr g, task)) + | _ -> + Queries.Result.top q + end | IterSysVars (vq, vf) -> (* vars for S *) let vf' x = vf (Obj.repr (V.s (Obj.obj x))) in diff --git a/src/lifters/recursionTermLifter.ml b/src/lifters/recursionTermLifter.ml index 2d9f45de60..37522305b9 100644 --- a/src/lifters/recursionTermLifter.ml +++ b/src/lifters/recursionTermLifter.ml @@ -106,6 +106,14 @@ struct | `Right v -> Queries.Result.top q end + | YamlEntryGlobal (v, task) -> + let v: V.t = Obj.obj v in + begin match v with + | `Left v -> + S.query (conv ctx) (YamlEntryGlobal (Obj.repr v, task)) + | `Right v -> + Queries.Result.top q + end | _ -> S.query (conv ctx) q let branch ctx = S.branch (conv ctx) diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml index e8292bedc0..39c7799395 100644 --- a/src/lifters/specLifters.ml +++ b/src/lifters/specLifters.ml @@ -737,6 +737,14 @@ struct | `Right g -> Queries.Result.top q end + | YamlEntryGlobal (g, task) -> + let g: V.t = Obj.obj g in + begin match g with + | `Left g -> + S.query (conv ctx) (YamlEntryGlobal (Obj.repr g, task)) + | `Right g -> + Queries.Result.top q + end | IterSysVars (vq, vf) -> (* vars for S *) let vf' x = vf (Obj.repr (V.s (Obj.obj x))) in diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 76c09c36a2..6643b58eef 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1097,6 +1097,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__VERIFIER_nondet_int", unknown []); (* declare invalidate actions to prevent invalidating globals when extern in regression tests *) ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ("__VERIFIER_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if definition missing (e.g. in evalAssert transformed output) or extraspecial *) + ("reach_error", special [] @@ Abort); (* only used if definition missing (e.g. in evalAssert transformed output) or extraspecial *) ] [@@coverage off] diff --git a/src/witness/witnessGhost.ml b/src/witness/witnessGhost.ml new file mode 100644 index 0000000000..3eaa8ef69b --- /dev/null +++ b/src/witness/witnessGhost.ml @@ -0,0 +1,32 @@ +(** Ghost variables for YAML witnesses. *) + +let enabled () = + YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type + +module Var = WitnessGhostVar + +include Var + +module Map = RichVarinfo.BiVarinfoMap.Make (Var) + +include Map + +let variable' x = + let variable = name_varinfo x in + let type_ = String.trim (CilType.Typ.show (typ x)) in (* CIL printer puts space at the end of some types *) + let initial = CilType.Exp.show (initial x) in + YamlWitness.Entry.ghost_variable' ~variable ~type_ ~initial + +let update' x e = + let variable = name_varinfo x in + let expression = CilType.Exp.show e in + YamlWitness.Entry.ghost_update' ~variable ~expression + +let location_update' ~node ~updates = + let loc = Node.location node in + let location_function = (Node.find_fundec node).svar.vname in + let location = YamlWitness.Entry.location ~location:loc ~location_function in + YamlWitness.Entry.ghost_location_update' ~location ~updates + +let instrumentation_entry ~task ~variables ~location_updates = + YamlWitness.Entry.ghost_instrumentation ~task ~variables ~location_updates diff --git a/src/witness/witnessGhostVar.ml b/src/witness/witnessGhostVar.ml new file mode 100644 index 0000000000..0d71909ba0 --- /dev/null +++ b/src/witness/witnessGhostVar.ml @@ -0,0 +1,43 @@ +(** Ghost variables for YAML witnesses. *) + +type t = + | Locked of LockDomain.MustLock.t + | Multithreaded +[@@deriving eq, ord, hash] + +let name_varinfo = function + | Locked (v, os) -> + let name = + if CilType.Varinfo.equal v LibraryFunctions.verifier_atomic_var then + invalid_arg "__VERIFIER_atomic" + else + if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo v then + Printf.sprintf "alloc_%s%d" (if v.vid < 0 then "m" else "") (abs v.vid) (* turn minus into valid C name *) + else + Basetype.Variables.show v + in + let rec offs: Offset.Z.t -> string = function + | `NoOffset -> "" + | `Field (f, os') -> "_" ^ f.fname ^ offs os' + | `Index (i, os') -> + assert Z.Compare.(i >= Z.zero); "_" ^ Z.to_string i + in + name ^ offs os ^ "_locked" + | Multithreaded -> "multithreaded" + +let show = name_varinfo + +include Printable.SimpleShow (struct + type nonrec t = t + let show = show + end) + +let describe_varinfo _ _ = "" + +let typ = function + | Locked _ + | Multithreaded -> GoblintCil.intType + +let initial = function + | Locked _ + | Multithreaded -> GoblintCil.zero diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 06e355068e..9d04b597fa 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -148,6 +148,35 @@ struct }; metadata = metadata (); } + + let ghost_variable' ~variable ~type_ ~(initial): GhostInstrumentation.Variable.t = { + name = variable; + scope = "global"; + type_; + initial = { + value = initial; + format = "c_expression"; + }; + } + + let ghost_update' ~variable ~(expression): GhostInstrumentation.Update.t = { + variable; + value = expression; + format = "c_expression"; + } + + let ghost_location_update' ~location ~(updates): GhostInstrumentation.LocationUpdate.t = { + location; + updates; + } + + let ghost_instrumentation ~task ~variables ~(location_updates): Entry.t = { + entry_type = GhostInstrumentation { + ghost_variables = variables; + ghost_updates = location_updates; + }; + metadata = metadata ~task (); + } end let yaml_entries_to_file yaml_entries file = @@ -317,14 +346,34 @@ struct entries in + let invariant_global_nodes = lazy (R.ask_global InvariantGlobalNodes) in + + let fold_flow_insensitive_as_location ~inv f acc = + (* Currently same invariants (from InvariantGlobal query) for all nodes (from InvariantGlobalNodes query). + The alternative would be querying InvariantGlobal per local unknown when looping over them to generate location invariants. + See: https://github.com/goblint/analyzer/pull/1394#discussion_r1698149514. *) + let invs = WitnessUtil.InvariantExp.process_exp inv in + Queries.NS.fold (fun n acc -> + let fundec = Node.find_fundec n in + match WitnessInvariant.location_location n with (* Not just using Node.location because it returns expression location which may be invalid for location invariant (e.g. inside conditional). *) + | Some loc -> + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in + List.fold_left (fun acc inv -> + f ~location ~inv acc + ) acc invs + | None -> acc + ) (Lazy.force invariant_global_nodes) acc + in + (* Generate flow-insensitive invariants *) let entries = if entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type then ( GHT.fold (fun g v acc -> match g with - | `Left g -> (* Spec global *) - begin match R.ask_global (InvariantGlobal (Obj.repr g)) with - | `Lifted inv -> + | `Left g -> (* global unknown from analysis Spec *) + begin match R.ask_global (InvariantGlobal (Obj.repr g)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with + | `Lifted inv, "flow_insensitive_invariant" -> let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> let invariant = Entry.invariant (CilType.Exp.show inv) in @@ -332,10 +381,18 @@ struct incr cnt_flow_insensitive_invariant; entry :: acc ) acc invs - | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) + | `Lifted inv, "location_invariant" -> + fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc -> + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.location_invariant ~task ~location ~invariant in + incr cnt_location_invariant; + entry :: acc + ) acc + | `Lifted _, _ + | `Bot, _ | `Top, _ -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) acc end - | `Right _ -> (* contexts global *) + | `Right _ -> (* global unknown for FromSpec contexts *) acc ) gh entries ) @@ -343,6 +400,33 @@ struct entries in + (* Generate flow-insensitive entries (ghost instrumentation) *) + let entries = + if entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type then ( + (* TODO: only at most one ghost_instrumentation entry can ever be produced, so this fold and deduplication is overkill *) + let module EntrySet = Queries.YS in + fst @@ GHT.fold (fun g v accs -> + match g with + | `Left g -> (* global unknown from analysis Spec *) + begin match R.ask_global (YamlEntryGlobal (Obj.repr g, task)) with + | `Lifted _ as inv -> + Queries.YS.fold (fun entry (acc, acc') -> + if EntrySet.mem entry acc' then (* deduplicate only with other global entries because local ones have different locations anyway *) + accs + else + (entry :: acc, EntrySet.add entry acc') + ) inv accs + | `Top -> + accs + end + | `Right _ -> (* global unknown for FromSpec contexts *) + accs + ) gh (entries, EntrySet.empty ()) + ) + else + entries + in + (* Generate precondition loop invariants. We do this in three steps: 1. Collect contexts for each function @@ -445,12 +529,12 @@ struct (* Generate invariant set *) let entries = - if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then ( + if entry_type_enabled YamlWitnessType.InvariantSet.entry_type || entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type && GobConfig.get_string "witness.invariant.flow_insensitive-as" = "invariant_set-location_invariant" then ( let invariants = [] in (* Generate location invariants *) let invariants = - if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( + if entry_type_enabled YamlWitnessType.InvariantSet.entry_type && invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( LH.fold (fun loc ns acc -> let inv = List.fold_left (fun acc n -> let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in @@ -480,7 +564,7 @@ struct (* Generate loop invariants *) let invariants = - if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( + if entry_type_enabled YamlWitnessType.InvariantSet.entry_type && invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( LH.fold (fun loc ns acc -> if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *) let inv = List.fold_left (fun acc n -> @@ -511,6 +595,31 @@ struct invariants in + (* Generate flow-insensitive invariants as location invariants *) + let invariants = + if entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type && GobConfig.get_string "witness.invariant.flow_insensitive-as" = "invariant_set-location_invariant" then ( + GHT.fold (fun g v acc -> + match g with + | `Left g -> (* global unknown from analysis Spec *) + begin match R.ask_global (InvariantGlobal (Obj.repr g)) with + | `Lifted inv -> + fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc -> + let invariant = CilType.Exp.show inv in + let invariant = Entry.location_invariant' ~location ~invariant in + incr cnt_location_invariant; + invariant :: acc + ) acc + | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) + acc + end + | `Right _ -> (* global unknown for FromSpec contexts *) + acc + ) gh invariants + ) + else + invariants + in + let invariants = List.rev invariants in let entry = Entry.invariant_set ~task ~invariants in entry :: entries @@ -852,7 +961,7 @@ struct None | _ -> incr cnt_unsupported; - M.info_noloc ~category:Witness "cannot validate entry of type %s" target_type; + M.warn_noloc ~category:Witness "cannot validate entry of type %s" target_type; None in @@ -864,7 +973,7 @@ struct Option.to_list yaml_certificate_entry @ yaml_entry :: yaml_entries' | Error (`Msg e) -> incr cnt_error; - M.info_noloc ~category:Witness "couldn't parse entry: %s" e; + M.error_noloc ~category:Witness "couldn't parse entry: %s" e; yaml_entry :: yaml_entries' ) [] yaml_entries in diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index c77fadad4c..7a57197a6f 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -9,6 +9,7 @@ struct command_line: string option; (* TODO: description *) } + [@@deriving eq, ord, hash] let to_yaml {name; version; command_line} = `O ([ @@ -39,6 +40,7 @@ struct language: string; specification: string option; } + [@@deriving eq, ord, hash] let to_yaml {input_files; input_file_hashes; data_model; language; specification} = `O ([ @@ -78,6 +80,7 @@ struct producer: Producer.t; task: Task.t option; } + [@@deriving eq, ord, hash] let to_yaml {format_version; uuid; creation_time; producer; task} = `O ([ @@ -111,7 +114,7 @@ struct column: int option; function_: string option; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {file_name; file_hash; line; column; function_} = `O ([ @@ -155,7 +158,7 @@ struct type_: string; format: string; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {string; type_; format} = `O [ @@ -178,7 +181,7 @@ struct location: Location.t; loop_invariant: Invariant.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "loop_invariant" @@ -201,7 +204,7 @@ struct location: Location.t; location_invariant: Invariant.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "location_invariant" @@ -223,7 +226,7 @@ struct type t = { flow_insensitive_invariant: Invariant.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "flow_insensitive_invariant" @@ -245,7 +248,7 @@ struct loop_invariant: Invariant.t; precondition: Invariant.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "precondition_loop_invariant" @@ -273,7 +276,7 @@ struct value: string; format: string; } - [@@deriving ord] + [@@deriving eq, ord, hash] let invariant_type = "loop_invariant" @@ -305,7 +308,7 @@ struct type t = | LocationInvariant of LocationInvariant.t | LoopInvariant of LoopInvariant.t - [@@deriving ord] + [@@deriving eq, ord, hash] let invariant_type = function | LocationInvariant _ -> LocationInvariant.invariant_type @@ -333,7 +336,7 @@ struct type t = { invariant_type: InvariantType.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {invariant_type} = `O [ @@ -352,7 +355,7 @@ struct type t = { content: Invariant.t list; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "invariant_set" @@ -372,7 +375,7 @@ struct type_: string; file_hash: string; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {uuid; type_; file_hash} = `O [ @@ -396,7 +399,7 @@ struct type_: string; format: string; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {string; type_; format} = `O [ @@ -419,7 +422,7 @@ struct target: Target.t; certification: Certification.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "loop_invariant_certificate" @@ -453,7 +456,7 @@ struct type t = | String of string | Int of int (* Why doesn't format consider ints (for switch branches) as strings here, like everywhere else? *) - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml = function | String s -> GobYaml.string s @@ -471,7 +474,7 @@ struct value: Value.t; format: string option; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {value; format} = `O ([ @@ -498,7 +501,7 @@ struct action: string; constraint_: Constraint.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let waypoint_type = "assumption" @@ -523,7 +526,7 @@ struct location: Location.t; action: string; } - [@@deriving ord] + [@@deriving eq, ord, hash] let waypoint_type = "target" @@ -570,7 +573,7 @@ struct | FunctionEnter of FunctionEnter.t | FunctionReturn of FunctionReturn.t | Branching of Branching.t - [@@deriving ord] + [@@deriving eq, ord, hash] let waypoint_type = function | Assumption _ -> Assumption.waypoint_type @@ -613,7 +616,7 @@ struct type t = { waypoint_type: WaypointType.t; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {waypoint_type} = `O [ @@ -634,7 +637,7 @@ struct type t = { segment: Waypoint.t list; } - [@@deriving ord] + [@@deriving eq, ord, hash] let to_yaml {segment} = `O [("segment", `A (List.map Waypoint.to_yaml segment))] @@ -648,7 +651,7 @@ struct type t = { content: Segment.t list; } - [@@deriving ord] + [@@deriving eq, ord, hash] let entry_type = "violation_sequence" @@ -661,6 +664,126 @@ struct {content} end +module GhostInstrumentation = +struct + + module Initial = + struct + type t = { + value: string; + format: string; + } + [@@deriving eq, ord, hash] + + let to_yaml {value; format} = + `O [ + ("value", `String value); + ("format", `String format); + ] + + let of_yaml y = + let open GobYaml in + let+ value = y |> find "value" >>= to_string + and+ format = y |> find "format" >>= to_string in + {value; format} + end + + module Variable = + struct + type t = { + name: string; + scope: string; + type_: string; + initial: Initial.t; + } + [@@deriving eq, ord, hash] + + let to_yaml {name; scope; type_; initial} = + `O [ + ("name", `String name); + ("scope", `String scope); + ("type", `String type_); + ("initial", Initial.to_yaml initial); + ] + + let of_yaml y = + let open GobYaml in + let+ name = y |> find "name" >>= to_string + and+ scope = y |> find "scope" >>= to_string + and+ type_ = y |> find "type" >>= to_string + and+ initial = y |> find "initial" >>= Initial.of_yaml in + {name; scope; type_; initial} + end + + module Update = + struct + type t = { + variable: string; + value: string; + format: string; + } + [@@deriving eq, ord, hash] + + let to_yaml {variable; value; format} = + `O [ + ("variable", `String variable); + ("value", `String value); + ("format", `String format); + ] + + let of_yaml y = + let open GobYaml in + let+ variable = y |> find "variable" >>= to_string + and+ value = y |> find "value" >>= to_string + and+ format = y |> find "format" >>= to_string in + {variable; value; format} + end + + module LocationUpdate = + struct + type t = { + location: Location.t; + updates: Update.t list; + } + [@@deriving eq, ord, hash] + + let to_yaml {location; updates} = + `O [ + ("location", Location.to_yaml location); + ("updates", `A (List.map Update.to_yaml updates)); + ] + + let of_yaml y = + let open GobYaml in + let+ location = y |> find "location" >>= Location.of_yaml + and+ updates = y |> find "updates" >>= list >>= list_map Update.of_yaml in + {location; updates} + end + + type t = { + ghost_variables: Variable.t list; + ghost_updates: LocationUpdate.t list; + } + [@@deriving eq, ord, hash] + + let entry_type = "ghost_instrumentation" + + let to_yaml' {ghost_variables; ghost_updates} = + [("content", + `O [ + ("ghost_variables", `A (List.map Variable.to_yaml ghost_variables)); + ("ghost_updates", `A (List.map LocationUpdate.to_yaml ghost_updates)); + ]) + ] + + let of_yaml y = + let open GobYaml in + let* content = y |> find "content" in + let+ ghost_variables = content |> find "ghost_variables" >>= list >>= list_map Variable.of_yaml + and+ ghost_updates = content |> find "ghost_updates" >>= list >>= list_map LocationUpdate.of_yaml in + {ghost_variables; ghost_updates} +end + (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *) module EntryType = struct @@ -673,7 +796,8 @@ struct | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t | InvariantSet of InvariantSet.t | ViolationSequence of ViolationSequence.t - [@@deriving ord] + | GhostInstrumentation of GhostInstrumentation.t + [@@deriving eq, ord, hash] let entry_type = function | LocationInvariant _ -> LocationInvariant.entry_type @@ -684,6 +808,7 @@ struct | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type | InvariantSet _ -> InvariantSet.entry_type | ViolationSequence _ -> ViolationSequence.entry_type + | GhostInstrumentation _ -> GhostInstrumentation.entry_type let to_yaml' = function | LocationInvariant x -> LocationInvariant.to_yaml' x @@ -694,6 +819,7 @@ struct | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x | InvariantSet x -> InvariantSet.to_yaml' x | ViolationSequence x -> ViolationSequence.to_yaml' x + | GhostInstrumentation x -> GhostInstrumentation.to_yaml' x let of_yaml y = let open GobYaml in @@ -722,16 +848,24 @@ struct else if entry_type = ViolationSequence.entry_type then let+ x = y |> ViolationSequence.of_yaml in ViolationSequence x + else if entry_type = GhostInstrumentation.entry_type then + let+ x = y |> GhostInstrumentation.of_yaml in + GhostInstrumentation x else - Error (`Msg "entry_type") + Error (`Msg ("entry_type " ^ entry_type)) end module Entry = struct + include Printable.StdLeaf + type t = { entry_type: EntryType.t; - metadata: Metadata.t; + metadata: Metadata.t [@equal fun _ _ -> true] [@compare fun _ _ -> 0] [@hash fun _ -> 1]; } + [@@deriving eq, ord, hash] + + let name () = "YAML entry" let to_yaml {entry_type; metadata} = `O ([ @@ -744,4 +878,10 @@ struct let+ metadata = y |> find "metadata" >>= Metadata.of_yaml and+ entry_type = y |> EntryType.of_yaml in {entry_type; metadata} + + let pp ppf x = Yaml.pp ppf (to_yaml x) + include Printable.SimpleFormat (struct + type nonrec t = t + let pp = pp + end) end diff --git a/tests/regression/13-privatized/04-priv_multi.t b/tests/regression/13-privatized/04-priv_multi.t new file mode 100644 index 0000000000..1f6dff3fdc --- /dev/null +++ b/tests/regression/13-privatized/04-priv_multi.t @@ -0,0 +1,335 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 04-priv_multi.c + [Success][Assert] Assertion "p == 5" will succeed (04-priv_multi.c:50:7-50:30) + [Success][Assert] Assertion "A == B" will succeed (04-priv_multi.c:71:5-71:28) + [Warning][Deadcode] Function 'dispose' has dead code: + on line 53 (04-priv_multi.c:53-53) + on line 56 (04-priv_multi.c:56-56) + [Warning][Deadcode] Function 'process' has dead code: + on line 37 (04-priv_multi.c:37-37) + on line 40 (04-priv_multi.c:40-40) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 40 + dead: 4 + total lines: 44 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (04-priv_multi.c:25:10-25:11) + [Warning][Deadcode][CWE-571] condition 'A > 0' is always true (04-priv_multi.c:27:9-27:14) + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (04-priv_multi.c:45:10-45:11) + [Warning][Deadcode][CWE-571] condition 'B > 0' is always true (04-priv_multi.c:47:9-47:14) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 3 + total generation entries: 4 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + + $ yamlWitnessStrip < witness.yml | tee witness.flow_insensitive.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: mutex_A_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: mutex_B_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 15 + column: 5 + function: generate + updates: + - variable: mutex_A_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 18 + column: 5 + function: generate + updates: + - variable: mutex_A_locked + value: "0" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 26 + column: 5 + function: process + updates: + - variable: mutex_A_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 29 + column: 7 + function: process + updates: + - variable: mutex_B_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 32 + column: 7 + function: process + updates: + - variable: mutex_B_locked + value: "0" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 34 + column: 7 + function: process + updates: + - variable: mutex_A_locked + value: "0" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 46 + column: 5 + function: dispose + updates: + - variable: mutex_B_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 49 + column: 7 + function: dispose + updates: + - variable: mutex_B_locked + value: "0" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 63 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 68 + column: 5 + function: main + updates: + - variable: mutex_A_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 69 + column: 5 + function: main + updates: + - variable: mutex_B_locked + value: "1" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 73 + column: 5 + function: main + updates: + - variable: mutex_B_locked + value: "0" + format: c_expression + - location: + file_name: 04-priv_multi.c + file_hash: $FILE_HASH + line: 74 + column: 5 + function: main + updates: + - variable: mutex_A_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (mutex_B_locked || (mutex_A_locked || B == 5))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (mutex_A_locked || A == 5)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || ((0 <= B && B <= 127) && B != 0)' + type: assertion + format: C + +Flow-insensitive invariants as location invariants. + + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' --set witness.invariant.flow_insensitive-as location_invariant 04-priv_multi.c + [Success][Assert] Assertion "p == 5" will succeed (04-priv_multi.c:50:7-50:30) + [Success][Assert] Assertion "A == B" will succeed (04-priv_multi.c:71:5-71:28) + [Warning][Deadcode] Function 'dispose' has dead code: + on line 53 (04-priv_multi.c:53-53) + on line 56 (04-priv_multi.c:56-56) + [Warning][Deadcode] Function 'process' has dead code: + on line 37 (04-priv_multi.c:37-37) + on line 40 (04-priv_multi.c:40-40) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 40 + dead: 4 + total lines: 44 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (04-priv_multi.c:25:10-25:11) + [Warning][Deadcode][CWE-571] condition 'A > 0' is always true (04-priv_multi.c:27:9-27:14) + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (04-priv_multi.c:45:10-45:11) + [Warning][Deadcode][CWE-571] condition 'B > 0' is always true (04-priv_multi.c:47:9-47:14) + [Info][Witness] witness generation summary: + location invariants: 9 + loop invariants: 0 + flow-insensitive invariants: 0 + total generation entries: 10 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + + $ yamlWitnessStrip < witness.yml > witness.location.yml + +Location invariant at `for` loop in `main` should be on column 3, not 7. + + $ diff witness.flow_insensitive.yml witness.location.yml + 153,154c153,160 + < - entry_type: flow_insensitive_invariant + < flow_insensitive_invariant: + --- + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 67 + > column: 3 + > function: main + > location_invariant: + 158,159c164,171 + < - entry_type: flow_insensitive_invariant + < flow_insensitive_invariant: + --- + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 67 + > column: 3 + > function: main + > location_invariant: + 163,164c175,248 + < - entry_type: flow_insensitive_invariant + < flow_insensitive_invariant: + --- + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 67 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || ((0 <= B && B <= 127) && B != 0)' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 65 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || (mutex_B_locked || (mutex_A_locked || B == 5))' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 65 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || (mutex_A_locked || A == 5)' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 65 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || ((0 <= B && B <= 127) && B != 0)' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 64 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || (mutex_B_locked || (mutex_A_locked || B == 5))' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 64 + > column: 3 + > function: main + > location_invariant: + > string: '! multithreaded || (mutex_A_locked || A == 5)' + > type: assertion + > format: C + > - entry_type: location_invariant + > location: + > file_name: 04-priv_multi.c + > file_hash: $FILE_HASH + > line: 64 + > column: 3 + > function: main + > location_invariant: + [1] diff --git a/tests/regression/13-privatized/25-struct_nr.t b/tests/regression/13-privatized/25-struct_nr.t new file mode 100644 index 0000000000..fa00b2a5a5 --- /dev/null +++ b/tests/regression/13-privatized/25-struct_nr.t @@ -0,0 +1,97 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 25-struct_nr.c + [Success][Assert] Assertion "glob1 == 5" will succeed (25-struct_nr.c:26:3-26:30) + [Success][Assert] Assertion "t == 5" will succeed (25-struct_nr.c:16:3-16:26) + [Success][Assert] Assertion "glob1 == -10" will succeed (25-struct_nr.c:18:3-18:32) + [Success][Assert] Assertion "glob1 == 6" will succeed (25-struct_nr.c:30:3-30:30) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 19 + dead: 0 + total lines: 19 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: lock1_mutex_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 25-struct_nr.c + file_hash: $FILE_HASH + line: 14 + column: 3 + function: t_fun + updates: + - variable: lock1_mutex_locked + value: "1" + format: c_expression + - location: + file_name: 25-struct_nr.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: t_fun + updates: + - variable: lock1_mutex_locked + value: "0" + format: c_expression + - location: + file_name: 25-struct_nr.c + file_hash: $FILE_HASH + line: 27 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 25-struct_nr.c + file_hash: $FILE_HASH + line: 28 + column: 3 + function: main + updates: + - variable: lock1_mutex_locked + value: "1" + format: c_expression + - location: + file_name: 25-struct_nr.c + file_hash: $FILE_HASH + line: 32 + column: 3 + function: main + updates: + - variable: lock1_mutex_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (lock1_mutex_locked || glob1 == 5)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || ((-128 <= glob1 && glob1 <= 127) && glob1 != 0)' + type: assertion + format: C diff --git a/tests/regression/13-privatized/74-mutex.t b/tests/regression/13-privatized/74-mutex.t new file mode 100644 index 0000000000..4b370db387 --- /dev/null +++ b/tests/regression/13-privatized/74-mutex.t @@ -0,0 +1,395 @@ + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml | tee witness.flow_insensitive.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 20 + column: 5 + function: producer + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 23 + column: 5 + function: producer + updates: + - variable: m_locked + value: "0" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 34 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 36 + column: 3 + function: main + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 38 + column: 3 + function: main + updates: + - variable: m_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m_locked || used == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= used && used <= 1)' + type: assertion + format: C + +Flow-insensitive invariants as location invariants. + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' --set witness.invariant.flow_insensitive-as location_invariant 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml > witness.location.yml + + $ diff witness.flow_insensitive.yml witness.location.yml + 67,68c67,74 + < - entry_type: flow_insensitive_invariant + < flow_insensitive_invariant: + --- + > - entry_type: location_invariant + > location: + > file_name: 74-mutex.c + > file_hash: $FILE_HASH + > line: 36 + > column: 3 + > function: main + > location_invariant: + 72,73c78,85 + < - entry_type: flow_insensitive_invariant + < flow_insensitive_invariant: + --- + > - entry_type: location_invariant + > location: + > file_name: 74-mutex.c + > file_hash: $FILE_HASH + > line: 36 + > column: 3 + > function: main + > location_invariant: + [1] + +Should also work with earlyglobs. +Earlyglobs shouldn't cause protected writes in multithreaded mode from being immediately published to protected invariant. + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable exp.earlyglobs 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + +Same with ghost_instrumentation and invariant_set entries. + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' --set witness.invariant.flow_insensitive-as invariant_set-location_invariant 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Witness] witness generation summary: + location invariants: 2 + loop invariants: 0 + flow-insensitive invariants: 0 + total generation entries: 2 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 20 + column: 5 + function: producer + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 23 + column: 5 + function: producer + updates: + - variable: m_locked + value: "0" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 34 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 36 + column: 3 + function: main + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 38 + column: 3 + function: main + updates: + - variable: m_locked + value: "0" + format: c_expression + - entry_type: invariant_set + content: + - invariant: + type: location_invariant + location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 36 + column: 3 + function: main + value: '! multithreaded || (0 <= used && used <= 1)' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 36 + column: 3 + function: main + value: '! multithreaded || (m_locked || used == 0)' + format: c_expression + +Same with mutex-meet. + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 20 + column: 5 + function: producer + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 23 + column: 5 + function: producer + updates: + - variable: m_locked + value: "0" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 34 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 36 + column: 3 + function: main + updates: + - variable: m_locked + value: "1" + format: c_expression + - location: + file_name: 74-mutex.c + file_hash: $FILE_HASH + line: 38 + column: 3 + function: main + updates: + - variable: m_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m_locked || used == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= used && used <= 1)' + type: assertion + format: C + +Should also work with earlyglobs. + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable exp.earlyglobs 74-mutex.c + [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29) + [Warning][Deadcode] Function 'producer' has dead code: + on line 26 (74-mutex.c:26-26) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 1 + total lines: 15 + [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (74-mutex.c:19:10-19:11) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 diff --git a/tests/regression/13-privatized/92-idx_priv.c b/tests/regression/13-privatized/92-idx_priv.c new file mode 100644 index 0000000000..ed0e8d3228 --- /dev/null +++ b/tests/regression/13-privatized/92-idx_priv.c @@ -0,0 +1,26 @@ +#include +#include + +int data; +pthread_mutex_t m[10]; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[4]); + data++; // NORACE + data--; // NORACE + pthread_mutex_unlock(&m[4]); + return NULL; +} + +int main() { + for (int i = 0; i < 10; i++) + pthread_mutex_init(&m[i], NULL); + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&m[4]); + __goblint_check(data == 0); // NORACE + pthread_mutex_unlock(&m[4]); + return 0; +} + diff --git a/tests/regression/13-privatized/92-idx_priv.t b/tests/regression/13-privatized/92-idx_priv.t new file mode 100644 index 0000000000..7b3adc5e0b --- /dev/null +++ b/tests/regression/13-privatized/92-idx_priv.t @@ -0,0 +1,45 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 92-idx_priv.c + [Success][Assert] Assertion "data == 0" will succeed (92-idx_priv.c:22:3-22:29) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 1 + total generation entries: 2 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 92-idx_priv.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= data && data <= 1)' + type: assertion + format: C + +TODO: protected invariant with m_4_locked without making 56-witness/68-ghost-ambiguous-idx unsound diff --git a/tests/regression/13-privatized/dune b/tests/regression/13-privatized/dune index 23c0dd3290..9227128b15 100644 --- a/tests/regression/13-privatized/dune +++ b/tests/regression/13-privatized/dune @@ -1,2 +1,6 @@ (cram (deps (glob_files *.c))) + +(cram + (applies_to 04-priv_multi) + (enabled_if (<> %{system} macosx))) diff --git a/tests/regression/29-svcomp/16-atomic_priv.t b/tests/regression/29-svcomp/16-atomic_priv.t new file mode 100644 index 0000000000..1662f881b7 --- /dev/null +++ b/tests/regression/29-svcomp/16-atomic_priv.t @@ -0,0 +1,111 @@ + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 16-atomic_priv.c + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:12:3-12:33) + [Success][Assert] Assertion "myglobal == 6" will succeed (16-atomic_priv.c:14:3-14:33) + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:16:3-16:33) + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:24:3-24:33) + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:26:3-26:33) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17) + write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) + write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) + read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 1 + total generation entries: 2 + [Info][Race] Memory locations race summary: + safe: 0 + vulnerable: 0 + unsafe: 1 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 16-atomic_priv.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || myglobal == 5' + type: assertion + format: C + +Non-atomic privatization: + + $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 16-atomic_priv.c + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:12:3-12:33) + [Success][Assert] Assertion "myglobal == 6" will succeed (16-atomic_priv.c:14:3-14:33) + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:16:3-16:33) + [Warning][Assert] Assertion "myglobal == 5" is unknown. (16-atomic_priv.c:24:3-24:33) + [Success][Assert] Assertion "myglobal == 5" will succeed (16-atomic_priv.c:26:3-26:33) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 17 + dead: 0 + total lines: 17 + [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17) + write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) + write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) + read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 0 + vulnerable: 0 + unsafe: 1 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 16-atomic_priv.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || myglobal == 5' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || ((0 <= myglobal && myglobal <= 127) && myglobal != + 0)' + type: assertion + format: C diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t index d0cebd6d1c..2a760c0dcb 100644 --- a/tests/regression/36-apron/12-traces-min-rpb1.t +++ b/tests/regression/36-apron/12-traces-min-rpb1.t @@ -57,3 +57,123 @@ string: (0LL - (long long )g) + (long long )h == 0LL type: assertion format: C + + + $ goblint --enable warn.deterministic --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 12-traces-min-rpb1.c --enable ana.apron.invariant.diff-box + [Warning][Assert] Assertion "g == h" is unknown. (12-traces-min-rpb1.c:27:3-27:26) + [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26) + [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:29:3-29:26) + [Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10) + write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) + [Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10) + write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26) + [Info][Race] Memory locations race summary: + safe: 0 + vulnerable: 0 + unsafe: 2 + total memory locations: 2 + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 18 + dead: 0 + total lines: 18 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 1 + total generation entries: 2 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: A_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: A_locked + value: "1" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 17 + column: 3 + function: t_fun + updates: + - variable: A_locked + value: "0" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 18 + column: 3 + function: t_fun + updates: + - variable: A_locked + value: "1" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 19 + column: 3 + function: t_fun + updates: + - variable: A_locked + value: "0" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 25 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 28 + column: 3 + function: main + updates: + - variable: A_locked + value: "1" + format: c_expression + - location: + file_name: 12-traces-min-rpb1.c + file_hash: $FILE_HASH + line: 30 + column: 3 + function: main + updates: + - variable: A_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (A_locked || ((0LL - (long long )g) + (long long )h + >= 0LL && (long long )g - (long long )h >= 0LL))' + type: assertion + format: C diff --git a/tests/regression/56-witness/64-ghost-multiple-protecting.c b/tests/regression/56-witness/64-ghost-multiple-protecting.c new file mode 100644 index 0000000000..a9fa3310e4 --- /dev/null +++ b/tests/regression/56-witness/64-ghost-multiple-protecting.c @@ -0,0 +1,41 @@ +// PARAM: --set ana.activated[+] mutexGhosts +#include +#include +int g1, g2; +pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER; +// CRAM +void *t_fun(void *arg) { + pthread_mutex_lock(&m1); + pthread_mutex_lock(&m2); + g1 = 1; + g1 = 0; + pthread_mutex_unlock(&m2); + pthread_mutex_unlock(&m1); + + pthread_mutex_lock(&m1); + pthread_mutex_lock(&m2); + g2 = 1; + pthread_mutex_unlock(&m2); + pthread_mutex_lock(&m2); + g2 = 0; + pthread_mutex_unlock(&m2); + pthread_mutex_unlock(&m1); + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + /* pthread_mutex_lock(&m1); + __goblint_check(g1 == 0); // NOWARN (commented out) + __goblint_check(g2 == 0); // NOWARN (commented out) + pthread_mutex_unlock(&m1); + + pthread_mutex_lock(&m2); + __goblint_check(g1 == 0); // NOWARN (commented out) + __goblint_check(g2 == 0); // NOWARN (commented out) + pthread_mutex_unlock(&m2); */ + return 0; +} diff --git a/tests/regression/56-witness/64-ghost-multiple-protecting.t b/tests/regression/56-witness/64-ghost-multiple-protecting.t new file mode 100644 index 0000000000..cfa3995005 --- /dev/null +++ b/tests/regression/56-witness/64-ghost-multiple-protecting.t @@ -0,0 +1,508 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 19 + dead: 0 + total lines: 19 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 3 + total generation entries: 4 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +protection doesn't have precise protected invariant for g2. + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m1_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: m2_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 9 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 10 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 14 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 16 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 17 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 19 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 22 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 29 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m2_locked || (m1_locked || g1 == 0))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g2 && g2 <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C + + $ goblint --set ana.base.privatization protection-read --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 19 + dead: 0 + total lines: 19 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 4 + total generation entries: 5 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + +protection-read has precise protected invariant for g2. + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m1_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: m2_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 9 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 10 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 14 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 16 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 17 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 19 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 22 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 29 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m2_locked || (m1_locked || g2 == 0))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m2_locked || (m1_locked || g1 == 0))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g2 && g2 <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C + + $ goblint --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 64-ghost-multiple-protecting.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 19 + dead: 0 + total lines: 19 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 4 + total generation entries: 5 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m1_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: m2_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 9 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 10 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 14 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 16 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 17 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 19 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 22 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 64-ghost-multiple-protecting.c + file_hash: $FILE_HASH + line: 29 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m2_locked || ((0 <= g2 && g2 <= 1) && g1 == 0))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m1_locked || (g1 == 0 && g2 == 0))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g2 && g2 <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C diff --git a/tests/regression/56-witness/65-ghost-ambiguous-lock.c b/tests/regression/56-witness/65-ghost-ambiguous-lock.c new file mode 100644 index 0000000000..7719c0cec4 --- /dev/null +++ b/tests/regression/56-witness/65-ghost-ambiguous-lock.c @@ -0,0 +1,44 @@ +// PARAM: --set ana.activated[+] mutexGhosts +#include +#include +// CRAM +int g1, g2; +pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m1); + g1 = 1; + g1 = 0; + pthread_mutex_unlock(&m1); + pthread_mutex_lock(&m2); + g2 = 1; + g2 = 0; + pthread_mutex_unlock(&m2); + return NULL; +} + +void fun(pthread_mutex_t *m) { + pthread_mutex_lock(m); + // what g2 can read? + pthread_mutex_unlock(m); +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_t *m; + int r; // rand + m = r ? &m1 : &m2; + + pthread_mutex_lock(m); + // what g1 can read? + pthread_mutex_unlock(m); + + if (r) + fun(&m1); + else + fun(&m2); + return 0; +} diff --git a/tests/regression/56-witness/65-ghost-ambiguous-lock.t b/tests/regression/56-witness/65-ghost-ambiguous-lock.t new file mode 100644 index 0000000000..36df2e4576 --- /dev/null +++ b/tests/regression/56-witness/65-ghost-ambiguous-lock.t @@ -0,0 +1,47 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 65-ghost-ambiguous-lock.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 23 + dead: 0 + total lines: 23 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 65-ghost-ambiguous-lock.c + file_hash: $FILE_HASH + line: 29 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g2 && g2 <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C diff --git a/tests/regression/56-witness/66-ghost-alloc-lock.c b/tests/regression/56-witness/66-ghost-alloc-lock.c new file mode 100644 index 0000000000..073540b9db --- /dev/null +++ b/tests/regression/56-witness/66-ghost-alloc-lock.c @@ -0,0 +1,37 @@ +// PARAM: --set ana.activated[+] mutexGhosts --set ana.malloc.unique_address_count 1 +#include +#include + +int g1, g2; +pthread_mutex_t *m1; +pthread_mutex_t *m2; + +void *t_fun(void *arg) { + pthread_mutex_lock(m1); + g1 = 1; + g1 = 0; + pthread_mutex_unlock(m1); + pthread_mutex_lock(m2); + g2 = 1; + g2 = 0; + pthread_mutex_unlock(m2); + return NULL; +} + +int main() { + m1 = malloc(sizeof(pthread_mutex_t)); + pthread_mutex_init(m1, NULL); + m2 = malloc(sizeof(pthread_mutex_t)); + pthread_mutex_init(m2, NULL); + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(m1); + __goblint_check(g1 == 0); + pthread_mutex_unlock(m1); + pthread_mutex_lock(m2); + __goblint_check(g2 == 0); + pthread_mutex_unlock(m2); + return 0; +} diff --git a/tests/regression/56-witness/66-ghost-alloc-lock.t b/tests/regression/56-witness/66-ghost-alloc-lock.t new file mode 100644 index 0000000000..09c7c4250b --- /dev/null +++ b/tests/regression/56-witness/66-ghost-alloc-lock.t @@ -0,0 +1,151 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set ana.malloc.unique_address_count 1 --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 66-ghost-alloc-lock.c + [Success][Assert] Assertion "g1 == 0" will succeed (66-ghost-alloc-lock.c:31:3-31:27) + [Success][Assert] Assertion "g2 == 0" will succeed (66-ghost-alloc-lock.c:34:3-34:27) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 23 + dead: 0 + total lines: 23 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 4 + total generation entries: 5 + [Info][Race] Memory locations race summary: + safe: 4 + vulnerable: 0 + unsafe: 0 + total memory locations: 4 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: alloc_m559918035_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: alloc_m861095507_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 10 + column: 3 + function: t_fun + updates: + - variable: alloc_m559918035_locked + value: "1" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: alloc_m559918035_locked + value: "0" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 14 + column: 3 + function: t_fun + updates: + - variable: alloc_m861095507_locked + value: "1" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 17 + column: 3 + function: t_fun + updates: + - variable: alloc_m861095507_locked + value: "0" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 28 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 30 + column: 3 + function: main + updates: + - variable: alloc_m559918035_locked + value: "1" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 32 + column: 3 + function: main + updates: + - variable: alloc_m559918035_locked + value: "0" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 33 + column: 3 + function: main + updates: + - variable: alloc_m861095507_locked + value: "1" + format: c_expression + - location: + file_name: 66-ghost-alloc-lock.c + file_hash: $FILE_HASH + line: 35 + column: 3 + function: main + updates: + - variable: alloc_m861095507_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (alloc_m861095507_locked || g2 == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (alloc_m559918035_locked || g1 == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g2 && g2 <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C diff --git a/tests/regression/56-witness/67-ghost-no-unlock.c b/tests/regression/56-witness/67-ghost-no-unlock.c new file mode 100644 index 0000000000..69ad571118 --- /dev/null +++ b/tests/regression/56-witness/67-ghost-no-unlock.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] mutexGhosts +#include +#include + +int g1; +pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m1); + g1 = 1; + g1 = 0; + pthread_mutex_unlock(&m1); + return NULL; +} + +int main() { + + + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&m1); + __goblint_check(g1 == 0); + // no unlock + return 0; // there should be no ghost updates for unlock here +} diff --git a/tests/regression/56-witness/67-ghost-no-unlock.t b/tests/regression/56-witness/67-ghost-no-unlock.t new file mode 100644 index 0000000000..c49daf3e24 --- /dev/null +++ b/tests/regression/56-witness/67-ghost-no-unlock.t @@ -0,0 +1,84 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 67-ghost-no-unlock.c + [Success][Assert] Assertion "g1 == 0" will succeed (67-ghost-no-unlock.c:24:3-24:27) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 3 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m1_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 67-ghost-no-unlock.c + file_hash: $FILE_HASH + line: 9 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 67-ghost-no-unlock.c + file_hash: $FILE_HASH + line: 12 + column: 3 + function: t_fun + updates: + - variable: m1_locked + value: "0" + format: c_expression + - location: + file_name: 67-ghost-no-unlock.c + file_hash: $FILE_HASH + line: 21 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 67-ghost-no-unlock.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: main + updates: + - variable: m1_locked + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m1_locked || g1 == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g1 && g1 <= 1)' + type: assertion + format: C diff --git a/tests/regression/56-witness/68-ghost-ambiguous-idx.c b/tests/regression/56-witness/68-ghost-ambiguous-idx.c new file mode 100644 index 0000000000..7babbe003c --- /dev/null +++ b/tests/regression/56-witness/68-ghost-ambiguous-idx.c @@ -0,0 +1,28 @@ +#include +#include + +int data; +pthread_mutex_t m[10]; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[4]); + data++; + data--; + pthread_mutex_unlock(&m[4]); + return NULL; +} + +int main() { + for (int i = 0; i < 10; i++) + pthread_mutex_init(&m[i], NULL); + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + int r; + int j = r ? 4 : 5; + pthread_mutex_lock(&m[r]); + __goblint_check(data == 0); // UNKNOWN! + pthread_mutex_unlock(&m[4]); + return 0; +} + diff --git a/tests/regression/56-witness/68-ghost-ambiguous-idx.t b/tests/regression/56-witness/68-ghost-ambiguous-idx.t new file mode 100644 index 0000000000..40025acf17 --- /dev/null +++ b/tests/regression/56-witness/68-ghost-ambiguous-idx.t @@ -0,0 +1,48 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 68-ghost-ambiguous-idx.c + [Warning][Assert] Assertion "data == 0" is unknown. (68-ghost-ambiguous-idx.c:24:3-24:29) + [Warning][Unknown] unlocking mutex (m[4]) which may not be held (68-ghost-ambiguous-idx.c:25:3-25:30) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 15 + dead: 0 + total lines: 15 + [Warning][Race] Memory location data (race with conf. 110): (68-ghost-ambiguous-idx.c:4:5-4:9) + write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:9:3-9:9) + write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:10:3-10:9) + read with [mhp:{created={[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:24:3-24:29) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 1 + total generation entries: 2 + [Info][Race] Memory locations race summary: + safe: 0 + vulnerable: 0 + unsafe: 1 + total memory locations: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 68-ghost-ambiguous-idx.c + file_hash: $FILE_HASH + line: 20 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= data && data <= 1)' + type: assertion + format: C diff --git a/tests/regression/56-witness/69-ghost-ptr-protection.c b/tests/regression/56-witness/69-ghost-ptr-protection.c new file mode 100644 index 0000000000..f5557f3fc8 --- /dev/null +++ b/tests/regression/56-witness/69-ghost-ptr-protection.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.activated[+] mutexGhosts +// CRAM +#include +#include + +int g = 0; +int *p = &g; +pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + int x = 10; + pthread_mutex_lock(&m2); + p = &x; + p = &g; + pthread_mutex_unlock(&m2); + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&m1); + g = 1; + // m2_locked || (p == & g && *p == 0) would be violated here + __goblint_check(*p != 0); // 1 from g or 10 from x in t_fun + g = 0; + pthread_mutex_unlock(&m1); + return 0; +} diff --git a/tests/regression/56-witness/69-ghost-ptr-protection.t b/tests/regression/56-witness/69-ghost-ptr-protection.t new file mode 100644 index 0000000000..53aa7dd34a --- /dev/null +++ b/tests/regression/56-witness/69-ghost-ptr-protection.t @@ -0,0 +1,116 @@ + $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types '["flow_insensitive_invariant", "ghost_instrumentation"]' 69-ghost-ptr-protection.c + [Success][Assert] Assertion "*p != 0" will succeed (69-ghost-ptr-protection.c:26:3-26:27) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 15 + dead: 0 + total lines: 15 + [Warning][Race] Memory location p (race with conf. 110): (69-ghost-ptr-protection.c:7:5-7:12) + write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9) + write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9) + read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, thread:[main]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27) + [Info][Witness] witness generation summary: + location invariants: 0 + loop invariants: 0 + flow-insensitive invariants: 4 + total generation entries: 5 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 + +Should not contain unsound flow-insensitive invariant m2_locked || (p == & g && *p == 0): + + $ yamlWitnessStrip < witness.yml + - entry_type: ghost_instrumentation + content: + ghost_variables: + - name: m1_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: m2_locked + scope: global + type: int + initial: + value: "0" + format: c_expression + - name: multithreaded + scope: global + type: int + initial: + value: "0" + format: c_expression + ghost_updates: + - location: + file_name: 69-ghost-ptr-protection.c + file_hash: $FILE_HASH + line: 13 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "1" + format: c_expression + - location: + file_name: 69-ghost-ptr-protection.c + file_hash: $FILE_HASH + line: 16 + column: 3 + function: t_fun + updates: + - variable: m2_locked + value: "0" + format: c_expression + - location: + file_name: 69-ghost-ptr-protection.c + file_hash: $FILE_HASH + line: 22 + column: 3 + function: main + updates: + - variable: multithreaded + value: "1" + format: c_expression + - location: + file_name: 69-ghost-ptr-protection.c + file_hash: $FILE_HASH + line: 23 + column: 3 + function: main + updates: + - variable: m1_locked + value: "1" + format: c_expression + - location: + file_name: 69-ghost-ptr-protection.c + file_hash: $FILE_HASH + line: 28 + column: 3 + function: main + updates: + - variable: m1_locked + value: "0" + format: c_expression + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m2_locked || ((0 <= *p && *p <= 1) && p == & g))' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (m1_locked || g == 0)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (0 <= g && g <= 1)' + type: assertion + format: C + - entry_type: flow_insensitive_invariant + flow_insensitive_invariant: + string: '! multithreaded || (*p == 10 || ((0 <= *p && *p <= 1) && p == & g))' + type: assertion + format: C diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.c b/tests/regression/56-witness/70-apron-unassume-set-tokens.c similarity index 88% rename from tests/regression/56-witness/64-apron-unassume-set-tokens.c rename to tests/regression/56-witness/70-apron-unassume-set-tokens.c index 75a6b5eee5..6ff07f6064 100644 --- a/tests/regression/56-witness/64-apron-unassume-set-tokens.c +++ b/tests/regression/56-witness/70-apron-unassume-set-tokens.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 64-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens +// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 70-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens #include // Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing. // Copied & extended from 56-witness/12-apron-unassume-branch. diff --git a/tests/regression/56-witness/64-apron-unassume-set-tokens.yml b/tests/regression/56-witness/70-apron-unassume-set-tokens.yml similarity index 82% rename from tests/regression/56-witness/64-apron-unassume-set-tokens.yml rename to tests/regression/56-witness/70-apron-unassume-set-tokens.yml index 8411ed045f..1fdc29067c 100644 --- a/tests/regression/56-witness/64-apron-unassume-set-tokens.yml +++ b/tests/regression/56-witness/70-apron-unassume-set-tokens.yml @@ -8,19 +8,19 @@ version: heads/yaml-witness-unassume-0-g48503c690-dirty command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''64-apron-unassume-set-tokens.c''' + ''70-apron-unassume-set-tokens.c''' task: input_files: - - 64-apron-unassume-set-tokens.c + - 70-apron-unassume-set-tokens.c input_file_hashes: - 64-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 + 70-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 data_model: LP64 language: C content: - invariant: type: location_invariant location: - file_name: 64-apron-unassume-set-tokens.c + file_name: 70-apron-unassume-set-tokens.c file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 line: 8 column: 3 @@ -30,7 +30,7 @@ - invariant: type: location_invariant location: - file_name: 64-apron-unassume-set-tokens.c + file_name: 70-apron-unassume-set-tokens.c file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 line: 8 column: 3 @@ -40,7 +40,7 @@ - invariant: type: location_invariant location: - file_name: 64-apron-unassume-set-tokens.c + file_name: 70-apron-unassume-set-tokens.c file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 line: 14 column: 3 @@ -50,7 +50,7 @@ - invariant: type: location_invariant location: - file_name: 64-apron-unassume-set-tokens.c + file_name: 70-apron-unassume-set-tokens.c file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60 line: 14 column: 3 diff --git a/tests/util/yamlWitnessStripCommon.ml b/tests/util/yamlWitnessStripCommon.ml index d1656d3ddc..39bc231d72 100644 --- a/tests/util/yamlWitnessStripCommon.ml +++ b/tests/util/yamlWitnessStripCommon.ml @@ -50,6 +50,12 @@ struct let segment_strip_file_hash ({segment}: ViolationSequence.Segment.t): ViolationSequence.Segment.t = {segment = List.map waypoint_strip_file_hash segment} in + let ghost_location_update_strip_file_hash (x: GhostInstrumentation.LocationUpdate.t): GhostInstrumentation.LocationUpdate.t = + { + location = location_strip_file_hash x.location; + updates = List.sort GhostInstrumentation.Update.compare x.updates + } + in let entry_type: EntryType.t = match entry_type with | LocationInvariant x -> @@ -65,9 +71,14 @@ struct | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target} | InvariantSet x -> - InvariantSet {content = List.map invariant_strip_file_hash x.content} + InvariantSet {content = List.sort InvariantSet.Invariant.compare (List.map invariant_strip_file_hash x.content)} (* Sort, so order is deterministic regardless of Goblint. *) | ViolationSequence x -> ViolationSequence {content = List.map segment_strip_file_hash x.content} + | GhostInstrumentation x -> + GhostInstrumentation { (* Sort, so order is deterministic regardless of Goblint. *) + ghost_variables = List.sort GhostInstrumentation.Variable.compare x.ghost_variables; + ghost_updates = List.sort GhostInstrumentation.LocationUpdate.compare (List.map ghost_location_update_strip_file_hash x.ghost_updates); + } in {entry_type}