add owi cpp

CHANGES.md

@@ -23,6 +23,7 @@
 - add `owi wat2wasm` subcommand
 - add a `no-assert-failure-expression-printing` flag to `owi c`, `owi sym` and `owi conc`
 - add `owi version` subcommand
+- add `owi c++` subcommand
 
 ## 0.2 - 2024-04-24
 

README.md

@@ -3,6 +3,7 @@
 [Owi] is a toolchain to work with WebAssembly. It is written in [OCaml]. It provides a binary with many subcommands:
 
 - [`owi c`]: a bug finding tool for C code that performs symbolic execution by compiling to Wasm and using our symbolic Wasm interpreter;
+- [`owi c++`]: a bug finding tool for C++ code that performs symbolic execution by compiling to Wasm and using our symbolic Wasm interpreter;
 - [`owi conc`]: a concolic Wasm interpreter;
 - [`owi fmt`]: a formatter for Wasm;
 - [`owi opt`]: an optimizer for Wasm;
@@ -218,6 +219,7 @@ This project was partly funded through the [NGI0 Core] Fund, a fund established
 [JS Promise Integration]: https://github.com/WebAssembly/js-promise-integration
 
 [`owi c`]: example/c
+[`owi c++`]: example/cpp
 [`owi conc`]: example/conc
 [`owi fmt`]: example/fmt
 [`owi opt`]: example/opt

dune-project

@@ -88,4 +88,4 @@
   (cohttp :with-dev-setup)
   (cohttp-lwt-unix :with-dev-setup)
   )
- (sites (share binc) (share libc)))
+ (sites (share binc) (share libc) (share bincpp) (share libcpp)))

example/README.md

@@ -3,6 +3,7 @@
 ## Owi binary
 
 - [`owi c`]
+- [`owi c++`]
 - [`owi conc`]
 - [`owi fmt`]
 - [`owi opt`]
