diff --git a/.gitignore b/.gitignore index 480839d17e..512c8f865e 100644 --- a/.gitignore +++ b/.gitignore @@ -44,6 +44,7 @@ _opam/ cfgs/ cfg.dot cilcfg.*.dot +arg.dot *.graphml goblint.bc.js diff --git a/src/framework/control.ml b/src/framework/control.ml index 7f5b3040e6..665e29e479 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -12,6 +12,7 @@ module type S2S = functor (X : Spec) -> Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; + let arg_enabled = get_bool "ana.sv-comp.enabled" || get_bool "exp.arg" in let open Batteries in (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in @@ -19,10 +20,10 @@ let spec_module: (module Spec) Lazy.t = lazy ( (module MCP.MCP2 : Spec) |> lift true (module WidenContextLifterSide) (* option checked in functor *) (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *) - |> lift (get_bool "ana.opt.hashcons" || get_bool "ana.sv-comp.enabled") (module HashconsContextLifter) - |> lift (get_bool "ana.sv-comp.enabled") (module HashconsLifter) - |> lift (get_bool "ana.sv-comp.enabled") (module WitnessConstraints.PathSensitive3) - |> lift (not (get_bool "ana.sv-comp.enabled")) (module PathSensitive2) + |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter) + |> lift arg_enabled (module HashconsLifter) + |> lift arg_enabled (module WitnessConstraints.PathSensitive3) + |> lift (not arg_enabled) (module PathSensitive2) |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter) |> lift true (module DeadCodeLifter) |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter) @@ -658,6 +659,23 @@ struct in Timing.wrap "warn_global" (GHT.iter warn_global) gh; + if get_bool "exp.arg" then ( + let module ArgTool = ArgTools.Make (R) in + let module Arg = (val ArgTool.create entrystates) in + if get_bool "exp.argdot" then ( + let module ArgDot = ArgTools.Dot (Arg) in + let oc = Stdlib.open_out "arg.dot" in + Fun.protect (fun () -> + let ppf = Format.formatter_of_out_channel oc in + ArgDot.dot ppf; + Format.pp_print_flush ppf () + ) ~finally:(fun () -> + Stdlib.close_out oc + ) + ); + ArgTools.current_arg := Some (module Arg); + ); + (* Before SV-COMP, so result can depend on YAML witness validation. *) if get_string "witness.yaml.validate" <> "" then ( let module YWitness = YamlWitness.Validator (R) in diff --git a/src/framework/edge.ml b/src/framework/edge.ml index 6202f6bd31..045bfb8dbf 100644 --- a/src/framework/edge.ml +++ b/src/framework/edge.ml @@ -29,7 +29,7 @@ type t = * appeared *) | Skip (** This is here for historical reasons. I never use Skip edges! *) -[@@deriving eq, ord, hash, to_yojson] +[@@deriving eq, ord, hash] let pretty () = function @@ -55,3 +55,56 @@ let pretty_plain () = function | ASM _ -> text "ASM ..." | Skip -> text "Skip" | VDecl v -> dprintf "VDecl '%a %s;'" d_type v.vtype v.vname + +let to_yojson e = + let fields = match e with + | Assign (lval, exp) -> + [ + ("type", `String "assign"); + ("lval", CilType.Lval.to_yojson lval); + ("exp", CilType.Exp.to_yojson exp); + ] + | Test (exp, branch) -> + [ + ("type", `String "branch"); + ("exp", CilType.Exp.to_yojson exp); + ("branch", `Bool branch); + ] + | Proc (lval, function_, args) -> + [ + ("type", `String "call"); + ("lval", [%to_yojson: CilType.Lval.t option] lval); + ("function", CilType.Exp.to_yojson function_); + ("args", [%to_yojson: CilType.Exp.t list] args); + ] + | Entry function_ -> + [ + ("type", `String "entry"); + ("function", CilType.Fundec.to_yojson function_); + ] + | Ret (exp, function_) -> + [ + ("type", `String "return"); + ("function", CilType.Fundec.to_yojson function_); + ("exp", [%to_yojson: CilType.Exp.t option] exp); + ] + | ASM (instructions, output, input) -> + [ + ("type", `String "asm"); + ("instructions", [%to_yojson: string list] instructions); + ("output", asm_out_to_yojson output); + ("input", asm_in_to_yojson input); + ] + | VDecl variable -> + [ + ("type", `String "declare"); + ("variable", CilType.Varinfo.to_yojson variable); + ] + | Skip -> + [ + ("type", `String "nop"); + ] + in + `Assoc ([ + ("string", `String (Pretty.sprint ~width:max_int (pretty () e))) + ] @ fields) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index c3346677d6..a2a96aec45 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1634,6 +1634,18 @@ "description": "Hide standard extern globals (e.g. `stdout`) from cluttering local states.", "type": "boolean", "default": true + }, + "arg": { + "title": "exp.arg", + "description": "Construct abstract reachability graph (ARG).", + "type": "boolean", + "default": false + }, + "argdot": { + "title": "exp.argdot", + "description": "Output ARG as dot file.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/src/util/server.ml b/src/util/server.ml index 486ee9fa39..7a9c793e33 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -2,9 +2,19 @@ open Batteries open Jsonrpc open GoblintCil +module type ArgWrapper = +sig + module Arg: ArgTools.BiArg + module Locator: module type of WitnessUtil.Locator (Arg.Node) + val locator: Locator.t + val find_node: string -> Arg.Node.t + val find_cfg_node: string -> Arg.Node.t list +end + type t = { mutable file: Cil.file option; mutable max_ids: MaxIdUtil.max_ids; + arg_wrapper: (module ArgWrapper) ResettableLazy.t; input: IO.input; output: unit IO.output; } @@ -106,6 +116,36 @@ let serve serv = |> Seq.map Packet.t_of_yojson |> Seq.iter (handle_packet serv) +let arg_wrapper: (module ArgWrapper) ResettableLazy.t = + ResettableLazy.from_fun (fun () -> + let module Arg = (val (Option.get_exn !ArgTools.current_arg Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or arg disabled" ())))) in + let module Locator = WitnessUtil.Locator (Arg.Node) in + let module StringH = Hashtbl.Make (Printable.Strings) in + + let locator = Locator.create () in + let ids = StringH.create 113 in + let cfg_nodes = StringH.create 113 in + Arg.iter_nodes (fun n -> + let cfgnode = Arg.Node.cfgnode n in + let loc = UpdateCil.getLoc cfgnode in + if not loc.synthetic then + Locator.add locator loc n; + StringH.replace ids (Arg.Node.to_string n) n; + StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *) + ); + + let module ArgWrapper = + struct + module Arg = Arg + module Locator = Locator + let locator = locator + let find_node = StringH.find ids + let find_cfg_node = StringH.find_all cfg_nodes + end + in + (module ArgWrapper: ArgWrapper) + ) + let make ?(input=stdin) ?(output=stdout) file : t = let max_ids = match file with @@ -115,6 +155,7 @@ let make ?(input=stdin) ?(output=stdout) file : t = { file; max_ids; + arg_wrapper; input; output } @@ -189,7 +230,7 @@ let node_locator: Locator.t ResettableLazy.t = let rec iter_node node = if not (NH.mem reachable node) then begin NH.replace reachable node (); - let loc = Node.location node in + let loc = UpdateCil.getLoc node in if not loc.synthetic then Locator.add locator loc node; List.iter (fun (_, prev_node) -> @@ -219,6 +260,7 @@ let analyze ?(reset=false) (s: t) = Serialize.Cache.reset_data AnalysisData); let increment_data, fresh = increment_data s file reparsed in ResettableLazy.reset node_locator; + ResettableLazy.reset s.arg_wrapper; Cilfacade.reset_lazy (); InvariantCil.reset_lazy (); WideningThresholds.reset_lazy (); @@ -389,7 +431,7 @@ let () = Response.Error.(raise (make ~code:RequestFailed ~message:"requires node xor location" ())) in let node_id = Node.show_id node in - let location = Node.location node in + let location = UpdateCil.getLoc node in let module Cfg = (val !MyCFG.current_cfg) in let next = Cfg.next node @@ -406,6 +448,100 @@ let () = {node = node_id; location; next; prev} end); + register (module struct + let name = "arg/lookup" + type params = { + node: string option [@default None]; + location: CilType.Location.t option [@default None]; + cfg_node: string option [@default None]; + } [@@deriving of_yojson] + + type edge_node = { + edge: MyARG.inline_edge; + node: string; + cfg_node: string; + context: string; + path: string; + location: CilType.Location.t; + } [@@deriving to_yojson] + type one_response = { + node: string; + cfg_node: string; + context: string; + path: string; + location: CilType.Location.t; + next: edge_node list; + prev: edge_node list; + } [@@deriving to_yojson] + type response = one_response list [@@deriving to_yojson] + + let process (params: params) serv = + let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in + let open ArgWrapper in + let open GobList.Syntax in + let+ n: Arg.Node.t = match params.node, params.location, params.cfg_node with + | None, None, None -> + [Arg.main_entry] + | Some node_id, None, None -> + begin try + [ArgWrapper.find_node node_id] + with Not_found -> + [] (* non-existent node *) + end + | None, Some location, None -> + let nodes_opt = + let open GobOption.Syntax in + let+ nodes = Locator.find_opt locator location in + Locator.ES.elements nodes + in + Option.default [] nodes_opt (* cannot find node for location *) + | None, None, Some cfg_node -> + ArgWrapper.find_cfg_node cfg_node + | _, _, _ -> + Response.Error.(raise (make ~code:RequestFailed ~message:"requires at most one of node, location and cfg_node" ())) + in + let cfg_node = Arg.Node.cfgnode n in + let cfg_node_id = Node.show_id cfg_node in + let location = UpdateCil.getLoc cfg_node in + let next = + Arg.next n + |> List.map (fun (edge, to_node) -> + let cfg_to_node = Arg.Node.cfgnode to_node in + { + edge; + node = Arg.Node.to_string to_node; + cfg_node = Node.show_id cfg_to_node; + context = string_of_int (Arg.Node.context_id to_node); + path = string_of_int (Arg.Node.path_id to_node); + location = UpdateCil.getLoc cfg_to_node; + } + ) + in + let prev = + Arg.prev n + |> List.map (fun (edge, to_node) -> + let cfg_to_node = Arg.Node.cfgnode to_node in + { + edge; + node = Arg.Node.to_string to_node; + cfg_node = Node.show_id cfg_to_node; + context = string_of_int (Arg.Node.context_id to_node); + path = string_of_int (Arg.Node.path_id to_node); + location = UpdateCil.getLoc cfg_to_node; + } + ) + in + { + node = Arg.Node.to_string n; + cfg_node = cfg_node_id; + context = string_of_int (Arg.Node.context_id n); + path = string_of_int (Arg.Node.path_id n); + location; + next; + prev + } + end); + register (module struct let name = "node_state" type params = { nid: string } [@@deriving of_yojson] diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml new file mode 100644 index 0000000000..6c6c9d4e4f --- /dev/null +++ b/src/witness/argTools.ml @@ -0,0 +1,156 @@ +open MyCFG + +module type BiArg = +sig + include MyARG.S with module Edge = MyARG.InlineEdge + + val prev: Node.t -> (Edge.t * Node.t) list + val iter_nodes: (Node.t -> unit) -> unit +end + +module Dot (Arg: BiArg) = +struct + let dot_node_name ppf node = + Format.fprintf ppf "\"%s\"" (Arg.Node.to_string node) + + let dot_edge ppf from_node (edge, to_node) = + Format.fprintf ppf "@,%a -> %a [label=\"%s\"];" dot_node_name from_node dot_node_name to_node (String.escaped (Arg.Edge.to_string edge)) + + let dot_node ppf node = + let shape = match Arg.Node.cfgnode node with + | Statement {skind=If (_,_,_,_,_); _} -> "diamond" + | Statement _ -> "oval" + | Function _ + | FunctionEntry _ -> "box" + in + Format.fprintf ppf "@,%a [shape=%s];" dot_node_name node shape; + List.iter (dot_edge ppf node) (Arg.next node) + + let dot_nodes ppf = + Arg.iter_nodes (dot_node ppf) + + let dot ppf = + Format.fprintf ppf "@[digraph arg {%t@]@,}@\n" dot_nodes +end + +let current_arg: (module BiArg) option ref = ref None + +module Make (R: ResultQuery.SpecSysSol2) = +struct + open R + open SpecSys + + module Query = ResultQuery.Query (SpecSys) + + let get: node * Spec.C.t -> Spec.D.t = + fun nc -> LHT.find_default lh nc (Spec.D.bot ()) + + let ask_indices lvar = + let indices = ref [] in + ignore (ask_local lvar (Queries.IterVars (fun i -> + indices := i :: !indices + ))); + !indices + + module CfgNode = Node + + module Node = + struct + type t = MyCFG.node * Spec.C.t * int + + let equal (n1, c1, i1) (n2, c2, i2) = + EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2 + + let compare (n1, c1, i1) (n2, c2, i2) = + let r = EQSys.LVar.compare (n1, c1) (n2, c2) in + if r <> 0 then + r + else + Int.compare i1 i2 + + let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i + + let cfgnode (n, c, i) = n + let context_id (n, c, i) = Spec.C.tag c + let path_id (n, c, i) = i + + let to_string (n, c, i) = + (* copied from NodeCtxStackGraphMlWriter *) + let c_tag = Spec.C.tag c in + let i_str = string_of_int i in + match n with + | Statement stmt -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str + | Function f -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str + | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str + + (* TODO: less hacky way (without ask_indices) to move node *) + let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c))) + let move_opt (n, c, i) to_n = + match ask_indices (to_n, c) with + | [] -> None + | [to_i] -> + let to_node = (to_n, c, to_i) in + BatOption.filter is_live (Some to_node) + | _ :: _ :: _ -> + failwith "Node.move_opt: ambiguous moved index" + let equal_node_context (n1, c1, i1) (n2, c2, i2) = + EQSys.LVar.equal (n1, c1) (n2, c2) + end + + module NHT = BatHashtbl.Make (Node) + + let create entrystates: (module BiArg with type Node.t = MyCFG.node * Spec.C.t * int) = + let (witness_prev_map, witness_prev, witness_next) = + let prev = NHT.create 100 in + let next = NHT.create 100 in + LHT.iter (fun lvar local -> + ignore (ask_local lvar ~local (Queries.IterPrevVars (fun i (prev_node, prev_c_obj, j) edge -> + let lvar' = (fst lvar, snd lvar, i) in + let prev_lvar: NHT.key = (prev_node, Obj.obj prev_c_obj, j) in + NHT.modify_def [] lvar' (fun prevs -> (edge, prev_lvar) :: prevs) prev; + NHT.modify_def [] prev_lvar (fun nexts -> (edge, lvar') :: nexts) next + ))) + ) lh; + + (prev, + (fun n -> + NHT.find_default prev n []), (* main entry is not in prev at all *) + (fun n -> + NHT.find_default next n [])) (* main return is not in next at all *) + in + let witness_main = + let lvar = WitnessUtil.find_main_entry entrystates in + let main_indices = ask_indices lvar in + (* TODO: get rid of this hack for getting index of entry state *) + assert (List.compare_length_with main_indices 1 = 0); + let main_index = List.hd main_indices in + (fst lvar, snd lvar, main_index) + in + + let module Arg = + struct + module Node = Node + module Edge = MyARG.InlineEdge + let main_entry = witness_main + let next = witness_next + end + in + let module Arg = + struct + open MyARG + module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg))) + include Intra (ArgIntra) (Arg) + + let prev = witness_prev + let iter_nodes f = + f main_entry; + NHT.iter (fun n _ -> + f n + ) witness_prev_map + end + in + (module Arg: BiArg with type Node.t = MyCFG.node * Spec.C.t * int) + + let create entrystates = + Timing.wrap "arg create" create entrystates +end diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml index a4ffeef5bd..330ae07909 100644 --- a/src/witness/myARG.ml +++ b/src/witness/myARG.ml @@ -4,8 +4,11 @@ open GoblintCil module type Node = sig include Hashtbl.HashedType + include Set.OrderedType with type t := t val cfgnode: t -> MyCFG.node + val context_id: t -> int + val path_id: t -> int val to_string: t -> string val move_opt: t -> MyCFG.node -> t option @@ -30,15 +33,43 @@ end type inline_edge = | CFGEdge of Edge.t - | InlineEntry of CilType.Exp.t list - | InlineReturn of CilType.Lval.t option -[@@deriving eq, ord, hash, to_yojson] + | InlineEntry of CilType.Lval.t option * CilType.Fundec.t * CilType.Exp.t list + | InlineReturn of CilType.Lval.t option * CilType.Fundec.t * CilType.Exp.t list + | InlinedEdge of Edge.t +[@@deriving eq, ord, hash] let pretty_inline_edge () = function | CFGEdge e -> Edge.pretty_plain () e - | InlineEntry args -> Pretty.dprintf "InlineEntry '(%a)'" (Pretty.d_list ", " Cil.d_exp) args - | InlineReturn None -> Pretty.dprintf "InlineReturn" - | InlineReturn (Some ret) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret + | InlineEntry (_, _, args) -> Pretty.dprintf "InlineEntry '(%a)'" (Pretty.d_list ", " Cil.d_exp) args + | InlineReturn (None, _, _) -> Pretty.dprintf "InlineReturn" + | InlineReturn (Some ret, _, _) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret + | InlinedEdge e -> Pretty.dprintf "Inlined %a" Edge.pretty_plain e + +let inline_edge_to_yojson = function + | CFGEdge e -> + `Assoc [ + ("cfg", Edge.to_yojson e) + ] + | InlineEntry (lval, function_, args) -> + `Assoc [ + ("entry", `Assoc [ + ("lval", [%to_yojson: CilType.Lval.t option] lval); + ("function", CilType.Fundec.to_yojson function_); + ("args", [%to_yojson: CilType.Exp.t list] args); + ]); + ] + | InlineReturn (lval, function_, args) -> + `Assoc [ + ("return", `Assoc [ + ("lval", [%to_yojson: CilType.Lval.t option] lval); + ("function", CilType.Fundec.to_yojson function_); + ("args", [%to_yojson: CilType.Exp.t list] args); + ]); + ] + | InlinedEdge e -> + `Assoc [ + ("inlined", Edge.to_yojson e) + ] module InlineEdgePrintable: Printable.S with type t = inline_edge = struct @@ -78,9 +109,11 @@ end module StackNode (Node: Node): Node with type t = Node.t list = struct - type t = Node.t list [@@deriving eq, hash] + type t = Node.t list [@@deriving eq, ord, hash] let cfgnode nl = Node.cfgnode (List.hd nl) + let context_id nl = Node.context_id (List.hd nl) + let path_id nl = Node.path_id (List.hd nl) let to_string nl = nl |> List.map Node.to_string diff --git a/src/witness/violation.ml b/src/witness/violation.ml index 51952bb3c9..a3aec7d25f 100644 --- a/src/witness/violation.ml +++ b/src/witness/violation.ml @@ -94,8 +94,13 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod else if not (NHT.mem itered_nodes node) then begin NHT.replace itered_nodes node (); List.iter (fun (edge, prev_node) -> - if not (NHT.mem itered_nodes prev_node) then - NHT.replace next_nodes prev_node (edge, node) + match edge with + | MyARG.CFGEdge _ + | InlineEntry _ + | InlineReturn _ -> + if not (NHT.mem itered_nodes prev_node) then + NHT.replace next_nodes prev_node (edge, node) + | InlinedEdge _ -> () ) (Arg.prev node); bfs curs' (List.map snd (Arg.prev node) @ nexts) end diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 937f83473f..400016d516 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -231,11 +231,20 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) (* TODO: keep control (Test) edges to dead (sink) nodes for violation witness? *) in List.iter (fun (edge, to_node) -> - write_node to_node; - write_edge node edge to_node + match edge with + | MyARG.CFGEdge _ + | InlineEntry _ + | InlineReturn _ -> + write_node to_node; + write_edge node edge to_node + | InlinedEdge _ -> () ) edge_to_nodes; List.iter (fun (edge, to_node) -> - iter_node to_node + match edge with + | MyARG.CFGEdge _ + | InlineEntry _ + | InlineReturn _ -> iter_node to_node + | InlinedEdge _ -> () ) edge_to_nodes end end @@ -271,100 +280,11 @@ struct open Svcomp module Query = ResultQuery.Query (SpecSys) + module ArgTool = ArgTools.Make (R) + module NHT = ArgTool.NHT let determine_result entrystates (module Task:Task): (module WitnessTaskResult) = - let get: node * Spec.C.t -> Spec.D.t = - fun nc -> LHT.find_default lh nc (Spec.D.bot ()) - in - let ask_indices lvar = - let indices = ref [] in - ignore (ask_local lvar (Queries.IterVars (fun i -> - indices := i :: !indices - ))); - !indices - in - - let module CfgNode = Node in - - let module Node = - struct - type t = MyCFG.node * Spec.C.t * int - - let equal (n1, c1, i1) (n2, c2, i2) = - EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2 - - let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i - - let cfgnode (n, c, i) = n - - let to_string (n, c, i) = - (* copied from NodeCtxStackGraphMlWriter *) - let c_tag = Spec.C.tag c in - let i_str = string_of_int i in - match n with - | Statement stmt -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str - | Function f -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str - | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str - - (* TODO: less hacky way (without ask_indices) to move node *) - let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c))) - let move_opt (n, c, i) to_n = - match ask_indices (to_n, c) with - | [] -> None - | [to_i] -> - let to_node = (to_n, c, to_i) in - BatOption.filter is_live (Some to_node) - | _ :: _ :: _ -> - failwith "Node.move_opt: ambiguous moved index" - let equal_node_context (n1, c1, i1) (n2, c2, i2) = - EQSys.LVar.equal (n1, c1) (n2, c2) - end - in - - let module NHT = BatHashtbl.Make (Node) in - - let (witness_prev_map, witness_prev, witness_next) = - let prev = NHT.create 100 in - let next = NHT.create 100 in - LHT.iter (fun lvar local -> - ignore (ask_local lvar ~local (Queries.IterPrevVars (fun i (prev_node, prev_c_obj, j) edge -> - let lvar' = (fst lvar, snd lvar, i) in - let prev_lvar: NHT.key = (prev_node, Obj.obj prev_c_obj, j) in - NHT.modify_def [] lvar' (fun prevs -> (edge, prev_lvar) :: prevs) prev; - NHT.modify_def [] prev_lvar (fun nexts -> (edge, lvar') :: nexts) next - ))) - ) lh; - - (prev, - (fun n -> - NHT.find_default prev n []), (* main entry is not in prev at all *) - (fun n -> - NHT.find_default next n [])) (* main return is not in next at all *) - in - let witness_main = - let lvar = WitnessUtil.find_main_entry entrystates in - let main_indices = ask_indices lvar in - (* TODO: get rid of this hack for getting index of entry state *) - assert (List.compare_length_with main_indices 1 = 0); - let main_index = List.hd main_indices in - (fst lvar, snd lvar, main_index) - in - - let module Arg = - struct - module Node = Node - module Edge = MyARG.InlineEdge - let main_entry = witness_main - let next = witness_next - end - in - let module Arg = - struct - open MyARG - module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg))) - include Intra (ArgIntra) (Arg) - end - in + let module Arg = (val ArgTool.create entrystates) in let find_invariant (n, c, i) = let context = {Invariant.default_context with path = Some i} in @@ -407,18 +327,18 @@ struct |> List.exists (fun (_, to_n) -> is_violation to_n) in let violations = - NHT.fold (fun lvar _ acc -> + (* TODO: fold_nodes?s *) + let acc = ref [] in + Arg.iter_nodes (fun lvar -> if is_violation lvar then - lvar :: acc - else - acc - ) witness_prev_map [] + acc := lvar :: !acc + ); + !acc in let module ViolationArg = struct include Arg - let prev = witness_prev let violations = violations end in diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml index 60469adc9a..68a28a0e23 100644 --- a/src/witness/witnessConstraints.ml +++ b/src/witness/witnessConstraints.ml @@ -137,6 +137,7 @@ struct with Ctx_failure _ -> R.bot () let step_ctx_edge ctx x = step_ctx ctx x (CFGEdge ctx.edge) + let step_ctx_inlined_edge ctx x = step_ctx ctx x (InlinedEdge ctx.edge) let map ctx f g = (* we now use Sync for every tf such that threadspawn after tf could look up state before tf *) @@ -237,7 +238,7 @@ struct (* R.bot () isn't right here? doesn't actually matter? *) let yr = if should_inline f then - step_ctx ctx x' (InlineEntry a) + step_ctx ctx x' (InlineEntry (l, f, a)) else R.bot () in @@ -257,7 +258,9 @@ struct if should_inline f then let nosync = (Sync.singleton x (SyncSet.singleton x)) in (* returns already post-sync in FromSpec *) - step (Function f) (Option.get fc) x (InlineReturn l) nosync (* fc should be Some outside of MCP *) + let returnr = step (Function f) (Option.get fc) x (InlineReturn (l, f, a)) nosync in (* fc should be Some outside of MCP *) + let procr = step_ctx_inlined_edge ctx cd in + R.join procr returnr else step_ctx_edge ctx cd in