From 73d02511a0366816d428853634fb939bd2f0a1b7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 Sep 2024 11:05:15 +0300
Subject: [PATCH 1/3] Generate 32bit and 64bit Machdep if possible

The -m32 and -m64 arguments are x86-only, so these have to be optional.
---
 src/dune                    | 18 +++++++++++++++++-
 src/machdep.cppo.ml         |  7 +++++++
 src/machdepArchConfigure.ml | 20 ++++++++++++++++++++
 3 files changed, 44 insertions(+), 1 deletion(-)
 create mode 100644 src/machdepArchConfigure.ml

diff --git a/src/dune b/src/dune
index 6b3766013..09b365c02 100644
--- a/src/dune
+++ b/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}
diff --git a/src/machdep.cppo.ml b/src/machdep.cppo.ml
index 45d734e93..b00ef8cfc 100644
--- a/src/machdep.cppo.ml
+++ b/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
diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
new file mode 100644
index 000000000..ebf4ee0e7
--- /dev/null
+++ b/src/machdepArchConfigure.ml
@@ -0,0 +1,20 @@
+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-ml" ^ !m ^ ".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
+        Printf.printf "Some {%s}" stdout
+      )
+      else 
+        Printf.printf "None"
+    )

From 72829a316bd35a1317dd715c6fc412d49c5873e5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 Sep 2024 15:32:40 +0300
Subject: [PATCH 2/3] Change machdepArchConfigure compiled output name to avoid
 potential conflict with modelConfigure

---
 src/machdepArchConfigure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
index ebf4ee0e7..95ed6a22e 100644
--- a/src/machdepArchConfigure.ml
+++ b/src/machdepArchConfigure.ml
@@ -9,7 +9,7 @@ let () =
     ]
   in
   C.main ~name:"model" ~args (fun c ->
-      let exe = "./machdep-ml" ^ !m ^ ".exe" in
+      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

From 9f4fac450c02bc61a13717784515056b185794cd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 Sep 2024 15:33:12 +0300
Subject: [PATCH 3/3] Assert machdep-ml exit code to be 0

---
 src/machdepArchConfigure.ml | 1 +
 src/modelConfigure.ml       | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
index 95ed6a22e..29a249cd0 100644
--- a/src/machdepArchConfigure.ml
+++ b/src/machdepArchConfigure.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 [] in
+        assert (exit_code = 0);
         Printf.printf "Some {%s}" stdout
       )
       else 
diff --git a/src/modelConfigure.ml b/src/modelConfigure.ml
index 5b0e8a4ac..a161e703a 100644
--- a/src/modelConfigure.ml
+++ b/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