Merge branch 'master' into multishot-svcomp25

Author: DrMichaelPetter

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) =
@@ -230,15 +141,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
@@ -252,12 +157,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
@@ -268,10 +167,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
@@ -280,17 +178,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
@@ -301,9 +189,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/config/gobConfig.ml

@@ -404,8 +404,7 @@ struct
 
   (** Merge configurations form a file with current. *)
   let merge_file fn =
-    let cwd = Fpath.v (Sys.getcwd ()) in
-    let config_dirs = cwd :: Fpath.(parent (v Sys.executable_name)) :: Goblint_sites.conf in
+    let config_dirs = GobFpath.cwd () :: GobSys.exe_dir :: Goblint_sites.conf in
     let file = List.find_map_opt (fun custom_include_dir ->
         let path = Fpath.append custom_include_dir fn in
         if Sys.file_exists (Fpath.to_string path) then

src/config/options.schema.json

@@ -2790,7 +2790,6 @@
               "description": "YAML witness format version",
               "type": "string",
               "enum": [
-                "0.1",
                 "2.0",
                 "2.1"
               ],
@@ -2803,9 +2802,6 @@
               "items": {
                 "type": "string",
                 "enum": [
-                  "location_invariant",
-                  "loop_invariant",
-                  "precondition_loop_invariant",
                   "invariant_set",
                   "violation_sequence",
                   "ghost_instrumentation"

src/framework/xsltResultOutput.ml

@@ -288,7 +288,7 @@ struct
     Timing.wrap "graphviz" (ProcessPool.run ~jobs:(GobConfig.jobs ())) tasks
 
   let copy_resources ~result_dir =
-    let xslt_dirs = Fpath.(parent (v Sys.executable_name) / "xslt") :: Goblint_sites.xslt in
+    let xslt_dirs = Fpath.(GobSys.exe_dir / "xslt") :: Goblint_sites.xslt in
     let xslt_dir = List.find_opt (fun dir ->
         let dir_str = Fpath.to_string dir in
         Sys.file_exists dir_str && Sys.is_directory dir_str