Merge branch 'master' into yaml-witness-2.1

Author: sim642

.github/workflows/coverage.yml

@@ -66,7 +66,7 @@ jobs:
           COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
           PULL_REQUEST_NUMBER: ${{ github.event.number }}
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: suite_result

.github/workflows/locked.yml

@@ -60,7 +60,7 @@ jobs:
       - name: Test
         run: opam exec -- dune runtest
 
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v5
         if: always()
         with:
           name: suite_result-${{ matrix.os }}

conf/svcomp-ghost.json

@@ -117,8 +117,10 @@
       "sv-comp-true-only": false,
       "format-version": "2.1",
       "entry-types": [
-        "flow_insensitive_invariant",
         "ghost_instrumentation"
+      ],
+      "invariant-types": [
+        "flow_insensitive_invariant"
       ]
     },
     "invariant": {

conf/svcomp-validate.json

@@ -98,8 +98,6 @@
       "strict": true,
       "format-version": "2.0",
       "entry-types": [
-        "location_invariant",
-        "loop_invariant",
         "invariant_set",
         "violation_sequence"
       ],

conf/svcomp24-validate.json

@@ -117,8 +117,6 @@
       "strict": true,
       "format-version": "2.0",
       "entry-types": [
-        "location_invariant",
-        "loop_invariant",
         "invariant_set"
       ],
       "invariant-types": [

conf/svcomp25-validate.json

@@ -98,8 +98,6 @@
       "strict": true,
       "format-version": "2.0",
       "entry-types": [
-        "location_invariant",
-        "loop_invariant",
         "invariant_set",
         "violation_sequence"
       ],

src/analyses/unassumeAnalysis.ml

@@ -7,21 +7,12 @@ open Analyses
 module Cil = GoblintCil.Cil
 
 module NH = CfgTools.NH
-module FH = Hashtbl.Make (CilType.Fundec)
-module EH = Hashtbl.Make (CilType.Exp)
 
 module Spec =
 struct
-  (* TODO: Should be context-sensitive? Some spurious widening in knot_comb fails self-validation after self-unassume. *)
-  include Analyses.IdentityUnitContextsSpec
+  include UnitAnalysis.Spec
   let name () = "unassume"
 
-  module D = SetDomain.Make (CilType.Exp)
-
-  let startstate _ = D.empty ()
-  let morphstate _ _ = D.empty ()
-  let exitstate _ = D.empty ()
-
   module Locator = WitnessUtil.Locator (Node)
 
   let location_locator: Locator.t = Locator.create () (* empty default, so don't have to use option everywhere *)
@@ -34,9 +25,6 @@ struct
 
   let invs: inv NH.t = NH.create 100
 
-  let fun_pres: Cil.exp FH.t = FH.create 100
-  let pre_invs: inv EH.t NH.t = NH.create 100
-
   let init _ =
     Locator.clear location_locator;
     Locator.clear loop_locator;
@@ -83,8 +71,6 @@ struct
     let inv_parser = InvariantParser.create !Cilfacade.current_file in
 
     NH.clear invs;
-    FH.clear fun_pres;
-    NH.clear pre_invs;
 
     let unassume_entry (entry: YamlWitnessType.Entry.t) =
       let uuid = entry.metadata.uuid in
@@ -112,81 +98,6 @@ struct
           M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv
       in
 
-      let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
-        let loc = YamlWitness.loc_of_location location_invariant.location in
-        let inv = location_invariant.location_invariant.string in
-        let msgLoc: M.Location.t = CilLocation loc in
-
-        match Locator.find_opt location_locator loc with
-        | Some nodes ->
-          unassume_nodes_invariant ~loc ~nodes inv
-        | None ->
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
-      in
-
-      let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
-        let loc = YamlWitness.loc_of_location loop_invariant.location in
-        let inv = loop_invariant.loop_invariant.string in
-        let msgLoc: M.Location.t = CilLocation loc in
-
-        match Locator.find_opt loop_locator loc with
-        | Some nodes ->
-          unassume_nodes_invariant ~loc ~nodes inv
-        | None ->
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
-      in
-
-      let unassume_precondition_nodes_invariant ~loc ~nodes pre inv =
-        let msgLoc: M.Location.t = CilLocation loc in
-        match InvariantParser.parse_cabs pre, InvariantParser.parse_cabs inv with
-        | Ok pre_cabs, Ok inv_cabs ->
-
-          Locator.ES.iter (fun n ->
-              let fundec = Node.find_fundec n in
-
-              match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc pre_cabs with
-              | Ok pre_exp ->
-                M.debug ~category:Witness ~loc:msgLoc "located precondition to %a: %a" CilType.Fundec.pretty fundec Cil.d_exp pre_exp;
-                FH.add fun_pres fundec pre_exp;
-
-                begin match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
-                  | Ok inv_exp ->
-                    M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
-                    if not (NH.mem pre_invs n) then
-                      NH.replace pre_invs n (EH.create 10);
-                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)}
-                  | Error e ->
-                    M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
-                    M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
-                end
-
-              | Error e ->
-                M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse precondition: %s" pre;
-                M.info ~category:Witness ~loc:msgLoc "precondition has undefined variables or side effects: %s" pre
-            ) nodes;
-
-        | Error e, _ ->
-          M.error ~category:Witness ~loc:msgLoc "Frontc couldn't parse precondition: %s" pre;
-          M.info ~category:Witness ~loc:msgLoc "precondition has invalid syntax: %s" pre
-
-        | _, Error e ->
-          M.error ~category:Witness ~loc:msgLoc "Frontc couldn't parse invariant: %s" inv;
-          M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv
-      in
-
-      let unassume_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) =
-        let loc = YamlWitness.loc_of_location precondition_loop_invariant.location in
-        let pre = precondition_loop_invariant.precondition.string in
-        let inv = precondition_loop_invariant.loop_invariant.string in
-        let msgLoc: M.Location.t = CilLocation loc in
-
-        match Locator.find_opt loop_locator loc with
-        | Some nodes ->
-          unassume_precondition_nodes_invariant ~loc ~nodes pre inv
-        | None ->
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
-      in
-
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
@@ -239,15 +150,9 @@ struct
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
-      | true, LocationInvariant x ->
-        unassume_location_invariant x
-      | true, LoopInvariant x ->
-        unassume_loop_invariant x
-      | true, PreconditionLoopInvariant x ->
-        unassume_precondition_loop_invariant x
       | true, InvariantSet x ->
         unassume_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
