add a owi llvm or owi bc command

[FUJIZZ]

What does this PR do ?

Add a command to compile .ll and .bc files.
Add llvm command cramtests.
Add llvm command docs.

Not a native symbolic execution for LLVM -> convert files into wasm and then use Owi Symbolic Execution.
Here is the pipeline to compile the LLVM file (in the order).

• llvm-as : .ll file -> .bc file
• llc : bitcode compilation -> .o wasm files
• wasm-ld : link .o files to produce final wasm file
• Owi symex executed on the wasm file

Why this change needed ?

Add a new command to facilitate .bc and .ll files.

How to test ?

The following cramtest are provided to validate the feature :

./test/cram/llvm/empty.t
./test/cram/llvm/not_exists.t
./test/cram/llvm/simple.t
./test/cram/llvm/trap_div_zero.t
./test/cram/llvm/unsupported_ext.t

To test :

dune runtest {test}

Issue

Closes #300

N-B: This contribution is part of work carried out as a student at Université Paris-Cité.
Apologies if this is inappropriate or if the contribution does not meet the project's standards, any feedback is welcome.

[redianthus]

Hi !

Thanks for the contribution. I think you need to run dune fmt (with the correct ocamlformat version installed) for the Nix CI to pass (the others CI are broken and you can ignore them).

[redianthus]

Is this really necessary? I think it'd be better if we could omit this from the llvm file and simply pass it inside Owi when calling llvm. It will allow people to use it on any llvm file rather than on file that were made specifically for Wasm (but I don't know if it's possible as I'm not familiar with llvm).

[FUJIZZ]

Yes, I agree with you and I can remove it.
The target is already enforced by the option -march=wasm32, in the command llc , in cmd_llvm.ml file.
We can eventually add the target triple option in the llc command with the option -mtriple=wasm32-unknown-unknown if necessary.

[redianthus]

Yes, I think it would be much better!

[FUJIZZ]

It still work if we remove the line though.

Moreover, I didn't test my code with any other env/distro, so I don't known if the compilation may fail.

[FUJIZZ]

I have made the corrections you suggested to me, but the Nix CI seems still fail, even after dune fmt.

[redianthus]

Yes, this time it seems you are using an old version of cmdliner and the output is different which makes the cram tests fail. Which version of cmdliner are you using? Could you try to use a more recent one? (If you use opam, it may be that our opam file is not updated to use the latest cmdliner version, in which case, you could fix it along the way by changing dune-project and then dune build owi.opam).

[FUJIZZ]

Yes I was using cmdliner 1.3.0, I updated it manually to 2.1.1 version.

I also updated the dune-project file.

[redianthus]

Thanks! You need to run dune runtest and then dune promote now.

[FUJIZZ]

Actually, when I'm running dune runtest, there is a lot of test (not llvm's ones) with different outputs from the original outputs.

I seems like there is a problem with my env (missing deps or other...).
Therefore, I'm not sure about dune promote now.

Maybe I can show you through Zulip?

[redianthus]

Looks all good now, thanks for the contribution! :)