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] 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"
+    )