Merge pull request #173 from goblint/machdep-arch

Generate 32bit and 64bit `Machdep` if possible

src/dune

@@ -4,7 +4,7 @@
   (public_name goblint-cil)
   (name goblintCil)
   (libraries zarith findlib dynlink unix str stdlib-shims)
-  (modules (:standard \ main ciloptions machdepConfigure modelConfigure))
+  (modules (:standard \ main ciloptions machdepConfigure machdepArchConfigure modelConfigure))
 )
 
 (executable
@@ -21,6 +21,21 @@
  (target machdep-ml.exe)
  (action (run %{read-lines:../bin/real-gcc} -D_GNUCC machdep-ml.c -o %{target})))
 
+(executable
+ (name machdepArchConfigure)
+ (modules machdepArchConfigure)
+ (libraries dune-configurator))
+
+(rule
+ (deps machdep-config.h machdep-ml.c)
+ (target machdep32)
+ (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 32))))
+
+(rule
+ (deps machdep-config.h machdep-ml.c)
+ (target machdep64)
+ (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64))))
+
 ; for Cilly.pm
 (executable
  (name modelConfigure)
@@ -40,6 +55,7 @@
  (action (with-stdout-to %{target} (run ./modelConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64))))
 
 (rule
+ (deps machdep32 machdep64)
  (target machdep.ml)
  (action (run %{bin:cppo} -V OCAML:%{ocaml_version}
               %{dep:machdep.cppo.ml} -x machdep:./%{dep:machdep-ml.exe}

src/machdep.cppo.ml

@@ -56,4 +56,11 @@ let gcc = {
 #ext machdep
 #endext
 }
+
+let gcc32 =
+#include "machdep32"
+
+let gcc64 =
+#include "machdep64"
+
 let theMachine : mach ref = ref gcc

src/machdepArchConfigure.ml

@@ -0,0 +1,21 @@
+module C = Configurator.V1
+
+let () =
+  let real_gcc = ref "" in
+  let m = ref "" in
+  let args = Arg.[
+      ("--real-gcc", Set_string real_gcc, "");
+      ("-m", Set_string m, "");
+    ]
+  in
+  C.main ~name:"model" ~args (fun c ->
+      let exe = "./machdep" ^ !m ^ "-ml.exe" in
+      let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
+      if exit_code = 0 then (
+        let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in
+        assert (exit_code = 0);
+        Printf.printf "Some {%s}" stdout
+      )
+      else 
+        Printf.printf "None"
+    )

src/modelConfigure.ml

@@ -13,6 +13,7 @@ let () =
       let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
       if exit_code = 0 then (
         let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe ["--env"] in
+        assert (exit_code = 0);
         print_string stdout;
       )
       else