Support exp.architecture outside of SV-COMP mode, add default host ar…

…chitecture

This breaks a lot of SV-COMP/witness tests.

src/common/util/cilfacade.ml

@@ -49,12 +49,11 @@ let init_options () =
   Cil.gnu89inline := get_bool "cil.gnu89inline";
   Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
 
-  if get_bool "ana.sv-comp.enabled" then (
-    Cil.envMachine := match get_string "exp.architecture" with
-      | "32bit" -> Machdep.gcc32
-      | "64bit" -> Machdep.gcc64
-      | _ -> assert false
-  )
+  Cil.envMachine := match get_string "exp.architecture" with
+    | "host" -> Some Machdep.gcc
+    | "32bit" -> Machdep.gcc32
+    | "64bit" -> Machdep.gcc64
+    | _ -> assert false
 
 let init () =
   initCIL ();

src/config/options.schema.json

@@ -1819,10 +1819,10 @@
         },
         "architecture": {
           "title": "exp.architecture",
-          "description": "Architecture for analysis, currently for witness",
+          "description": "Architecture for analysis",
           "type": "string",
-          "enum": ["64bit", "32bit"],
-          "default": "64bit"
+          "enum": ["host", "64bit", "32bit"],
+          "default": "host"
         },
         "gcc_path": {
           "title": "exp.gcc_path",

src/maingoblint.ml

@@ -275,14 +275,12 @@ let preprocess_files () =
   (* Preprocessor flags *)
   let cppflags = ref (get_string_list "pre.cppflags") in
 
-  if get_bool "ana.sv-comp.enabled" then (
-    let architecture_flag = match get_string "exp.architecture" with
-      | "32bit" -> "-m32"
-      | "64bit" -> "-m64"
-      | _ -> assert false
-    in
-    cppflags := architecture_flag :: !cppflags
-  );
+  cppflags := begin match get_string "exp.architecture" with
+    | "host" -> !cppflags
+    | "32bit" -> "-m32" :: !cppflags
+    | "64bit" -> "-m64" :: !cppflags
+    | _ -> assert false
+  end;
 
   (* the base include directory *)
   (* TODO: any better way? dune executable promotion doesn't add _build sites *)

src/witness/witness.ml

@@ -124,7 +124,11 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   GML.write_metadata g "programfile" programfile;
   let programhash = Sha256.(to_hex (file programfile)) in
   GML.write_metadata g "programhash" programhash;
-  GML.write_metadata g "architecture" (get_string "exp.architecture");
+  let architecture = match GobConfig.get_string "exp.architecture" with
+    | ("64bit" | "32bit") as architecture -> architecture
+    | _ -> failwith "invalid SV-COMP architecture"
+  in
+  GML.write_metadata g "architecture" architecture;
   GML.write_metadata g "creationtime" (TimeUtil.iso8601_now ());
 
   let write_node ?(entry=false) node =

src/witness/yamlWitness.ml

@@ -203,7 +203,7 @@ struct
     let data_model = match GobConfig.get_string "exp.architecture" with
       | "64bit" -> "LP64"
       | "32bit" -> "ILP32"
-      | _ -> failwith "invalid architecture"
+      | _ -> failwith "invalid SV-COMP architecture"
     in
     let specification = Option.map (fun (module Task: Svcomp.Task) ->
         Svcomp.Specification.to_string Task.specification