diff --git a/CHANGES.md b/CHANGES.md index 0db836b9..00bb0cc9 100644 --- a/CHANGES.md +++ b/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 diff --git a/README.md b/README.md index 55a4b976..e98f4cc1 100644 --- a/README.md +++ b/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 diff --git a/dune-project b/dune-project index 7eb8f727..bd40398b 100644 --- a/dune-project +++ b/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))) diff --git a/example/README.md b/example/README.md index 03322c8f..3bd69719 100644 --- a/example/README.md +++ b/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 diff --git a/example/cpp/README.md b/example/cpp/README.md new file mode 100644 index 00000000..64f6464b --- /dev/null +++ b/example/cpp/README.md @@ -0,0 +1,197 @@ +# Performing symbolic execution on C++ programs + +## Solving polynomials + +Given the following `poly.cpp` file: + + +```c +#include + +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)`: + + +```c +#include + +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 . + +SEE ALSO + owi(1) + +``` diff --git a/example/cpp/dune b/example/cpp/dune new file mode 100644 index 00000000..111c258a --- /dev/null +++ b/example/cpp/dune @@ -0,0 +1,8 @@ +(mdx + (libraries owi) + (deps + %{bin:owi} + (file poly.cpp) + (file poly2.cpp) + (package owi)) + (files README.md)) diff --git a/example/cpp/poly.cpp b/example/cpp/poly.cpp new file mode 100644 index 00000000..6426dec9 --- /dev/null +++ b/example/cpp/poly.cpp @@ -0,0 +1,27 @@ +#include + +/* +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; +} diff --git a/example/cpp/poly2.cpp b/example/cpp/poly2.cpp new file mode 100644 index 00000000..89402460 --- /dev/null +++ b/example/cpp/poly2.cpp @@ -0,0 +1,25 @@ +#include + +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; +} diff --git a/src/bin/owi.ml b/src/bin/owi.ml index d7ca59f1..3cfa1875 100644 --- a/src/bin/owi.ml +++ b/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 diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 19af221a..ff81e897 100644 --- a/src/cmd/cmd_c.ml +++ b/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 diff --git a/src/cmd/cmd_cpp.ml b/src/cmd/cmd_cpp.ml new file mode 100644 index 00000000..c3c843a1 --- /dev/null +++ b/src/cmd/cmd_cpp.ml @@ -0,0 +1,86 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +open Bos +open Syntax + +(* TODO: refactor to re-use code in Cmd_c.ml *) +let binc_location = List.map Fpath.v Share.Sites.binc + +let libc_location = List.map Fpath.v Share.Sites.libc + +let find location file : Fpath.t Result.t = + let* l = + list_map + (fun dir -> + let filename = Fpath.append dir file in + match OS.File.exists filename with + | Ok true -> Ok (Some filename) + | Ok false -> Ok None + | Error (`Msg msg) -> Error (`Msg msg) ) + location + in + let rec loop = function + | [] -> Error (`Msg (Fmt.str "can't find file %a" Fpath.pp file)) + | None :: tl -> loop tl + | Some file :: _tl -> Ok file + in + loop l + +let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t = + let flags = + let stack_size = 8 * 1024 * 1024 |> string_of_int in + let includes = Cmd.of_list ~slip:"-I" (List.map Fpath.to_string includes) in + Cmd.( + of_list + [ Fmt.str "-O%s" opt_lvl + ; "--target=wasm32" + ; "-m32" + ; "-ffreestanding" + ; "--no-standard-libraries" + ; "-Wno-everything" + ; "-flto=thin" + ; (* LINKER FLAGS: *) + "-Wl,--entry=main" + ; "-Wl,--export=main" + (* TODO: allow this behind a flag, this is slooooow *) + ; "-Wl,--lto-O0" + ; Fmt.str "-Wl,-z,stack-size=%s" stack_size + ] + %% includes ) + in + + let* clangpp_bin = OS.Cmd.resolve @@ Cmd.v "clang++" in + + let out = Fpath.(v "a.out.wasm") in + + let* libc = find binc_location (Fpath.v "libc.wasm") in + + let files = Cmd.of_list (List.map Fpath.to_string (libc :: files)) in + let clangpp : Cmd.t = Cmd.(clangpp_bin %% flags % "-o" % p out %% files) in + + let+ () = + match OS.Cmd.run clangpp with + | Ok _ as v -> v + | Error (`Msg e) -> + Error + (`Msg + (Fmt.str "clang++ failed: %s" + ( if debug then e + else "run with --debug to get the full error message" ) ) ) + in + + out + +let 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 : unit Result.t = + let includes = libc_location @ includes in + let* modul = compile ~includes ~opt_lvl debug files in + let files = [ modul ] in + (if concolic then Cmd_conc.cmd else Cmd_sym.cmd) + ~profiling ~debug ~unsafe ~rac:false ~srac:false ~optimize ~workers + ~no_stop_at_failure ~no_value ~no_assert_failure_expression_printing + ~deterministic_result_order ~fail_mode ~workspace:(Fpath.v "owi-out") + ~solver ~files diff --git a/src/cmd/cmd_cpp.mli b/src/cmd/cmd_cpp.mli new file mode 100644 index 00000000..7d782a16 --- /dev/null +++ b/src/cmd/cmd_cpp.mli @@ -0,0 +1,22 @@ +(* SPDX-License-Identifier: AGPL-3.0-or-later *) +(* Copyright © 2021-2024 OCamlPro *) +(* Written by the Owi programmers *) + +val cmd : + debug:bool + -> arch:int + -> workers:int + -> opt_lvl:string + -> includes:Fpath.t list + -> files:Fpath.t list + -> profiling:bool + -> unsafe:bool + -> optimize:bool + -> no_stop_at_failure:bool + -> no_value:bool + -> no_assert_failure_expression_printing:bool + -> deterministic_result_order:bool + -> fail_mode:Cmd_sym.fail_mode + -> concolic:bool + -> solver:Smtml.Solver_type.t + -> unit Result.t diff --git a/src/dune b/src/dune index fc8bde35..ea309565 100644 --- a/src/dune +++ b/src/dune @@ -11,10 +11,10 @@ binary_to_text binary_types binary_validate - c_share_site choice_intf cmd_utils cmd_c + cmd_cpp cmd_fmt cmd_instrument cmd_opt @@ -66,6 +66,7 @@ runtime script sexp + share solver symbolic symbolic_choice @@ -141,5 +142,5 @@ (-w +a-4-40-41-42-44-45-70-73 -warn-error +a)))) (generate_sites_module - (module c_share_site) + (module share) (sites owi)) diff --git a/src/libc/include/owi.h b/src/libc/include/owi.h index 1a1670b9..12f28892 100644 --- a/src/libc/include/owi.h +++ b/src/libc/include/owi.h @@ -1,6 +1,11 @@ #ifndef _OWI_H #define _OWI_H + +#ifdef __cplusplus +extern "C" +{ +#endif __attribute__((import_module("summaries"), import_name("alloc"))) void * owi_malloc(void *, unsigned int); __attribute__((import_module("summaries"), import_name("dealloc"))) void * @@ -18,7 +23,12 @@ __attribute__((import_module("symbolic"), import_name("f32_symbol"))) float owi_f32(void); __attribute__((import_module("symbolic"), import_name("f64_symbol"))) double owi_f64(void); -__attribute__((import_module("symbolic"), import_name("bool_symbol"))) _Bool +__attribute__((import_module("symbolic"), import_name("bool_symbol"))) +#ifdef __cplusplus + bool +#elif + _Bool +#endif owi_bool(void); __attribute__((import_module("symbolic"), import_name("assume"))) void @@ -31,4 +41,9 @@ owi_abort(void); __attribute__((import_module("summaries"))) __attribute__((import_name("exit"))) void owi_exit(int); +#ifdef __cplusplus +} +#endif + + #endif