Merge branch 'yaml-witness-test' into yaml-witness-ghost

conf/svcomp.json

@@ -84,7 +84,6 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic",
         "memsafetySpecification",
         "termination",
         "tmpSpecialAnalysis"

goblint.opam

@@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

goblint.opam.locked

@@ -134,7 +134,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
+    "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6"
   ]
   [
     "ppx_deriving.5.2.1"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

src/analyses/unassumeAnalysis.ml

@@ -27,7 +27,7 @@ struct
 
   module Locator = WitnessUtil.Locator (Node)
 
-  let locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
+  let location_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
   let loop_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
 
   type inv = {
@@ -41,26 +41,26 @@ struct
   let pre_invs: inv EH.t NH.t = NH.create 100
 
   let init _ =
-    Locator.clear locator;
+    Locator.clear location_locator;
     Locator.clear loop_locator;
     let module FileCfg =
     struct
       let file = !Cilfacade.current_file
       module Cfg = (val !MyCFG.current_cfg)
     end  in
-    let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in
+    let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
 
     (* DFS, copied from CfgTools.find_backwards_reachable *)
     let reachable = NH.create 100 in
     let rec iter_node node =
       if not (NH.mem reachable node) then begin
         NH.replace reachable node ();
-        (* TODO: filter synthetic?
-           See YamlWitness. *)
-        if WitnessInvariant.is_invariant_node node then
-          Locator.add locator (Node.location node) node;
-        if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
-          Locator.add loop_locator (Node.location node) node;
+        Option.iter (fun loc ->
+            Locator.add location_locator loc node
+          ) (WitnessInvariant.location_location node);
+        Option.iter (fun loc ->
+            Locator.add loop_locator loc node
+          ) (WitnessInvariant.loop_location node);
         List.iter (fun (_, prev_node) ->
             iter_node prev_node
           ) (FileCfg.Cfg.prev node)
@@ -130,7 +130,7 @@ struct
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt location_locator loc with
         | Some nodes ->
           unassume_nodes_invariant ~loc ~nodes inv
         | None ->
@@ -193,7 +193,7 @@ struct
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
-        match Locator.find_opt locator loc with
+        match Locator.find_opt loop_locator loc with
         | Some nodes ->
           unassume_precondition_nodes_invariant ~loc ~nodes pre inv
         | None ->
@@ -207,7 +207,7 @@ struct
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
-          match Locator.find_opt locator loc with
+          match Locator.find_opt location_locator loc with
           | Some nodes ->
             unassume_nodes_invariant ~loc ~nodes inv
           | None ->

src/common/framework/cfgTools.ml

@@ -132,13 +132,7 @@ let () = Printexc.register_printer (function
     | _ -> None (* for other exceptions *)
   )
 
-(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
-    along with the list of connecting instructions. *)
-module CfgEdge = struct
-  type t = Node.t * MyCFG.edges * Node.t [@@deriving eq, hash]
-end
 
-module CfgEdgeH = BatHashtbl.Make (CfgEdge)
 
 let createCFG (file: file) =
   let cfgF = H.create 113 in
@@ -254,7 +248,7 @@ let createCFG (file: file) =
         let pseudo_return = lazy (
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
           let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
-          let newst = mkStmt (Return (None, fd_end_loc)) in
+          let newst = mkStmt (Return (None, fd_end_loc, locUnknown)) in
           newst.sid <- Cilfacade.get_pseudo_return_id fd;
           Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
@@ -340,8 +334,8 @@ let createCFG (file: file) =
             (* CIL's xform_switch_stmt (via prepareCFG) always adds both continue and break statements to all Loops. *)
             failwith "MyCFG.createCFG: unprepared Loop"
 
-          | Return (exp, loc) ->
-            addEdge (Statement stmt) (loc, Ret (exp, fd)) (Function fd)
+          | Return (exp, loc, eloc) ->
+            addEdge (Statement stmt) (Cilfacade.eloc_fallback ~eloc ~loc, Ret (exp, fd)) (Function fd)
 
           | Goto (_, loc) ->
             (* Gotos are generally unnecessary and unwanted because find_real_stmt skips over these. *)
@@ -608,7 +602,7 @@ let fprint_hash_dot cfg  =
   close_out out
 
 
-let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
+let getCFG (file: file) : cfg * cfg * _ =
   let cfgF, cfgB, skippedByEdge = createCFG file in
   let cfgF, cfgB, skippedByEdge =
     if get_bool "exp.mincfg" then
@@ -617,13 +611,11 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
       (cfgF, cfgB, skippedByEdge)
   in
   if get_bool "justcfg" then fprint_hash_dot cfgB;
-  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge
+  (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), (fun u e v -> CfgEdgeH.find skippedByEdge (u, e, v))
 
-let compute_cfg_skips file =
+let compute_cfg file =
   let cfgF, cfgB, skippedByEdge = getCFG file in
-  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
-
-let compute_cfg file = fst (compute_cfg_skips file)
+  (module struct let prev = cfgB let next = cfgF let skippedByEdge = skippedByEdge end : CfgBidirSkip)
 
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =

src/common/framework/myCFG.ml

@@ -42,19 +42,34 @@ sig
   include CfgForward
 end
 
+(** Type of CFG "edges": keyed by 'from' and 'to' nodes,
+    along with the list of connecting instructions. *)
+module CfgEdge = struct
+  type t = Node.t * edges * Node.t [@@deriving eq, hash]
+end
+
+module CfgEdgeH = BatHashtbl.Make (CfgEdge)
+
+module type CfgBidirSkip =
+sig
+  include CfgBidir
+  val skippedByEdge: node -> edges -> node -> stmt list
+end
+
 
 module NodeH = BatHashtbl.Make (Node)
 
 
 let current_node = Node.current_node
-let current_cfg : (module CfgBidir) ref =
+let current_cfg : (module CfgBidirSkip) ref =
   let module Cfg =
   struct
     let next _ = raise Not_found
     let prev _ = raise Not_found
+    let skippedByEdge _ _ _ = raise Not_found
   end
   in
-  ref (module Cfg: CfgBidir)
+  ref (module Cfg: CfgBidirSkip)
 
 let unknown_exp : exp = mkString "__unknown_value__"
 let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)
@@ -64,5 +79,5 @@ let dummy_node = FunctionEntry Cil.dummyFunDec
 module type FileCfg =
 sig
   val file: Cil.file
-  module Cfg: CfgBidir
+  module Cfg: CfgBidirSkip
 end

src/common/util/cilLocation.ml

@@ -34,7 +34,7 @@ let rec get_stmtLoc stmt: locs =
     {loc = locUnknown; eloc = locUnknown}
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> {loc; eloc = locUnknown}
+  | Return (_, loc, eloc) -> {loc; eloc}
   | Goto (_, loc) -> {loc; eloc = locUnknown}
   | ComputedGoto (_, loc) -> {loc; eloc = locUnknown}
   | Break loc -> {loc; eloc = locUnknown}

src/common/util/cilfacade.ml

@@ -494,7 +494,7 @@ class countFnVisitor = object
   inherit nopCilVisitor
   method! vstmt s =
     match s.skind with
-    | Return (_, loc)
+    | Return (_, loc, _)
     | Goto (_, loc)
     | ComputedGoto (_, loc)
     | Break loc

src/common/util/cilfacade0.ml

@@ -42,7 +42,7 @@ let rec get_stmtLoc stmt =
     get_labelsLoc stmt.labels
 
   | Instr (hd :: _) -> get_instrLoc hd
-  | Return (_, loc) -> loc
+  | Return (_, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Goto (_, loc) -> loc
   | ComputedGoto (_, loc) -> loc
   | Break loc -> loc

src/framework/control.ml

@@ -54,7 +54,7 @@ let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _
 let current_varquery_global_state_json: (VarQuery.t option -> Yojson.Safe.t) ref = ref (fun _ -> `Null)
 
 (** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
-module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) =
+module AnalyzeCFG (Cfg:CfgBidirSkip) (Spec:Spec) (Inc:Increment) =
 struct
 
   module SpecSys: SpecSys with module Spec = Spec =
@@ -230,7 +230,7 @@ struct
     res
 
   (** The main function to preform the selected analyses. *)
-  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) skippedByEdge =
+  let analyze (file: file) (startfuns, exitfuns, otherfuns: Analyses.fundecs) =
     let module FileCfg: FileCfg =
     struct
       let file = file
@@ -625,13 +625,16 @@ struct
            let node_values = LHT.enum lh |> map (Tuple2.map1 fst) in (* drop context from key *)
            let hashtbl_size = if fast_count node_values then count node_values else 123 in
            let by_loc, by_node = Hashtbl.create hashtbl_size, NodeH.create hashtbl_size in
-           node_values |> iter (fun (node, v) ->
-               let loc = Node.location node in
-               (* join values once for the same location and once for the same node *)
-               let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
-               Hashtbl.modify_opt loc join by_loc;
-               NodeH.modify_opt node join by_node;
-             );
+           iter (fun (node, v) ->
+              let loc = match node with
+                | Statement s -> Cil.get_stmtLoc s.skind (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
+                | FunctionEntry _ | Function _ -> Node.location node
+              in
+              (* join values once for the same location and once for the same node *)
+              let join = Option.some % function None -> v | Some v' -> Spec.D.join v v' in
+              Hashtbl.modify_opt loc join by_loc;
+              NodeH.modify_opt node join by_node;
+            ) node_values;
            by_loc, by_node
         in
 
@@ -656,7 +659,10 @@ struct
         let must_be_uncalled fd = not @@ BatSet.Int.mem fd.svar.vid calledFuns in
 
         let skipped_statements from_node edge to_node =
-          CfgTools.CfgEdgeH.find_default skippedByEdge (from_node, edge, to_node) []
+          try
+            Cfg.skippedByEdge from_node edge to_node
+          with Not_found ->
+            []
         in
 
         Transform.run_transformations file active_transformations
@@ -793,22 +799,22 @@ end
    [analyze_loop] cannot reside in it anymore since each invocation of
    [get_spec] in the loop might/should return a different module, and we
    cannot swap the functor parameter from inside [AnalyzeCFG]. *)
-let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge =
+let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info =
   try
     let (module Spec) = get_spec () in
     let module A = AnalyzeCFG (CFG) (Spec) (struct let increment = change_info end) in
-    GobConfig.with_immutable_conf (fun () -> A.analyze file fs skippedByEdge)
+    GobConfig.with_immutable_conf (fun () -> A.analyze file fs)
   with Refinement.RestartAnalysis ->
     (* Tail-recursively restart the analysis again, when requested.
         All solving starts from scratch.
         Whoever raised the exception should've modified some global state
         to do a more precise analysis next time. *)
     (* TODO: do some more incremental refinement and reuse parts of solution *)
-    analyze_loop (module CFG) file fs change_info skippedByEdge
+    analyze_loop (module CFG) file fs change_info
 
 (** The main function to perform the selected analyses. *)
 let analyze change_info (file: file) fs =
   Logs.debug "Generating the control flow graph.";
-  let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in
+  let (module CFG) = CfgTools.compute_cfg file in
   MyCFG.current_cfg := (module CFG);
-  analyze_loop (module CFG) file fs change_info skippedByEdge
+  analyze_loop (module CFG) file fs change_info

src/incremental/compareAST.ml

@@ -339,8 +339,8 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   let eq_block' = fun x y ~(rename_mapping:rename_mapping) -> if cfg_comp then true, rename_mapping else eq_block (x, af) (y, bf) ~rename_mapping in
   match a, b with
   | Instr is1, Instr is2 -> forward_list_equal eq_instr is1 is2 ~rename_mapping
-  | Return (Some exp1, _l1), Return (Some exp2, _l2) -> eq_exp exp1 exp2 ~rename_mapping
-  | Return (None, _l1), Return (None, _l2) -> true, rename_mapping
+  | Return (Some exp1, _l1, _el1), Return (Some exp2, _l2, _el2) -> eq_exp exp1 exp2 ~rename_mapping
+  | Return (None, _l1, _el1), Return (None, _l2, _el2) -> true, rename_mapping
   | Return _, Return _ -> false, rename_mapping
   | Goto (st1, _l1), Goto (st2, _l2) -> eq_stmt_with_location (!st1, af) (!st2, bf), rename_mapping
   | Break _, Break _ -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else true, rename_mapping

src/maingoblint.ml

@@ -147,6 +147,8 @@ let check_arguments () =
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
   if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitely disabled by activating the \"assert\" tranformation.");
   if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.");
+  if (get_int "exp.unrolling-factor" > 0 || AutoTune0.isActivated "loopUnrollHeuristic") && (get_bool "witness.yaml.enabled" || get_string "witness.yaml.validate" <> "" || get_string "witness.yaml.unassume" <> "") then
+    fail "YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370).";
   if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
     (* 'assert' transform happens before 'remove_dead_code' transform *)
     ignore @@ List.fold_left

src/transform/expressionEvaluation.ml

@@ -68,7 +68,7 @@ struct
         (* Take all statements *)
         |> List.concat_map (fun (f : Cil.fundec) -> f.sallstmts |> List.map (fun s -> f, s))
         (* Add locations *)
-        |> List.map (fun (f, (s : Cil.stmt)) -> (Cilfacade.get_stmtLoc s, f, s))
+        |> List.map (fun (f, (s : Cil.stmt)) -> (Cil.get_stmtLoc s.skind, f, s)) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
         (* Filter artificial ones by impossible location *)
         |> List.filter (fun ((l : Cil.location), _, _) -> l.line >= 0)
         (* Create hash table *)
@@ -109,7 +109,7 @@ struct
                         fun (s : Cil.stmt) ->
                           succeeding_statement := Some s;
                           (* Evaluate at (directly before) a succeeding location *)
-                          Some(self#try_ask (Cilfacade.get_stmtLoc s) expression)
+                          Some(self#try_ask (Cil.get_stmtLoc s.skind) expression) (* nosemgrep: cilfacade *) (* Must use CIL's because syntactic search is in CIL. *)
                       end
                       statement.succs
                 with Not_found -> None

src/util/server.ml

@@ -121,6 +121,10 @@ let serve serv =
   |> Seq.map Packet.t_of_yojson
   |> Seq.iter (handle_packet serv)
 
+let is_server_node cfgnode =
+  let loc = UpdateCil.getLoc cfgnode in
+  not loc.synthetic
+
 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
@@ -133,7 +137,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
       Arg.iter_nodes (fun n ->
           let cfgnode = Arg.Node.cfgnode n in
           let loc = UpdateCil.getLoc cfgnode in
-          if not loc.synthetic then
+          if is_server_node cfgnode 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 *)
@@ -248,7 +252,7 @@ let node_locator: Locator.t ResettableLazy.t =
         if not (NH.mem reachable node) then begin
           NH.replace reachable node ();
           let loc = UpdateCil.getLoc node in
-          if not loc.synthetic then
+          if is_server_node node then
             Locator.add locator loc node;
           List.iter (fun (_, prev_node) ->
               iter_node prev_node
@@ -486,7 +490,7 @@ let () =
     let process { fname } serv =
       let fundec = Cilfacade.find_name_fundec fname in
       let live _ = true in (* TODO: fix this *)
-      let cfg = CfgTools.sprint_fundec_html_dot !MyCFG.current_cfg live fundec in
+      let cfg = CfgTools.sprint_fundec_html_dot (module (val !MyCFG.current_cfg: MyCFG.CfgBidirSkip): MyCFG.CfgBidir) live fundec in
       { cfg }
   end);