+      | false, InvariantSet _ ->
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
         M.warn_noloc ~category:Witness "cannot unassume entry of type %s" target_type
@@ -261,12 +166,6 @@ struct
 
   let emit_unassume man =
     let es = NH.find_all invs man.node in
-    let es = D.fold (fun pre acc ->
-        match NH.find_option pre_invs man.node with
-        | Some eh -> EH.find_all eh pre @ acc
-        | None -> acc
-      ) man.local es
-    in
     match es with
     | x :: xs ->
       let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
@@ -277,10 +176,9 @@ struct
           man.emit (Unassume {exp = e; tokens});
           List.iter WideningTokenLifter.add tokens
         )
-      );
-      man.local
+      )
     | [] ->
-      man.local
+      ()
 
   let assign man lv e =
     emit_unassume man
@@ -289,17 +187,7 @@ struct
     emit_unassume man
 
   let body man fd =
-    let pres = FH.find_all fun_pres fd in
-    let st = List.fold_left (fun acc pre ->
-        (* M.debug ~category:Witness "%a precondition %a evaluated to %a" CilType.Fundec.pretty fd CilType.Exp.pretty pre Queries.ID.pretty v; *)
-        if Queries.eval_bool (Analyses.ask_of_man man) pre = `Lifted true then
-          D.add pre acc
-        else
-          acc
-      ) (D.empty ()) pres
-    in
-
-    emit_unassume {man with local = st} (* doesn't query, so no need to redefine ask *)
+    emit_unassume man
 
   let asm man =
     emit_unassume man
@@ -310,9 +198,6 @@ struct
   let special man lv f args =
     emit_unassume man
 
-  let enter man lv f args =
-    [(man.local, D.empty ())]
-
   let combine_env man lval fexp f args fc au f_ask =
     man.local (* not here because isn't final transfer function on edge *)
 

src/arg/myARG.ml

@@ -156,7 +156,7 @@ struct
     | n :: stack ->
       let cfgnode = Arg.Node.cfgnode n in
       match cfgnode with
-      | Function _ -> (* TODO: can this be done without cfgnode? *)
+      | Function cfgnode_fd -> (* TODO: can this be done without cfgnode? *)
         begin match stack with
           (* | [] -> failwith "StackArg.next: return stack empty" *)
           | [] -> [] (* main return *)
@@ -171,14 +171,33 @@ struct
                   | _ -> None
                 )
             in
+            let (entry_lval, entry_args) =
+              Arg.next call_n
+              (* filter because infinite loops starting with function call
+                 will have another Neg(1) edge from the head *)
+              |> List.filter_map (fun (edge, to_n) ->
+                  match edge with
+                  | InlineEntry (lval, _, args) -> Some (lval, args)
+                  | _ -> None
+                )
+              |> List.sort_uniq [%ord: CilType.Lval.t option * CilType.Exp.t list] (* TODO: deduplicate unique element in O(n) *)
+              |> (function
+                  | [lval_args] -> lval_args
+                  | _ -> assert false (* all calls from a node must have same args and lval, even if called function might be different via function pointer *)
+                )
+            in
             Arg.next n
             |> List.filter_map (fun (edge, to_n) ->
-                if BatList.mem_cmp Arg.Node.compare to_n call_next then (
-                  let to_n' = to_n :: call_stack in
-                  Some (edge, to_n')
-                )
-                else
-                  None
+                match edge with
+                | InlineReturn (lval, fd, args) ->
+                  assert (CilType.Fundec.equal fd cfgnode_fd); (* fd in return node should be the same as in InlineReturn edge *)
+                  if BatList.mem_cmp Arg.Node.compare to_n call_next && [%eq: CilType.Lval.t option] lval entry_lval && [%eq: CilType.Exp.t list] args entry_args then (
+                    let to_n' = to_n :: call_stack in
+                    Some (edge, to_n')
+                  )
+                  else
+                    None
+                | _ -> assert false
               )
         end
       | _ ->

src/config/options.schema.json

@@ -2763,8 +2763,8 @@
               "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"
+              "enum": ["invariant_set-flow_insensitive_invariant", "invariant_set-location_invariant"],
+              "default": "invariant_set-flow_insensitive_invariant"
             }
           },
           "additionalProperties": false
@@ -2790,7 +2790,6 @@
               "description": "YAML witness format version",
               "type": "string",
               "enum": [
-                "0.1",
                 "2.0",
                 "2.1"
               ],
@@ -2803,10 +2802,6 @@
               "items": {
                 "type": "string",
                 "enum": [
-                  "location_invariant",
-                  "loop_invariant",
-                  "flow_insensitive_invariant",
-                  "precondition_loop_invariant",
                   "invariant_set",
                   "violation_sequence",
                   "ghost_instrumentation"
@@ -2824,7 +2819,8 @@
                 "type": "string",
                 "enum": [
                   "location_invariant",
-                  "loop_invariant"
+                  "loop_invariant",
+                  "flow_insensitive_invariant"
                 ]
               },
               "default": [