From d57ccc8d2cb6e71f95f1703bca67750d336238f2 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Fri, 24 Apr 2026 22:04:33 +0200
Subject: [PATCH 01/12] feat(cpd): add LLVM command module to compile .ll/.bc
 to wasm for symex

---
 src/cmd/cmd_llvm.ml | 116 ++++++++++++++++++++++++++++++++++++++++++++
 src/dune            |   1 +
 src/owi.ml          |   1 +
 3 files changed, 118 insertions(+)
 create mode 100644 src/cmd/cmd_llvm.ml

diff --git a/src/cmd/cmd_llvm.ml b/src/cmd/cmd_llvm.ml
new file mode 100644
index 000000000..f946f95c5
--- /dev/null
+++ b/src/cmd/cmd_llvm.ml
@@ -0,0 +1,116 @@
+open Bos
+open Syntax
+
+let resolve_binary name =
+  match OS.Cmd.resolve @@ Cmd.v name with
+  | Error _ ->
+    Fmt.error_msg
+      "The `%s` binary was not found, please make sure it is in your path."
+      name
+  | Ok _ as ok -> ok
+
+let err_output =
+  match Logs.Src.level Log.main_src with
+  | Some (Logs.Debug | Logs.Info) -> OS.Cmd.err_run_out
+  | None | Some _ -> OS.Cmd.err_null
+
+let bitcode_of_input ~workspace ~llvm_as_bin file : Fpath.t Result.t =
+  match Fpath.get_ext ~multi:false file with
+  | ".bc" -> Ok file
+  | ".ll" ->
+    let out_bc = Fpath.(workspace // Fpath.base (file -+ ".bc")) in
+    let llvm_as_cmd : Cmd.t = Cmd.(llvm_as_bin % p file % "-o" % p out_bc) in
+    let+ () =
+      match OS.Cmd.run ~err:err_output llvm_as_cmd with
+      | Ok _ as v -> v
+      | Error (`Msg e) ->
+        Log.debug (fun m -> m "llvm-as failed: %s" e);
+        Fmt.error_msg
+          "llvm-as failed: run with -vv to get the full error message if it was \
+           not displayed above"
+    in
+    out_bc
+  | ext ->
+    Fmt.error_msg
+      "Unsupported file extension `%s` for LLVM command, expected .ll or .bc"
+      ext
+
+let compile ~workspace ~entry_point ~out_file (files : Fpath.t list) :
+  Fpath.t Result.t =
+  let* llvm_as_bin = resolve_binary "llvm-as" in
+  let* llc_bin = resolve_binary "llc" in
+  let* wasmld_bin = resolve_binary "wasm-ld" in
+
+  let* bc_files =
+    list_map (bitcode_of_input ~workspace ~llvm_as_bin) files
+  in
+
+  let files_bc = Cmd.of_list (List.map Cmd.p bc_files) in
+  let llc_cmd : Cmd.t =
+    Cmd.(llc_bin % "-O0" % "-march=wasm32" % "-filetype=obj" %% files_bc)
+  in
+
+  let* () =
+    Log.bench_fn "llc time" @@ fun () ->
+    match OS.Cmd.run ~err:err_output llc_cmd with
+    | Ok _ as v -> v
+    | Error (`Msg e) ->
+      Log.debug (fun m -> m "llc failed: %s" e);
+      Fmt.error_msg "llc failed: run with -vv to get the full error message"
+  in
+
+  let files_o = Cmd.of_list (List.map (fun file -> Cmd.p Fpath.(file -+ ".o")) bc_files) in
+
+  let out = Option.value ~default:Fpath.(workspace / "a.out.wasm") out_file in
+
+  let* libc = Cmd_utils.find_installed_c_file (Fpath.v "libc.wasm") in
+  let* libowi = Cmd_utils.find_installed_c_file (Fpath.v "libowi.wasm") in
+
+  let wasmld_cmd : Cmd.t =
+    Cmd.(
+      wasmld_bin
+      %% of_list
+           ( [ "-z"; "stack-size=8388608" ]
+           @ ( match entry_point with
+             | None -> []
+             | Some entry_point ->
+               [ Fmt.str "--export=%s" entry_point
+               ; Fmt.str "--entry=%s" entry_point
+               ] )
+           @ [ "--allow-undefined" ]
+           @ [ p libc; p libowi ]
+           @ [ "-o"; p out ] )
+      %% files_o )
+  in
+
+  let+ () =
+    Log.bench_fn "wasm-ld time" @@ fun () ->
+    match OS.Cmd.run ~err:err_output wasmld_cmd with
+    | Ok _ as v -> v
+    | Error (`Msg e) ->
+      Log.debug (fun m -> m "wasm-ld failed: %s" e);
+      Fmt.error_msg
+        "wasm-ld failed: run with -vv to get the full error message if it was \
+         not displayed above"
+  in
+
+  out
+
+let cmd ~(symbolic_parameters : Symbolic_parameters.t) ~files ~out_file :
+  unit Result.t =
+  let* workspace =
+    match symbolic_parameters.workspace with
+    | Some path -> Ok path
+    | None -> OS.Dir.tmp "owi_llvm_%s"
+  in
+  let* _did_create : bool = OS.Dir.create ~path:true workspace in
+
+  let* source_file =
+    compile ~workspace ~entry_point:symbolic_parameters.entry_point ~out_file
+      files
+  in
+  let workspace = Some workspace in
+
+  let parameters = { symbolic_parameters with workspace } in
+
+  Cmd_sym.cmd ~parameters ~source_file
diff --git a/src/dune b/src/dune
index de33545ff..a3b07b15c 100644
--- a/src/dune
+++ b/src/dune
@@ -25,6 +25,7 @@
   cmd_haskell
   cmd_instrument_label
   cmd_iso
+  cmd_llvm
   cmd_replay
   cmd_run
   cmd_rust
diff --git a/src/owi.ml b/src/owi.ml
index f27fb4221..f0f88fd1a 100644
--- a/src/owi.ml
+++ b/src/owi.ml
@@ -12,6 +12,7 @@ module Cmd_fuzz = Cmd_fuzz
 module Cmd_haskell = Cmd_haskell
 module Cmd_instrument_label = Cmd_instrument_label
 module Cmd_iso = Cmd_iso
+module Cmd_llvm = Cmd_llvm
 module Cmd_replay = Cmd_replay
 module Cmd_run = Cmd_run
 module Cmd_rust = Cmd_rust

From 1a00530611a20651af83e06d2225efd0c69fcfc1 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sat, 25 Apr 2026 14:11:25 +0200
Subject: [PATCH 02/12] feat(cmd): add llvm cmd doc and .mli file

---
 src/bin/owi.ml       | 17 +++++++++++++++++
 src/cmd/cmd_llvm.mli |  5 +++++
 2 files changed, 22 insertions(+)
 create mode 100644 src/cmd/cmd_llvm.mli

diff --git a/src/bin/owi.ml b/src/bin/owi.ml
index 3f3a8a76a..699ca21b2 100644
--- a/src/bin/owi.ml
+++ b/src/bin/owi.ml
@@ -499,6 +499,22 @@ let iso_cmd =
     ~no_stop_at_failure ~no_value ~seed ~solver ~unsafe ~workers
     ~no_worker_isolation ~workspace ~model_out_file ~with_breadcrumbs
 
+(* owi llvm *)
+
+let llvm_info =
+  let doc =
+    "Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter on it"
+  in
+  let man = [] @ shared_man in
+  Cmd.info "llvm" ~version ~doc ~sdocs ~man
+
+let llvm_cmd =
+  let+ files
+  and+ out_file
+  and+ () = setup_log
+  and+ symbolic_parameters = symbolic_parameters None in
+  Cmd_llvm.cmd ~symbolic_parameters ~files ~out_file
+
 (* owi replay *)
 
 let replay_info =
@@ -701,6 +717,7 @@ let cli =
         [ Cmd.v instrument_label_info instrument_label_cmd ]
     ; Cmd.v haskell_info haskell_cmd
     ; Cmd.v iso_info iso_cmd
+    ; Cmd.v llvm_info llvm_cmd
     ; Cmd.v replay_info replay_cmd
     ; Cmd.v run_info run_cmd
     ; Cmd.v rust_info rust_cmd
diff --git a/src/cmd/cmd_llvm.mli b/src/cmd/cmd_llvm.mli
new file mode 100644
index 000000000..431cd6df7
--- /dev/null
+++ b/src/cmd/cmd_llvm.mli
@@ -0,0 +1,5 @@
+val cmd :
+     symbolic_parameters:Symbolic_parameters.t
+  -> files:Fpath.t list
+  -> out_file:Fpath.t option
+  -> unit Result.t
\ No newline at end of file

From 870a9b0163826eb8bf9e58e0746bff82fa0b6d44 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sat, 25 Apr 2026 15:58:46 +0200
Subject: [PATCH 03/12] fix(cmd): add cmd_llvm to owi.mli

---
 src/owi.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/owi.mli b/src/owi.mli
index 7340a6334..4845caa98 100644
--- a/src/owi.mli
+++ b/src/owi.mli
@@ -1755,6 +1755,14 @@ module Cmd_iso : sig
     -> unit Result.t
 end
 
+module Cmd_llvm : sig
+  val cmd :
+      symbolic_parameters:Symbolic_parameters.t
+  -> files:Fpath.t list
+  -> out_file:Fpath.t option
+  -> unit Result.t
+end
+
 module Cmd_replay : sig
   val cmd :
        unsafe:bool

From da3533fcd363144af4e3277076b265b092c690b2 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sat, 25 Apr 2026 16:02:38 +0200
Subject: [PATCH 04/12] feat(cramtest): add error cramtest for llvm

---
 test/cram/help/help.t            | 5 +++++
 test/cram/llvm/bad.txt           | 1 +
 test/cram/llvm/dune              | 3 +++
 test/cram/llvm/empty.t           | 5 +++++
 test/cram/llvm/not_exists.t      | 5 +++++
 test/cram/llvm/unsupported_ext.t | 3 +++
 6 files changed, 22 insertions(+)
 create mode 100644 test/cram/llvm/bad.txt
 create mode 100644 test/cram/llvm/dune
 create mode 100644 test/cram/llvm/empty.t
 create mode 100644 test/cram/llvm/not_exists.t
 create mode 100644 test/cram/llvm/unsupported_ext.t

diff --git a/test/cram/help/help.t b/test/cram/help/help.t
index 3eaf27674..b73a7718e 100644
--- a/test/cram/help/help.t
+++ b/test/cram/help/help.t
@@ -33,6 +33,10 @@ no subcommand should print help
              Check the iso-functionnality of two Wasm modules by comparing the
              output when calling their exports.
   
+         llvm [OPTION]… FILE…
+             Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter
+             on it
+  
          replay [OPTION]… FILE
              Replay a module containing symbols with concrete values in a
              replay file containing a model
@@ -93,3 +97,4 @@ no subcommand should print help
   BUGS
          Email them to <contact@ndrs.fr>.
   
+
diff --git a/test/cram/llvm/bad.txt b/test/cram/llvm/bad.txt
new file mode 100644
index 000000000..df441fe02
--- /dev/null
+++ b/test/cram/llvm/bad.txt
@@ -0,0 +1 @@
+not llvm
diff --git a/test/cram/llvm/dune b/test/cram/llvm/dune
new file mode 100644
index 000000000..f602e00ba
--- /dev/null
+++ b/test/cram/llvm/dune
@@ -0,0 +1,3 @@
+(cram
+ (deps %{bin:owi} bad.txt)
+ (alias quicktest))
diff --git a/test/cram/llvm/empty.t b/test/cram/llvm/empty.t
new file mode 100644
index 000000000..10b2ca835
--- /dev/null
+++ b/test/cram/llvm/empty.t
@@ -0,0 +1,5 @@
+  $ owi llvm
+  owi: required argument FILE is missing
+  Usage: owi llvm [OPTION]… FILE…
+  Try 'owi llvm --help' or 'owi --help' for more information.
+  [124]
diff --git a/test/cram/llvm/not_exists.t b/test/cram/llvm/not_exists.t
new file mode 100644
index 000000000..9f1127652
--- /dev/null
+++ b/test/cram/llvm/not_exists.t
@@ -0,0 +1,5 @@
+  $ owi llvm not_exists.bc
+  owi: FILE… arguments: no file 'not_exists.bc'
+  Usage: owi llvm [OPTION]… FILE…
+  Try 'owi llvm --help' or 'owi --help' for more information.
+  [124]
diff --git a/test/cram/llvm/unsupported_ext.t b/test/cram/llvm/unsupported_ext.t
new file mode 100644
index 000000000..59d26d80d
--- /dev/null
+++ b/test/cram/llvm/unsupported_ext.t
@@ -0,0 +1,3 @@
+  $ owi llvm bad.txt
+  owi: [ERROR] Unsupported file extension `.txt` for LLVM command, expected .ll or .bc
+  [26]

From 821e4f43a2e3dd08b86ae975cc21211b45871543 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sat, 25 Apr 2026 19:46:32 +0200
Subject: [PATCH 05/12] test(cmd): add llvm cramtests

---
 test/cram/llvm/dune             |   2 +-
 test/cram/llvm/simple.bc        | Bin 0 -> 1180 bytes
 test/cram/llvm/simple.ll        |   6 ++++++
 test/cram/llvm/simple.t         |   6 ++++++
 test/cram/llvm/trap_div_zero.bc | Bin 0 -> 1200 bytes
 test/cram/llvm/trap_div_zero.ll |   7 +++++++
 test/cram/llvm/trap_div_zero.t  |  12 ++++++++++++
 7 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 test/cram/llvm/simple.bc
 create mode 100644 test/cram/llvm/simple.ll
 create mode 100644 test/cram/llvm/simple.t
 create mode 100644 test/cram/llvm/trap_div_zero.bc
 create mode 100644 test/cram/llvm/trap_div_zero.ll
 create mode 100644 test/cram/llvm/trap_div_zero.t

diff --git a/test/cram/llvm/dune b/test/cram/llvm/dune
index f602e00ba..354d3ca30 100644
--- a/test/cram/llvm/dune
+++ b/test/cram/llvm/dune
@@ -1,3 +1,3 @@
 (cram
- (deps %{bin:owi} bad.txt)
+ (deps %{bin:owi} bad.txt simple.ll simple.bc trap_div_zero.ll trap_div_zero.bc)
  (alias quicktest))
diff --git a/test/cram/llvm/simple.bc b/test/cram/llvm/simple.bc
new file mode 100644
index 0000000000000000000000000000000000000000..f1ff4cca5d05ccb3f18f1dc5203d9286fc72fbf7
GIT binary patch
literal 1180
zcmYjRZ%kWN6u<3*z6#xa-KeY$?>*leEH)GItxRowZ9;i-K_#(7Khy-X7O?>b_3=mA
zf-x<x+hws!IznbYU;+srH1R{1@PQA+Kp)OZ>Vk_gBsPRfVQ4ziI5bP#2X8wyp5&c#
z?z#7!d(Q9v?(LM;c3w0APzwO)GYBoOzw>qA#$U^C*7roaH8{o_062l2dMyvMc-)9T
zGS+<4ovnFIXS6wHHF3k)TD^s>`Lr);cvaguTi@Alw3+OB^BZ+G+f0|d!8cz#g%U>h
zthPU^zir~AOEcVe8k;R{K4(3bJpXaJ_a>)iao+13-UnOTnXI1cy9D^>T2co7ELN6h
z4Of?vK3jh;*Ye)<LaG@M4N;p>(1M1qrt~N>fE-EXr7y^kmkfo`l#Kr8lQ)dlx?AFr
z#?0kg{L>vZc!U3>hP&-v7`O;PN2?Bi&v3k5AEh@6bikx>%}DmRn&^y@kuW)y8ZjII
z>VXj+M`636lg+F%cNgh^P+MK5H020aR&pf>S1z0wm&qwT8R<f@Ois$gL>S2&vgA&}
zQW6#fDkxBUWmxvWcH;)K!_(V5lku|w;kvl0h+C3lnQ*Qu&Nw0F%BBe)IW<7OJb*^A
zjv_gUWFI+UB_|%$;<TYCx~xYdW;B{YkyNbps0@#G;U8<TBoKYsMY_01=c+pIr#E?e
zBgSm{bw4E~M^<vAs(MAW&q?+fLYz}yz?(jv7Jnqfv}*Wv5XoLNDl6jyWY~ws&1if9
zS?<0?9Rcch4=g6(UI$g+U<r4@S(*Ggn{l)Ecsd_r^SgAh!2G6R1LhukT6$$(5p$lF
ze;V<jP?!v-db*F3R0RR{19sC-AM(u3I`fH!trW~NWxww2tBO6RifPG(0ePHp7A0{8
z57opsb+}U$!u9CMNh>*;iuLXpVQCHSd*DN%dHtT7Ef!917nmJfK$k^KE3RdwDX!WR
zk|U=&SJoX_75C`ObuEwRNnF(k2GENvKi`2RAN62YSLUdFf!gP&KRqyLgnI(S!-u=N
zUw2{A10M;^zm)uRCdO<RPM3J*fM+&%2A|*||4e}UTwIl0D}-ZCapb(K`1EnJleo?<
z6p~2*zBJ?eggI7UH)_RaM^1X>6ke}llpI^?^Z|Wm@x-CKLM@#32_}sf_I&WZ2SZI2
zD}Yn?J@7akjgb*+l?h>lyQtvcmFHFavPN7|Tyv`S3MLhuFVK08F8V9_Fve#5^wuJs
zeNw#U2O|KO@_@`amlSax6M%3nC{9d<q*}T6ehz@Aux+Sux8kLs5{sV%peashD(?X4
zF@A6IV+YF!2LOSs4I0nH!L`bCRo=yK2gKefVs5Y!81@ea&tGU0+JumQY`ER_{71nn
X!4E^hf9=@dusrmB+t5(;Zvg%Vz50=J

literal 0
HcmV?d00001

diff --git a/test/cram/llvm/simple.ll b/test/cram/llvm/simple.ll
new file mode 100644
index 000000000..30a63198e
--- /dev/null
+++ b/test/cram/llvm/simple.ll
@@ -0,0 +1,6 @@
+target triple = "wasm32-unknown-unknown"
+
+define i32 @main() {
+entry:
+  ret i32 0
+}
diff --git a/test/cram/llvm/simple.t b/test/cram/llvm/simple.t
new file mode 100644
index 000000000..b1cb21e75
--- /dev/null
+++ b/test/cram/llvm/simple.t
@@ -0,0 +1,6 @@
+simple.bc and simple.ll cramtests : 
+  $ owi llvm simple.ll --entry-point=main --no-value
+  All OK!
+
+  $ owi llvm simple.bc --entry-point=main --no-value
+  All OK!
diff --git a/test/cram/llvm/trap_div_zero.bc b/test/cram/llvm/trap_div_zero.bc
new file mode 100644
index 0000000000000000000000000000000000000000..246395204a768ec967fe9e1a896a35e48d8104f7
GIT binary patch
literal 1200
zcmYjRVQ3p=7{27%TxjFnwT)ZC?#{clV`0vEOXp0y1WZpy)qyGQM+TMVY7MR1vTIhG
zv=vQy*}e=j$VOrLQK6M04*Zcpe)LC?HWz0sanvDFFqFooU6rf^S7qQBewV8F!M*o>
z@AuvNJ<s#K?{$ky>o1uRq!B@o0TbWx=DDu}*Z<1C-P{{Jqk}Qdgdi=@Y1VUy9?lQI
z2aC1e@Dv)}FpzfVO<mk{q|s<)8a^F}nqJp;-)!z4B<*I0(ehT4-Ja-?^IZFDtsqHy
zZt4dM#ye(KJe^>_)7kBD%Q4%r)QOKWeK%OO0P|jB;W_YaKU^@f1E&%0`Hr-SI|7aM
zsOidl%5NX+V>{lPnoYMOXj{}y@_MB0t4Sjm9|F#la_UPg?8CwlFe!uo`Pg;xYWxdh
z<f-oV(`17B<lNP>NDDmWzd=UxhS=xNLXvkZ$SoM|GDfL<nF^S7?u6)wtI6&tHXgw)
zr$<cN2=S1__o8^0shi0y)A#160N+^OrW`7w?t<t}qV8fOIVxk5Mr^zX$TBt|qhk>u
zv%p$x!K*2}%o9PL*sS3-FWyDw>2;1;<LI2k1o&&hq9Uw{&MfL$R9taXDAvqler$3G
zdwB?ipp61K1!O-qX2ZrFH^Q{xDCjqW5eo>V!FW1$e7A=0Zs30`;Z+_TD9llnIjUH<
zC5c+$sC<lGkqkejL}x*Crt5Y=bxezn1S(9cFTz8gObI`tLPj-xI}BtW2+7Lm5Ek)+
zQ41KI1=f4-5W5KRyBDvd@Xc3=GK*Is3)V)LmYJM~xzACh7*pDyDrNdN9TTwhIx^xb
zGm233cKk!c55f^FlI}gTmm)L;m=Bm0iQ3`l^=0~F9isu}=$d3Wdqr^+RUsp~p&(Ck
zu8Jrm;8ab1(*&7<FvMfTCTv(J9qZd9@#+%3<;5TI?aTK)Or?BqtxT^&06kVAqqwum
zp}6Wuiq4|yT3B`#RLId)?8%N8F^Fme3g`pYpYP&TKk;zGP-BTLp4eiEKfQR6#5Z{y
zP9JR;e%-(;Ui>lN{!3M&axr?Xe6Y&V+Z>(eXn2D=+;ai;GhtD5FQCq8#aZ+%!rO;r
zCm_xq5SB3nxov?x1#7IiDP)6phfVn8G~BO3m7J^U)HZc@?wK8rR$4Iaz9t7wZu;>D
zUMMwD(F7+Rc=5eVG=`1a>Xi@ykcFm$Po7a7S)DMixTjV9d013bsZ5nvsv>E2C&uI?
zYITk(?1R_+Kq80%V!?{8c}19k1%SF|6&Eaql&bZ<#3Bf6f26I!a~y81_kX<AqAeju
z8?qh;45HA-yyW+0=@i+gEx<9t?#Jyoc{q*$?YB`M@4{pR^jgtrSqog0hJz<gcJiHk
mSh{?%%l^WL!SlgO;o!gT(U2tf4-Sv@PrM(x)Oq28_RZe|#hMEM

literal 0
HcmV?d00001

diff --git a/test/cram/llvm/trap_div_zero.ll b/test/cram/llvm/trap_div_zero.ll
new file mode 100644
index 000000000..6ff4a871a
--- /dev/null
+++ b/test/cram/llvm/trap_div_zero.ll
@@ -0,0 +1,7 @@
+target triple = "wasm32-unknown-unknown"
+
+define i32 @main() {
+entry:
+  %x = sdiv i32 1, 0
+  ret i32 %x
+}
diff --git a/test/cram/llvm/trap_div_zero.t b/test/cram/llvm/trap_div_zero.t
new file mode 100644
index 000000000..5a0859030
--- /dev/null
+++ b/test/cram/llvm/trap_div_zero.t
@@ -0,0 +1,12 @@
+trap_div_zero:
+  $ owi llvm trap_div_zero.ll --entry-point=main --no-value
+  owi: [ERROR] Trap: integer divide by zero
+  model
+  owi: [ERROR] Reached problem!
+  [13]
+
+  $ owi llvm trap_div_zero.bc --entry-point=main --no-value
+  owi: [ERROR] Trap: integer divide by zero
+  model
+  owi: [ERROR] Reached problem!
+  [13]

From 1a1463dc79c844b1cc6cb77bce3ec15dfe9cd91c Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sat, 25 Apr 2026 19:53:12 +0200
Subject: [PATCH 06/12] fix(cmd llvm): add cmd_llvm files licence headers

---
 src/cmd/cmd_llvm.ml  | 4 ++++
 src/cmd/cmd_llvm.mli | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/src/cmd/cmd_llvm.ml b/src/cmd/cmd_llvm.ml
index f946f95c5..d81369cfa 100644
--- a/src/cmd/cmd_llvm.ml
+++ b/src/cmd/cmd_llvm.ml
@@ -1,3 +1,7 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
 open Bos
 open Syntax
 
diff --git a/src/cmd/cmd_llvm.mli b/src/cmd/cmd_llvm.mli
index 431cd6df7..1016ede60 100644
--- a/src/cmd/cmd_llvm.mli
+++ b/src/cmd/cmd_llvm.mli
@@ -1,3 +1,7 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
 val cmd :
      symbolic_parameters:Symbolic_parameters.t
   -> files:Fpath.t list

From e24f7f6c66a5ce37585e4fbb864b5e1496e46c3f Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Sun, 26 Apr 2026 02:39:07 +0200
Subject: [PATCH 07/12] docs(cmd llvm): add docs for llvm command

---
 doc/src/SUMMARY.md           |   1 +
 doc/src/manpages/dune        |   1 +
 doc/src/manpages/owi-llvm.md | 141 +++++++++++++++++++++++++++++++++++
 doc/src/manpages/owi.md      |   4 +
 4 files changed, 147 insertions(+)
 create mode 100644 doc/src/manpages/owi-llvm.md

diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index e783837b1..63a00e255 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -42,6 +42,7 @@
     - [`owi fmt`](manpages/owi-fmt.md)
     - [`owi instrument`](manpages/owi-instrument.md)
     - [`owi iso`](manpages/owi-iso.md)
+    - [`owi llvm`](manpages/owi-llvm.md)
     - [`owi replay`](manpages/owi-replay.md)
     - [`owi run`](manpages/owi-run.md)
     - [`owi rust`](manpages/owi-rust.md)
diff --git a/doc/src/manpages/dune b/doc/src/manpages/dune
index 4d6542a62..4ac136953 100644
--- a/doc/src/manpages/dune
+++ b/doc/src/manpages/dune
@@ -10,6 +10,7 @@
   owi-fmt.md
   owi-instrument.md
   owi-iso.md
+  owi-llvm.md
   owi-replay.md
   owi-run.md
   owi-rust.md
diff --git a/doc/src/manpages/owi-llvm.md b/doc/src/manpages/owi-llvm.md
new file mode 100644
index 000000000..e06a0ceb7
--- /dev/null
+++ b/doc/src/manpages/owi-llvm.md
@@ -0,0 +1,141 @@
+# `owi llvm`
+
+```sh
+$ owi llvm --help=plain
+NAME
+       owi-llvm - Compile LLVM IR/bitcode to Wasm and run the symbolic
+       interpreter on it
+
+SYNOPSIS
+       owi llvm [OPTION]… FILE…
+
+ARGUMENTS
+       FILE (required)
+           source files
+
+OPTIONS
+       --deterministic-result-order
+           Guarantee a fixed deterministic order of found failures. This
+           implies --no-stop-at-failure.
+
+       --entry-point=FUNCTION
+           entry point of the executable
+
+       --exploration=VAL (absent=fifo)
+           exploration strategy to use ("fifo", "lifo", "random",
+           "random-unseen-then-random", "rarity", "hot-path-penalty",
+           "rarity-aging", "rarity-depth-aging", "rarity-depth-loop-aging",
+           "rarity-depth-loop-aging-random")
+
+       --fail-on-assertion-only
+           ignore traps and only report assertion violations
+
+       --fail-on-trap-only
+           ignore assertion violations and only report traps
+
+       --invoke-with-symbols
+           Invoke the entry point of the program with symbolic values instead
+           of dummy constants.
+
+       --model-format=VAL (absent=scfg)
+          The format of the model ("json" or "scfg")
+
+       --model-out-file=FILE
+           Output the generated model to FILE. if --no-stop-at-failure is
+           given this is used as a prefix and the ouputed files would have
+           PREFIX_%d.
+
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
+       --no-ite-for-select
+           do not use ite for select
+
+       --no-stop-at-failure
+           do not stop when a program failure is encountered
+
+       --no-value
+           do not display a value for each symbol
+
+       --no-worker-isolation
+           Do not force each worker to run on an isolated physical core.
+
+       -o FILE, --output=FILE
+           Output the generated .wasm or .wat to FILE.
+
+       -s VALUE, --solver=VALUE (absent=Z3)
+           SMT solver to use. VALUE must be one of the 6 available solvers:
+           Z3, Bitwuzla, Colibri2, cvc5, Alt-Ergo, SMTZilla
+
+       --seed=I
+           Initial seed for the PRNG state
+
+       --timeout=S
+           Stop execution after S seconds.
+
+       --timeout-instr=I
+           Stop execution after running I instructions.
+
+       -u, --unsafe
+           skip typechecking pass
+
+       -w VAL, --workers=VAL (absent=n)
+           Number of workers for symbolic execution. Defaults to the number
+           of physical cores.
+
+       --with-breadcrumbs
+           add breadcrumbs to the generated model
+
+       --workspace=DIR
+           write results and intermediate compilation artifacts to dir
+
+COMMON OPTIONS
+       --bench
+           enable benchmarks
+
+       --color=WHEN (absent=auto)
+           Colorize the output. WHEN must be one of auto, always or never.
+
+       --help[=FMT] (default=auto)
+           Show this help in format FMT. The value FMT must be one of auto,
+           pager, groff or plain. With auto, the format is pager or plain
+           whenever the TERM env var is dumb or undefined.
+
+       -q, --quiet
+           Be quiet. Takes over -v and --verbosity.
+
+       -v, --verbose
+           Increase verbosity. Repeatable, but more than twice does not bring
+           more.
+
+       --verbosity=LEVEL (absent=warning or OWI_VERBOSITY env)
+           Be more or less verbose. LEVEL must be one of quiet, error,
+           warning, info or debug. Takes over -v.
+
+       --version
+           Show version information.
+
+EXIT STATUS
+       owi llvm exits with:
+
+       0   on success.
+
+       123 on indiscriminate errors reported on standard error.
+
+       124 on command line parsing errors.
+
+       125 on unexpected internal errors (bugs).
+
+ENVIRONMENT
+       These environment variables affect the execution of owi llvm:
+
+       OWI_VERBOSITY
+           See option --verbosity.
+
+BUGS
+       Email them to <contact@ndrs.fr>.
+
+SEE ALSO
+       owi(1)
+
+```
diff --git a/doc/src/manpages/owi.md b/doc/src/manpages/owi.md
index d5939b369..87f7bcaa8 100644
--- a/doc/src/manpages/owi.md
+++ b/doc/src/manpages/owi.md
@@ -35,6 +35,10 @@ COMMANDS
            Check the iso-functionnality of two Wasm modules by comparing the
            output when calling their exports.
 
+       llvm [OPTION]… FILE…
+           Compile LLVM IR/bitcode to Wasm and run the symbolic interpreter
+           on it
+
        replay [OPTION]… FILE
            Replay a module containing symbols with concrete values in a
            replay file containing a model

From b7211ba6b429a6d1ce2b32a3109abde3dde66fe7 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Mon, 27 Apr 2026 16:02:49 +0200
Subject: [PATCH 08/12] style(llvm): dune fmt

---
 src/cmd/cmd_llvm.ml  | 15 +++++++--------
 src/cmd/cmd_llvm.mli |  2 +-
 src/owi.mli          |  8 ++++----
 test/cram/llvm/dune  |  8 +++++++-
 4 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/cmd/cmd_llvm.ml b/src/cmd/cmd_llvm.ml
index d81369cfa..8399292d1 100644
--- a/src/cmd/cmd_llvm.ml
+++ b/src/cmd/cmd_llvm.ml
@@ -9,8 +9,7 @@ let resolve_binary name =
   match OS.Cmd.resolve @@ Cmd.v name with
   | Error _ ->
     Fmt.error_msg
-      "The `%s` binary was not found, please make sure it is in your path."
-      name
+      "The `%s` binary was not found, please make sure it is in your path." name
   | Ok _ as ok -> ok
 
 let err_output =
@@ -30,8 +29,8 @@ let bitcode_of_input ~workspace ~llvm_as_bin file : Fpath.t Result.t =
       | Error (`Msg e) ->
         Log.debug (fun m -> m "llvm-as failed: %s" e);
         Fmt.error_msg
-          "llvm-as failed: run with -vv to get the full error message if it was \
-           not displayed above"
+          "llvm-as failed: run with -vv to get the full error message if it \
+           was not displayed above"
     in
     out_bc
   | ext ->
@@ -45,9 +44,7 @@ let compile ~workspace ~entry_point ~out_file (files : Fpath.t list) :
   let* llc_bin = resolve_binary "llc" in
   let* wasmld_bin = resolve_binary "wasm-ld" in
 
-  let* bc_files =
-    list_map (bitcode_of_input ~workspace ~llvm_as_bin) files
-  in
+  let* bc_files = list_map (bitcode_of_input ~workspace ~llvm_as_bin) files in
 
   let files_bc = Cmd.of_list (List.map Cmd.p bc_files) in
   let llc_cmd : Cmd.t =
@@ -63,7 +60,9 @@ let compile ~workspace ~entry_point ~out_file (files : Fpath.t list) :
       Fmt.error_msg "llc failed: run with -vv to get the full error message"
   in
 
-  let files_o = Cmd.of_list (List.map (fun file -> Cmd.p Fpath.(file -+ ".o")) bc_files) in
+  let files_o =
+    Cmd.of_list (List.map (fun file -> Cmd.p Fpath.(file -+ ".o")) bc_files)
+  in
 
   let out = Option.value ~default:Fpath.(workspace / "a.out.wasm") out_file in
 
diff --git a/src/cmd/cmd_llvm.mli b/src/cmd/cmd_llvm.mli
index 1016ede60..e95076f63 100644
--- a/src/cmd/cmd_llvm.mli
+++ b/src/cmd/cmd_llvm.mli
@@ -6,4 +6,4 @@ val cmd :
      symbolic_parameters:Symbolic_parameters.t
   -> files:Fpath.t list
   -> out_file:Fpath.t option
-  -> unit Result.t
\ No newline at end of file
+  -> unit Result.t
diff --git a/src/owi.mli b/src/owi.mli
index 4845caa98..6a5e87b53 100644
--- a/src/owi.mli
+++ b/src/owi.mli
@@ -1757,10 +1757,10 @@ end
 
 module Cmd_llvm : sig
   val cmd :
-      symbolic_parameters:Symbolic_parameters.t
-  -> files:Fpath.t list
-  -> out_file:Fpath.t option
-  -> unit Result.t
+       symbolic_parameters:Symbolic_parameters.t
+    -> files:Fpath.t list
+    -> out_file:Fpath.t option
+    -> unit Result.t
 end
 
 module Cmd_replay : sig
diff --git a/test/cram/llvm/dune b/test/cram/llvm/dune
index 354d3ca30..50f102aa8 100644
--- a/test/cram/llvm/dune
+++ b/test/cram/llvm/dune
@@ -1,3 +1,9 @@
 (cram
- (deps %{bin:owi} bad.txt simple.ll simple.bc trap_div_zero.ll trap_div_zero.bc)
+ (deps
+  %{bin:owi}
+  bad.txt
+  simple.ll
+  simple.bc
+  trap_div_zero.ll
+  trap_div_zero.bc)
  (alias quicktest))

From e4f3ca5e0de815813ec5515a674f50a6ee4f88db Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Mon, 27 Apr 2026 17:02:18 +0200
Subject: [PATCH 09/12] fix(llvm cramtest): remove unnecessary target triple
 from .ll files cramtest

---
 src/cmd/cmd_llvm.ml             |   4 +++-
 test/cram/llvm/simple.bc        | Bin 1180 -> 1116 bytes
 test/cram/llvm/simple.ll        |   2 --
 test/cram/llvm/trap_div_zero.bc | Bin 1200 -> 1140 bytes
 test/cram/llvm/trap_div_zero.ll |   2 --
 5 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/cmd/cmd_llvm.ml b/src/cmd/cmd_llvm.ml
index 8399292d1..4a8c1276e 100644
--- a/src/cmd/cmd_llvm.ml
+++ b/src/cmd/cmd_llvm.ml
@@ -48,7 +48,9 @@ let compile ~workspace ~entry_point ~out_file (files : Fpath.t list) :
 
   let files_bc = Cmd.of_list (List.map Cmd.p bc_files) in
   let llc_cmd : Cmd.t =
-    Cmd.(llc_bin % "-O0" % "-march=wasm32" % "-filetype=obj" %% files_bc)
+    Cmd.(
+      llc_bin % "-O0" % "-march=wasm32" % "-mtriple=wasm32-unknown-unknown"
+      % "-filetype=obj" %% files_bc )
   in
 
   let* () =
diff --git a/test/cram/llvm/simple.bc b/test/cram/llvm/simple.bc
index f1ff4cca5d05ccb3f18f1dc5203d9286fc72fbf7..5f4e73b872e924bea0dd9b287350302face2721e 100644
GIT binary patch
delta 103
zcmbQkd52?y3M0!z)!FJ&iaawtI6mvN?ALMDYT#f%0vrxW%?^Pr3=9nsJe#>0-I?|N
nGQy-|c^DYjfgB;`DZ;slnR$jLdIow1#hJMUIjMR%IbdY~nxz#>

delta 166
zcmcb^F^6-43M21C)!E*{YpOZgD>K?HCp4R_U@wngFRy5?E@($$v-b+L`KYv1iXDod
zrYP#b!hi%=6gE08$Z%m`aL{36*!bL?*{h8SCLPPez`zIO2r*B|1c~J)X66~1=o#o4
flqVMF8XM`B=4I#Qm*>Ig;>_HFoK(G>9H;>RVx%kp

diff --git a/test/cram/llvm/simple.ll b/test/cram/llvm/simple.ll
index 30a63198e..6266b98be 100644
--- a/test/cram/llvm/simple.ll
+++ b/test/cram/llvm/simple.ll
@@ -1,5 +1,3 @@
-target triple = "wasm32-unknown-unknown"
-
 define i32 @main() {
 entry:
   ret i32 0
diff --git a/test/cram/llvm/trap_div_zero.bc b/test/cram/llvm/trap_div_zero.bc
index 246395204a768ec967fe9e1a896a35e48d8104f7..b15ac3947827756179b4a178cd22a5428fa8f73b 100644
GIT binary patch
delta 116
zcmdnM`GsSG3M0ov)!8~yiaeaYf*<}c2mO^4wEVY;XC;FY0}@bR=;UQ`m1JUINHW|k
zz!=1A_Ky)J9m~VOzzO6CF;9`oP0Y+QG|@BAGbkxaEQn9ZEQ_y7Ey~x+$$_W_00QnA
AH~;_u

delta 175
zcmeyuv4L}f3Zvje)!6~UYpOZgD>K?HCp4R_U@wngFRy5?E@($$v-b+LwJhVP_{X^N
zUr&cjePmk*gCGME5NJ5U*0@NNk%3{O1jEKRLCk*bOfczK9tH+}AV-LKN&!eLH!(BM
s&_vHb&!9Z9IM>)nw=^$1FTXqwMwb*N7R0Aymc>`47Uk>Z<bd=50Fsz9R{#J2

diff --git a/test/cram/llvm/trap_div_zero.ll b/test/cram/llvm/trap_div_zero.ll
index 6ff4a871a..c7f5ad34b 100644
--- a/test/cram/llvm/trap_div_zero.ll
+++ b/test/cram/llvm/trap_div_zero.ll
@@ -1,5 +1,3 @@
-target triple = "wasm32-unknown-unknown"
-
 define i32 @main() {
 entry:
   %x = sdiv i32 1, 0

From e347f7b18ad7bb9f6dcadd91055001f7d7bf7710 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Mon, 27 Apr 2026 18:52:19 +0200
Subject: [PATCH 10/12] build(cmdliner): update to 2.1.1

---
 dune-project | 2 +-
 owi.opam     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/dune-project b/dune-project
index 90849931f..1c16775e9 100644
--- a/dune-project
+++ b/dune-project
@@ -59,7 +59,7 @@
   (bos
    (>= 0.2.1))
   (cmdliner
-   (>= 2.1.0))
+   (>= 2.1.1))
   (digestif
    (>= 1.2.0))
   (domainpc
diff --git a/owi.opam b/owi.opam
index dd6218b30..13258b6a3 100644
--- a/owi.opam
+++ b/owi.opam
@@ -31,7 +31,7 @@ depends: [
   "dune-site" {build}
   "conf-clang"
   "bos" {>= "0.2.1"}
-  "cmdliner" {>= "2.1.0"}
+  "cmdliner" {>= "2.1.1"}
   "digestif" {>= "1.2.0"}
   "domainpc" {>= "0.2"}
   "logs" {>= "0.10.0"}

From 508ab6ceba5932585ba176cea49f613d5efec3d2 Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Tue, 28 Apr 2026 15:07:47 +0200
Subject: [PATCH 11/12] test(llvm): update cramtest ouput for empty.t and
 not_exists.t

---
 test/cram/llvm/empty.t      | 3 +--
 test/cram/llvm/not_exists.t | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/test/cram/llvm/empty.t b/test/cram/llvm/empty.t
index 10b2ca835..53988fba1 100644
--- a/test/cram/llvm/empty.t
+++ b/test/cram/llvm/empty.t
@@ -1,5 +1,4 @@
   $ owi llvm
+  Usage: owi llvm [--help] [OPTION]… FILE…
   owi: required argument FILE is missing
-  Usage: owi llvm [OPTION]… FILE…
-  Try 'owi llvm --help' or 'owi --help' for more information.
   [124]
diff --git a/test/cram/llvm/not_exists.t b/test/cram/llvm/not_exists.t
index 9f1127652..d2d7e0744 100644
--- a/test/cram/llvm/not_exists.t
+++ b/test/cram/llvm/not_exists.t
@@ -1,5 +1,4 @@
   $ owi llvm not_exists.bc
+  Usage: owi llvm [--help] [OPTION]… FILE…
   owi: FILE… arguments: no file 'not_exists.bc'
-  Usage: owi llvm [OPTION]… FILE…
-  Try 'owi llvm --help' or 'owi --help' for more information.
   [124]

From 9d2fcdbb5a7a90417d1ad0d50221bd12ae4450de Mon Sep 17 00:00:00 2001
From: LIN leo <leo.lin@etu.u-paris.fr>
Date: Wed, 29 Apr 2026 17:16:38 +0200
Subject: [PATCH 12/12] docs(llvm): update llvm doc via dune promote

---
 doc/src/manpages/owi-llvm.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/doc/src/manpages/owi-llvm.md b/doc/src/manpages/owi-llvm.md
index e06a0ceb7..da1ea031b 100644
--- a/doc/src/manpages/owi-llvm.md
+++ b/doc/src/manpages/owi-llvm.md
@@ -21,7 +21,7 @@ OPTIONS
        --entry-point=FUNCTION
            entry point of the executable
 
-       --exploration=VAL (absent=fifo)
+       --exploration=VALUE (absent=fifo)
            exploration strategy to use ("fifo", "lifo", "random",
            "random-unseen-then-random", "rarity", "hot-path-penalty",
            "rarity-aging", "rarity-depth-aging", "rarity-depth-loop-aging",
@@ -37,8 +37,8 @@ OPTIONS
            Invoke the entry point of the program with symbolic values instead
            of dummy constants.
 
-       --model-format=VAL (absent=scfg)
-          The format of the model ("json" or "scfg")
+       --model-format=VALUE (absent=scfg)
+            The format of the model ("json" or "scfg")
 
        --model-out-file=FILE
            Output the generated model to FILE. if --no-stop-at-failure is
@@ -79,7 +79,7 @@ OPTIONS
        -u, --unsafe
            skip typechecking pass
 
-       -w VAL, --workers=VAL (absent=n)
+       -w INT, --workers=INT (absent=n)
            Number of workers for symbolic execution. Defaults to the number
            of physical cores.