- Removed the unused lib/rust files

INSTALL.md

@@ -27,6 +27,7 @@ is required to compile everything from source.
 - autoconf >= 2.63 and automake >= 1.11.1 (if building from git)
 - gmp
 - mpfr
+- charon = 0.1.123 (only needed for the Rust analysis, instructions [here](https://github.com/AeneasVerif/charon))
 
 You can install some of these dependencies using
 [Homebrew](http://brew.sh/):
@@ -49,6 +50,7 @@ is required to compile everything from source.
 - CMake (only needed for the C/Objective-C analysis)
 - Ninja (optional, if you wish to use sequential linking when building the
   C/Objective-C analysis)
+- charon = 0.1.123 (only needed for the Rust analysis, instructions [here](https://github.com/AeneasVerif/charon))
 
 See also the distro-specific instructions for Ubuntu and Debian below.
 

build-infer.sh

@@ -167,6 +167,18 @@ if [ "$BUILD_CLANG" == "no" ] && [ "$BUILD_ERLANG" == "no" ] && \
   build_all
 fi
 
+CHARON_VERSION="0.1.123"
+CHARON_VERSION_COMMIT="4289a52cc427ac6f8ecbb746e2b226f5b297be40"
+# Check for charon on path when rust is enabled
+if [ "$BUILD_RUST" == "yes" ]; then
+  if [[ $(charon version) != "$CHARON_VERSION" ]] then
+    echo "Warning: charon command not found or charon is the incorrect version (is it on your PATH ?)"
+    echo "The rust analyzer requires version $CHARON_VERSION of the charon library" 
+    echo "You can download charon from https://github.com/AeneasVerif/charon/tree/$CHARON_VERSION_COMMIT"
+    exit 1
+  fi
+fi
+
 # enable --yes option for some commands in non-interactive mode
 YES=
 if [ "$INTERACTIVE" == "no" ]; then
@@ -190,8 +202,8 @@ install_opam_deps () {
     fi
 
     # Charon Version 0.1.123
-    opam pin add --no-action charon https://github.com/AeneasVerif/charon.git#4289a52cc427ac6f8ecbb746e2b226f5b297be40
-    opam pin add --no-action name_matcher_parser https://github.com/AeneasVerif/charon.git#4289a52cc427ac6f8ecbb746e2b226f5b297be40
+    opam pin add --no-action charon https://github.com/AeneasVerif/charon.git#$CHARON_VERSION_COMMIT
+    opam pin add --no-action name_matcher_parser https://github.com/AeneasVerif/charon.git#$CHARON_VERSION_COMMIT
     opam pin add --no-action ppx_show "$INFER_ROOT"/dependencies/ppx_show
     opam pin add --no-action pyml "$INFER_ROOT"/dependencies/pyml
     # camlzip checks that it is within the required version that the zip/jar file declares as

infer/src/integration/Rust.ml

@@ -6,20 +6,43 @@
  *)
 open! IStd
 module L = Logging
+module F = Format
+
+let run_charon json_file prog args =
+  let escaped_cmd = List.map ~f:Escape.escape_shell args |> String.concat ~sep:" " in
+  let redirected_cmd =
+    F.sprintf "charon %s --ullbc --dest-file %s -- %s" prog json_file escaped_cmd
+  in
+  let {IUnix.Process_info.stdin; stdout; stderr; pid} =
+    IUnix.create_process ~prog:"sh" ~args:["-c"; redirected_cmd]
+  in
+  Unix.close stdin ;
+  Unix.close stderr ;
+  let stdout = Unix.in_channel_of_descr stdout in
+  (pid, stdout)
+
+
+let compile prog args =
+  let json_file = IFilename.temp_file ~in_dir:(ResultsDir.get_path Temporary) "charon" ".ullbc" in
+  let pid, stdout = run_charon json_file prog args in
+  let output = In_channel.input_lines stdout |> String.concat ~sep:"\n" in
+  In_channel.close stdout ;
+  match IUnix.waitpid pid with
+  | Error _ as status ->
+      L.die ExternalError "Rustc exited with: %s@\n Trace: %s\n"
+        (IUnix.Exit_or_signal.to_string_hum status)
+        output
+  | Ok () ->
+      json_file
+
 
 let capture prog (args : string list) =
   if not (String.equal prog "rustc") then
     L.die UserError "rustc should be explicitly used instead of %s." prog ;
-  let json_file =
-    match List.hd args with
-    | Some json_file ->
-        json_file
-    | None ->
-        L.die UserError "No arguments provided, missing argument json_file"
-  in
+  let json_file = compile prog args in
   let json = Yojson.Basic.from_file json_file in
   match Charon.UllbcOfJson.crate_of_json json with
   | Ok _crate ->
-      Printf.printf "success"
+      Printf.printf "Success: %s" json_file
   | Error err ->
       L.die UserError "%s: %s" err (Yojson.Basic.to_string json)

infer/src/rust/unit/RustMir2TextualTest.ml

@@ -8,23 +8,46 @@
 open! IStd
 module F = Format
 
-let program_path = "./programs"
+let run_charon json_file rust_file =
+  let redirected_cmd =
+    F.sprintf "charon rustc --ullbc --dest-file %s -- %s --crate-name \"dummy\"" json_file rust_file
+  in
+  let {IUnix.Process_info.stdin; stderr} =
+    IUnix.create_process ~prog:"sh" ~args:["-c"; redirected_cmd]
+  in
+  Unix.close stdin ;
+  In_channel.input_lines (Unix.in_channel_of_descr stderr) |> String.concat ~sep:"\n"
 
-let test json_filename =
+
+let test source =
+  let json_file = IFilename.temp_file "charon" ".ullbc" in
+  let rust_file = IFilename.temp_file "dummy" ".rs" in
+  Out_channel.write_all rust_file ~data:source ;
+  let cmd_out = run_charon json_file rust_file in
   try
-    let file_path = Filename.concat program_path json_filename in
-    let json = Yojson.Basic.from_file file_path in
+    let json = Yojson.Basic.from_file json_file in
     match Charon.UllbcOfJson.crate_of_json json with
     | Ok _crate ->
         F.printf "Not yet implemented"
     | Error err ->
         F.printf "Test failed: %s" err
-  with e -> F.printf "%s" (Exn.to_string e)
+  with e -> F.printf "Exn %s\n Command output: %s" (Exn.to_string e) cmd_out
 
 (* An example test *)
-(*
-let%expect_test "example" =
-  test "./example.ullbc" ;
+(* let%expect_test "example" =
+  let source = 
+    {|
+#[allow(unused)]
+fn foo() {
+    let x = 42;
+}
+
+fn main(){
+    foo();
+}
+|} 
+  in
+  test source ;
   [%expect
     {|
   .source_language = "Rust"
@@ -57,5 +80,4 @@ let%expect_test "example" =
         unreachable
 
   }
-|}]
-*)
+|}] *)