@@ -95,6 +96,7 @@ BUGS
 ```
 
 [`owi c`]: ./c
+[`owi c++`]: ./cpp
 [`owi conc`]: ./conc
 [`owi fmt`]: ./fmt
 [`owi opt`]: ./opt

example/cpp/README.md

@@ -0,0 +1,197 @@
+# Performing symbolic execution on C++ programs
+
+## Solving polynomials
+
+Given the following `poly.cpp` file:
+
+<!-- $MDX file=poly.cpp -->
+```c
+#include <owi.h>
+
+int main() {
+  int x = owi_i32();
+  int x2 = x * x;
+  int x3 = x * x * x;
+
+  int a = 1;
+  int b = -7;
+  int c = 14;
+  int d = -8;
+
+  int poly = a * x3 + b * x2 + c * x + d;
+
+  owi_assert(poly != 0);
+
+  return 0;
+}
+```
+
+We are defining one symbolic variable `x` using the function `owi_i32(void)`. Then we build a polynomial `poly` equal to $x^3 - 7x^2 + 14x - 8$.
+
+Then we use `owi_assert(poly != 0)`. Which should fail as this polynomial has multiple roots. Let's see what owi says about it:
+
+```sh
+$ owi c++ ./poly.cpp -w1 --no-assert-failure-expression-printing
+Assert failure
+model {
+  symbol symbol_0 i32 4
+}
+Reached problem!
+[13]
+```
+
+Indeed, `4` is a root of the polynomial and thus it is expected to be equal to `0` in this case. We know the three roots are `1`, `2` and `4`, so let's inform owi that we are not interested in this cases.
+
+We can do so by assuming that `x` is not equal to any of these with the function `owi_assume(bool)`:
+
+<!-- $MDX file=poly2.cpp -->
+```c
+#include <owi.h>
+
+int main() {
+  int x = owi_i32();
+  int x2 = x * x;
+  int x3 = x * x * x;
+
+  int a = 1;
+  int b = -7;
+  int c = 14;
+  int d = -8;
+
+  int poly = a * x3 + b * x2 + c * x + d;
+
+  owi_assume(x != 1);
+  owi_assume(x != 2);
+  owi_assume(x != 4);
+
+  // Make model output deterministic
+  owi_assume(x > -2147483646);
+
+  owi_assert(poly != 0);
+
+  return 0;
+}
+```
+
+Let's run owi on this new input:
+
+
+```sh
+$ owi c++ ./poly2.cpp --no-assert-failure-expression-printing
+Assert failure
+model {
+  symbol symbol_0 i32 -2147483644
+}
+Reached problem!
+[13]
+```
+
+And indeed, `-2147483644` is a root of the polynomial! Well, not quite…
+
+Remember that we are working on 32 bits integers here. Thus *overflows* are a thing we have to think about. And indeed when `x` is equal to `-2147483644`, because of overflows, the polynomial will be equal to zero.
+
+Exercise: can you find another "root" of the polynomial ? :-)
+
+## Man page
+
+```sh
+$ owi c++ --help=plain
+NAME
+       owi-c - Compile a C file to Wasm and run the symbolic interpreter on
+       it
+
+SYNOPSIS
+       owi c [OPTION]… [ARG]…
+
+OPTIONS
+       --concolic
+           concolic mode
+
+       -d, --debug
+           debug mode
+
+       --deterministic-result-order
+           Guarantee a fixed deterministic order of found failures. This
+           implies --no-stop-at-failure.
+
+       --e-acsl
+           e-acsl mode, refer to
+           https://frama-c.com/download/e-acsl/e-acsl-implementation.pdf for
+           Frama-C's current language feature implementations
+
+       --fail-on-assertion-only
+           ignore traps and only report assertion violations
+
+       --fail-on-trap-only
+           ignore assertion violations and only report traps
+
+       -I VAL
+           headers path
+
+       -m VAL, --arch=VAL (absent=32)
+           data model
+
+       --no-assert-failure-expression-printing
+           do not display the expression in the assert failure
+
+       --no-stop-at-failure
+           do not stop when a program failure is encountered
+
+       --no-value
+           do not display a value for each symbol
+
+       -O VAL (absent=3)
+           specify which optimization level to use
+
+       -o VAL, --outpt=VAL (absent=owi-out)
+           write results to dir
+
+       --optimize
+           optimize mode
+
+       -p, --profiling
+           profiling mode
+
+       --property=VAL
+           property file
+
+       -s VAL, --solver=VAL (absent=Z3)
+           SMT solver to use
+
+       --testcomp
+           test-comp mode
+
+       -u, --unsafe
+           skip typechecking pass
+
+       -w VAL, --workers=VAL (absent=n)
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
+
+COMMON OPTIONS
+       --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.
+
+       --version
+           Show version information.
+
+EXIT STATUS
+       owi c 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).
+
+BUGS
+       Email them to <contact@ndrs.fr>.
+
+SEE ALSO
+       owi(1)
+
+```

example/cpp/dune

@@ -0,0 +1,8 @@
+(mdx
+ (libraries owi)
+ (deps
+  %{bin:owi}
+  (file poly.cpp)
+  (file poly2.cpp)
+  (package owi))
+ (files README.md))

example/cpp/poly.cpp

@@ -0,0 +1,27 @@
+#include <owi.h>
+
+/*
+extern "C" {
+  void _start() {
+    owi_abort();
+  }
+}
+*/
+
+
+int main() {
+  int x = owi_i32();
+  int x2 = x * x;
+  int x3 = x * x * x;
+
+  int a = 1;
+  int b = -7;
+  int c = 14;
+  int d = -8;
+
+  int poly = a * x3 + b * x2 + c * x + d;
+
+  owi_assert(poly != 0);
+
+  return 0;
+}

example/cpp/poly2.cpp

@@ -0,0 +1,25 @@
+#include <owi.h>
+
+int main() {
+  int x = owi_i32();
+  int x2 = x * x;
+  int x3 = x * x * x;
+
+  int a = 1;
+  int b = -7;
+  int c = 14;
+  int d = -8;
+
+  int poly = a * x3 + b * x2 + c * x + d;
+
+  owi_assume(x != 1);
+  owi_assume(x != 2);
+  owi_assume(x != 4);
+
+  // Make model output deterministic
+  owi_assume(x > -2147483646);
+
+  owi_assert(poly != 0);
+
+  return 0;
+}

src/bin/owi.ml

@@ -138,6 +138,45 @@ let workspace =
   let doc = "write results to dir" in
   Arg.(value & opt path_conv (Fpath.v "owi-out") & info [ "outpt"; "o" ] ~doc)
 
+(* owi cpp *)
+
+let cpp_info =
+  let doc =
+    "Compile a C++ file to Wasm and run the symbolic interpreter on it"
+  in
+  let man = [] @ shared_man in
+  Cmd.info "c++" ~version ~doc ~sdocs ~man
+
+let cpp_cmd =
+  let+ arch =
+    let doc = "data model" in
+    Arg.(value & opt int 32 & info [ "arch"; "m" ] ~doc)
+  and+ includes =
+    let doc = "headers path" in
+    Arg.(value & opt_all existing_dir_conv [] & info [ "I" ] ~doc)
+  and+ opt_lvl =
+    let doc = "specify which optimization level to use" in
+    Arg.(value & opt string "3" & info [ "O" ] ~doc)
+  and+ concolic =
+    let doc = "concolic mode" in
+    Arg.(value & flag & info [ "concolic" ] ~doc)
+  and+ debug
+  and+ workers
+  and+ files
+  and+ profiling
+  and+ unsafe
+  and+ optimize
+  and+ no_stop_at_failure
+  and+ no_value
+  and+ no_assert_failure_expression_printing
+  and+ deterministic_result_order
+  and+ fail_mode
+  and+ solver in
+  Cmd_cpp.cmd ~debug ~arch ~workers ~opt_lvl ~includes ~files ~profiling ~unsafe
+    ~optimize ~no_stop_at_failure ~no_value
+    ~no_assert_failure_expression_printing ~deterministic_result_order
+    ~fail_mode ~concolic ~solver
+
 (* owi c *)
 
 let c_info =
@@ -422,6 +461,7 @@ let cli =
   in
   Cmd.group info ~default
     [ Cmd.v c_info c_cmd
+    ; Cmd.v cpp_info cpp_cmd
     ; Cmd.v fmt_info fmt_cmd
     ; Cmd.v opt_info opt_cmd
     ; Cmd.v instrument_info instrument_cmd

src/cmd/cmd_c.ml

@@ -11,9 +11,9 @@ type metadata =
   ; files : Fpath.t list
   }
 
-let binc_location = List.map Fpath.v C_share_site.Sites.binc
+let binc_location = List.map Fpath.v Share.Sites.binc
 
-let libc_location = List.map Fpath.v C_share_site.Sites.libc
+let libc_location = List.map Fpath.v Share.Sites.libc
 
 let find location file : Fpath.t Result.t =
   let* l =
@@ -125,7 +125,7 @@ let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t =
     | Error (`Msg e) ->
       Error
         (`Msg
-           (Fmt.str "Clang failed: %s"
+           (Fmt.str "clang failed: %s"
               ( if debug then e
                 else "run with --debug to get the full error message" ) ) )
   in