Skip to content

Commit

Permalink
Generate 32bit and 64bit Machdep if possible
Browse files Browse the repository at this point in the history
The -m32 and -m64 arguments are x86-only, so these have to be optional.
  • Loading branch information
sim642 committed Sep 24, 2024
1 parent 135fc3c commit 73d0251
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 1 deletion.
18 changes: 17 additions & 1 deletion src/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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}
Expand Down
7 changes: 7 additions & 0 deletions src/machdep.cppo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -56,4 +56,11 @@ let gcc = {
#ext machdep
#endext
}

let gcc32 =
#include "machdep32"

let gcc64 =
#include "machdep64"

let theMachine : mach ref = ref gcc
20 changes: 20 additions & 0 deletions src/machdepArchConfigure.ml
Original file line number Diff line number Diff line change
@@ -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"
)

0 comments on commit 73d0251

Please sign in to comment.