diff --git a/src/cdomain/value/domains/invariant.ml b/src/cdomain/value/domains/invariant.ml index b281e8f7b3..477fc426a0 100644 --- a/src/cdomain/value/domains/invariant.ml +++ b/src/cdomain/value/domains/invariant.ml @@ -1,4 +1,4 @@ -(** Invariants for witnesses. *) + open GoblintCil @@ -37,6 +37,9 @@ include Lattice.LiftConf (N) (ExpLat) let none = top () let of_exp = lift +let to_exp = function + | `Lifted x -> Some x + | `Top | `Bot -> None let ( && ) = meet let ( || ) = join diff --git a/src/cdomain/value/domains/invariant.mli b/src/cdomain/value/domains/invariant.mli new file mode 100644 index 0000000000..da41da1755 --- /dev/null +++ b/src/cdomain/value/domains/invariant.mli @@ -0,0 +1,19 @@ +(** Invariants for witnesses. *) + +include Lattice.S + +val none: t +val of_exp: GoblintCil.exp -> t + +val to_exp: t -> GoblintCil.exp option + +val (&&): t -> t -> t +val (||): t -> t -> t + + +type context = { + path: int option; + lvals: Lval.Set.t; +} + +val default_context : context diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 8f858d09df..45dba8f5b0 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -58,8 +58,8 @@ struct | Some lval -> Lval.(Set.singleton lval) in let context = {Invariant.default_context with lvals} in - match (ask ~node loc).f (Queries.Invariant context) with - | `Lifted e -> + match Invariant.to_exp ((ask ~node loc).f (Queries.Invariant context)) with + | Some e -> let es = WitnessUtil.InvariantExp.process_exp e in let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in if surroundByAtomic then @@ -68,7 +68,7 @@ struct abegin :: (asserts @ [aend]) else asserts - | _ -> [] + | None -> [] in let instrument_instructions il s = diff --git a/src/witness/witness.ml b/src/witness/witness.ml index bb70c3319f..7f3069263d 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -6,6 +6,7 @@ open Svcomp open GobConfig module M = Messages +module OuterInvariant = Invariant module type WitnessTaskResult = TaskResult with module Arg.Edge = MyARG.InlineEdge @@ -38,8 +39,8 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) | MyARG.CFGEdge (Test _) -> true | _ -> false end || begin if Invariant.is_invariant_node to_cfgnode then - match to_cfgnode, TaskResult.invariant to_node with - | Statement _, `Lifted _ -> true + match to_cfgnode, OuterInvariant.to_exp (TaskResult.invariant to_node) with + | Statement _, Some _ -> true | _, _ -> false else false @@ -137,8 +138,8 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) end; begin if Invariant.is_invariant_node cfgnode then - match cfgnode, TaskResult.invariant node with - | Statement _, `Lifted i -> + match cfgnode, OuterInvariant.to_exp (TaskResult.invariant node) with + | Statement _, Some i -> let i = InvariantCil.exp_replace_original_name i in [("invariant", CilType.Exp.show i); ("invariant.scope", (Node.find_fundec cfgnode).svar.vname)] diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 9d04b597fa..77c4bb7924 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -293,8 +293,8 @@ struct Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in - match inv with - | `Lifted inv -> + match Invariant.to_exp inv with + | Some inv -> let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) let location_function = fundec.svar.vname in let location = Entry.location ~location:loc ~location_function in @@ -305,7 +305,7 @@ struct incr cnt_location_invariant; entry :: acc ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + | None -> (* TODO: 0 for bot (dead code)? *) acc ) (Lazy.force location_nodes) entries ) @@ -323,8 +323,8 @@ struct Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in - match inv with - | `Lifted inv -> + match Invariant.to_exp inv with + | Some inv -> let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) let location_function = fundec.svar.vname in let location = Entry.location ~location:loc ~location_function in @@ -335,7 +335,7 @@ struct incr cnt_loop_invariant; entry :: acc ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + | None -> (* TODO: 0 for bot (dead code)? *) acc ) else @@ -372,8 +372,8 @@ struct 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)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with - | `Lifted inv, "flow_insensitive_invariant" -> + begin match Invariant.to_exp (R.ask_global (InvariantGlobal (Obj.repr g))), GobConfig.get_string "witness.invariant.flow_insensitive-as" with + | Some 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 @@ -381,15 +381,15 @@ struct incr cnt_flow_insensitive_invariant; entry :: acc ) acc invs - | `Lifted inv, "location_invariant" -> + | Some 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 *) + | Some _, _ + | None, _ -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) acc end | `Right _ -> (* global unknown for FromSpec contexts *) @@ -450,11 +450,11 @@ struct let fc_map : con_inv list FCMap.t = FCMap.create 103 in FMap.iter (fun f con_invs -> List.iter (fun current_c -> - begin match current_c.invariant with - | `Lifted c_inv -> + begin match Invariant.to_exp current_c.invariant with + | Some c_inv -> (* Collect all start states that may satisfy the invariant of current_c *) List.iter (fun c -> - let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in + let x = R.ask_local (c.node, c.context) ~local:c.state (Queries.EvalInt c_inv) in (* TODO: illegal query *) if Queries.ID.is_bot x || Queries.ID.is_bot_ikind x then (* dead code *) failwith "Bottom not expected when querying context state" (* Maybe this is reachable, failwith for now so we see when this happens *) else if Queries.ID.to_bool x = Some false then () (* Nothing to do, the c does definitely not satisfy the predicate of current_c *) @@ -463,7 +463,7 @@ struct FCMap.modify_def [] (f, current_c.context) (fun cs -> c::cs) fc_map; end ) con_invs; - | `Bot | `Top -> + | None -> (* If the context invariant is None, we will not generate a precondition invariant. Nothing to do here. *) () end @@ -484,25 +484,25 @@ struct let fundec = Node.find_fundec n in let pre_lvar = (Node.FunctionEntry fundec, c) in let query = Queries.Invariant Invariant.default_context in - begin match R.ask_local pre_lvar query with - | `Lifted c_inv -> + begin match Invariant.to_exp (R.ask_local pre_lvar query) with + | Some c_inv -> (* Find unknowns for which the preceding start state satisfies the precondtion *) let xs = find_matching_states lvar in (* Generate invariants. Give up in case one invariant could not be generated. *) let invs = GobList.fold_while_some (fun acc local -> let lvals = local_lvals n local in - match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with - | `Lifted c -> Some ((`Lifted c)::acc) - | `Bot | `Top -> None + match Invariant.to_exp (R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) with + | Some c -> Some ((Invariant.of_exp c)::acc) + | None -> None ) [] xs in begin match invs with | None | Some [] -> acc | Some (x::xs) -> - begin match List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs with (* bisect_ppx cannot handle redefined (||) *) - | `Lifted inv -> + begin match Invariant.to_exp (List.fold_left (fun acc inv -> Invariant.(acc || inv) [@coverage off]) x xs) with (* bisect_ppx cannot handle redefined (||) *) + | Some inv -> let invs = WitnessUtil.InvariantExp.process_exp inv in let c_inv = InvariantCil.exp_replace_original_name c_inv in (* cannot be split *) List.fold_left (fun acc inv -> @@ -513,7 +513,7 @@ struct let entry = Entry.precondition_loop_invariant ~task ~location ~precondition ~invariant in entry :: acc ) acc invs - | `Bot | `Top -> acc + | None -> acc end end | _ -> (* Do not construct precondition invariants if we cannot express precondition *) @@ -542,8 +542,8 @@ struct Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in - match inv with - | `Lifted inv -> + match Invariant.to_exp inv with + | Some inv -> let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) let location_function = fundec.svar.vname in let location = Entry.location ~location:loc ~location_function in @@ -554,7 +554,7 @@ struct incr cnt_location_invariant; invariant :: acc ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + | None -> (* TODO: 0 for bot (dead code)? *) acc ) (Lazy.force location_nodes) invariants ) @@ -572,8 +572,8 @@ struct Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in - match inv with - | `Lifted inv -> + match Invariant.to_exp inv with + | Some inv -> let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) let location_function = fundec.svar.vname in let location = Entry.location ~location:loc ~location_function in @@ -584,7 +584,7 @@ struct incr cnt_loop_invariant; invariant :: acc ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + | None -> (* TODO: 0 for bot (dead code)? *) acc ) else @@ -601,15 +601,15 @@ struct 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 -> + begin match Invariant.to_exp (R.ask_global (InvariantGlobal (Obj.repr g))) with + | Some 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 *) + | None -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *) acc end | `Right _ -> (* global unknown for FromSpec contexts *)