Merge branch 'main' into docker_filter_syscalls

engine/DEV.md

@@ -42,3 +42,14 @@ To show the file nicely formated, use: `dune describe pp lib/types.ml` (or `dune
 
 You can also use `dune utop` and then `#show_type Hax_engine.Types.SOME_TYPE` and `#show_constructor Hax_engine.Types.SOME_CONSTRUCTOR`.
 
+## Debugging the phases
+You can enable a debug mode that prints a Rustish AST at each phase,
+that you can browse interactively along with the actual AST.
+
+Just add the flag `--debug-engine DIR` to the `into` subcommand, where
+`DIR` is a directory where will be outputted debug informations. Make
+sure to create the folder beforehand.
+
+To browse the debug information, run
+`./engine/utils/phase_debug_webapp/server.js DIR`. Note you can change
+to port by setting the environment variable `PORT`.

engine/backends/coq/coq/coq_backend.ml

@@ -306,7 +306,12 @@ struct
 
   (* let is_field_an_index = index_of_field >> Option.is_some *)
 
-  let rec pexpr (e : expr) : C.AST.term =
+  let rec pexpr (e : expr) =
+    try pexpr_unwrapped e
+    with Diagnostics.SpanFreeError kind ->
+      TODOs_debug.__TODO_term__ e.span "failure"
+
+  and pexpr_unwrapped (e : expr) : C.AST.term =
     let span = e.span in
     match e.e with
     | Literal e -> C.AST.Const (pliteral e)
@@ -386,6 +391,11 @@ struct
     | _ -> .
 
   let rec pitem (e : item) : C.AST.decl list =
+    try pitem_unwrapped e
+    with Diagnostics.SpanFreeError _kind ->
+      [ C.AST.Unimplemented "item error backend" ]
+
+  and pitem_unwrapped (e : item) : C.AST.decl list =
     let span = e.span in
     match e.v with
     | Fn { name; generics; body; params } ->

engine/backends/fstar/fstar_backend.ml

@@ -214,6 +214,22 @@ struct
     >> map_last_global_ident (fun s -> s ^ "_t")
     >> pglobal_ident span
 
+  (* This is a bit too fiddly. TODO: simplify *)
+  let pfield_concrete_ident (id : concrete_ident) =
+    let id_path = Non_empty_list.to_list id.path in
+    F.lid [ String.lowercase (List.last_exn id_path) ]
+
+  let pfield_ident span (f : global_ident) : F.Ident.lident =
+    match f with
+    | `Concrete cid -> pfield_concrete_ident cid
+    | `Projector (`TupleField (n, len)) | `TupleField (n, len) ->
+        F.lid [ "_" ^ Int.to_string (n + 1) ]
+    | `Projector (`Concrete cid) -> pfield_concrete_ident cid
+    | _ ->
+        Error.assertion_failure span
+          ("pfield_ident: not a valid field name in F* backend: "
+         ^ show_global_ident f)
+
   let pconstructor_ident span : global_ident -> F.Ident.lident =
     uppercase_global_ident >> pglobal_ident span
 
@@ -298,8 +314,8 @@ struct
                 (F.term_of_lid [ "FStar"; "List"; "Tot"; "Base"; "length" ])
                 [ x ]
             in
-            let lt = F.term @@ F.AST.Name (pprim_ident span @@ BinOp Lt) in
-            F.mk_e_app lt [ len_of_x; pexpr length ])
+            let eq = F.term @@ F.AST.Name (pprim_ident span @@ BinOp Eq) in
+            F.mk_e_app eq [ len_of_x; pexpr length ])
     | TParam i ->
         F.term
         @@ F.AST.Var
@@ -388,7 +404,7 @@ struct
         @@ F.AST.Project (pexpr arg, F.lid [ "_" ^ string_of_int (n + 1) ])
     | App { f = { e = GlobalVar (`Projector (`Concrete cid)) }; args = [ arg ] }
       ->
-        F.term @@ F.AST.Project (pexpr arg, pconcrete_ident cid)
+        F.term @@ F.AST.Project (pexpr arg, pfield_concrete_ident cid)
     | App { f = { e = GlobalVar x }; args } when Map.mem operators x ->
         let arity, op = Map.find_exn operators x in
         if List.length args <> arity then
@@ -436,7 +452,7 @@ struct
         @@ F.AST.Record
              ( Option.map ~f:(fst >> pexpr) base,
                List.map
-                 ~f:(fun (f, e) -> (pglobal_ident e.span f, pexpr e))
+                 ~f:(fun (f, e) -> (pfield_ident e.span f, pexpr e))
                  fields )
     | Construct { constructs_record = false; constructor; fields; base }
       when List.for_all ~f:(fst >> is_field_an_index) fields ->

engine/lib/diagnostics.ml

@@ -77,13 +77,7 @@ let to_thir_span (s : Ast.span) : T.span =
       }
 
 let run_hax_pretty_print_diagnostics (s : string) : string =
-  try
-    let stdout, stdin = Unix.open_process "hax-pretty-print-diagnostics" in
-    Out_channel.(
-      output_string stdin s;
-      flush stdin;
-      close stdin);
-    In_channel.input_all stdout
+  try (Utils.Command.run "hax-pretty-print-diagnostics" s).stdout
   with e ->
     "[run_hax_pretty_print_diagnostics] failed. Exn: " ^ Printexc.to_string e
     ^ ". Here is the JSON representation of the error that occurred:\n" ^ s

engine/lib/import_thir.ml

@@ -252,6 +252,22 @@ module Exn = struct
           args = [ { e = Borrow { e = x; _ }; _ }; index ];
         } ->
         Some (x, index)
+    | App
+        {
+          f =
+            {
+              e =
+                GlobalVar
+                  (`Concrete
+                    {
+                      crate = "core";
+                      path = Non_empty_list.[ "ops"; "Index"; "index" ];
+                    });
+              _;
+            };
+          args = [ x; index ];
+        } ->
+        Some (x, index)
     | _ -> None
 
   let rec c_expr (e : Thir.decorated_for__expr_kind) : expr =
@@ -545,7 +561,7 @@ module Exn = struct
             (mk_global ([ lhs_type; index_type ] ->. typ)
             @@ `Concrete
                  {
-                   crate = "std";
+                   crate = "core";
                    path = Non_empty_list.[ "ops"; "Index"; "index" ];
                  })
             [ lhs; index ]
@@ -581,7 +597,7 @@ module Exn = struct
                   {
                     f =
                       {
-                        e = GlobalVar (`Projector (`Concrete _) as field);
+                        e = GlobalVar (`Projector _ as field);
                         typ = TArrow ([ _ ], _);
                         span = _;
                       };

engine/lib/phase_utils.ml

@@ -172,22 +172,22 @@ end = struct
              let filename =
                Printf.sprintf "%02d" nth ^ "_" ^ [%show: DebugPhaseInfo.t] k
              in
-             let rustish = List.map ~f:Print_rust.pitem !l in
+             let rustish = Print_rust.pitems !l in
              let json =
                `Assoc
                  [
                    ("name", `String ([%show: DebugPhaseInfo.t] k));
                    ("nth", `Int nth);
                    ("items", [%yojson_of: Ast.Full.item list] !l);
                    ( "rustish",
-                     [%yojson_of: Print_rust.AnnotatedString.Output.t list]
-                       rustish );
+                     [%yojson_of: Print_rust.AnnotatedString.Output.t] rustish
+                   );
                  ]
              in
              let rustish =
-               List.map ~f:Print_rust.AnnotatedString.Output.raw_string rustish
-               |> String.concat ~sep:"\n\n"
+               Print_rust.AnnotatedString.Output.raw_string rustish
              in
+
              ((filename, rustish), json))
       |> List.unzip
     in

engine/lib/phases/phase_trivialize_assign_lhs.ml

@@ -8,6 +8,7 @@ module%inlined_contents Make (F : Features.T) = struct
   module FB = struct
     include F
     include Features.Off.Nontrivial_lhs
+    include Features.On.Construct_base
   end
 
   include
@@ -21,6 +22,8 @@ module%inlined_contents Make (F : Features.T) = struct
 
     module S = struct
       include Features.SUBTYPE.Id
+
+      let construct_base _ = Features.On.construct_base
     end
 
     module UA = Ast_utils.Make (F)
@@ -60,9 +63,27 @@ module%inlined_contents Make (F : Features.T) = struct
         (LocalIdent.t * B.ty) * B.expr =
       match lhs with
       | LhsLocalVar { var; typ } -> ((var, dty span typ), rhs)
-      | LhsFieldAccessor _ ->
-          Error.unimplemented ~issue_id:86
-            ~details:"Mutation of fields is not implemented yet" span
+      | LhsFieldAccessor { e; typ; field; _ } -> (
+          let lhs = expr_of_lhs e span in
+          let field =
+            match field with
+            | `Projector field -> (field :> global_ident)
+            | _ -> field
+          in
+          match lhs.typ with
+          | TApp { ident; args } ->
+              let rhs' =
+                B.Construct
+                  {
+                    constructor = ident;
+                    constructs_record = true;
+                    fields = [ (field, rhs) ];
+                    base = Some (lhs, Features.On.construct_base);
+                  }
+              in
+              let rhs = { B.e = rhs'; typ = lhs.typ; span } in
+              updater_of_lhs e rhs span
+          | _ -> Error.raise { kind = ArbitraryLHS; span })
       | LhsArrayAccessor { e; typ = _; index; _ } ->
           let lhs = expr_of_lhs e span in
           let rhs =

engine/lib/phases/phase_trivialize_assign_lhs.mli

@@ -9,6 +9,7 @@ module Make (F : Features.T) : sig
     module FB = struct
       include F
       include Features.Off.Nontrivial_lhs
+      include Features.On.Construct_base
     end
 
     module A = Ast.Make (F)

engine/lib/print_rust.ml

@@ -337,26 +337,19 @@ module Raw = struct
 end
 
 let rustfmt (s : string) : string =
-  let stdout, stdin, stderr =
-    Unix.open_process_full "rustfmt" (Unix.environment ())
-  in
-  Out_channel.(
-    output_string stdin s;
-    flush stdin;
-    close stdin);
-  let strout = In_channel.input_all stdout in
-  let strerr = In_channel.input_all stderr |> Caml.String.trim in
-  if String.is_empty strerr then strout
+  let open Utils.Command in
+  let { stderr; stdout } = run "rustfmt" s in
+  if String.is_empty stderr then stdout
   else
     let err =
       [%string
         "\n\n\
          #######################################################\n\
          ########### WARNING: Failed running rustfmt ###########\n\
          #### STDOUT:\n\
-         %{strout}\n\
+         %{stdout}\n\
          #### STDERR:\n\
-         %{strerr}\n\
+         %{stderr}\n\
          #######################################################\n"]
     in
     Caml.prerr_endline err;
@@ -393,6 +386,10 @@ let pitem : item -> AnnotatedString.Output.t =
   (* U.Mappers.regenerate_span_ids#visit_item () *)
   Raw.pitem >> rustfmt_annotated >> AnnotatedString.Output.convert
 
+let pitems : item list -> AnnotatedString.Output.t =
+  List.concat_map ~f:Raw.pitem
+  >> rustfmt_annotated >> AnnotatedString.Output.convert
+
 let pitem_str : item -> string = pitem >> AnnotatedString.Output.raw_string
 
 let pexpr_str (e : expr) : string =

engine/lib/print_rust.mli

@@ -9,5 +9,6 @@ module AnnotatedString : sig
 end
 
 val pitem : item -> AnnotatedString.Output.t
+val pitems : item list -> AnnotatedString.Output.t
 val pitem_str : item -> string
 val pexpr_str : expr -> string

engine/lib/utils.ml

@@ -42,3 +42,23 @@ let split_str (s : string) ~(on : string) : string list =
 
 let tabsize = 2
 let newline_indent depth : string = "\n" ^ String.make (tabsize * depth) ' '
+
+module Command = struct
+  type output = { stderr : string; stdout : string }
+
+  let run (command : string) (stdin_string : string) : output =
+    let stdout, stdin, stderr =
+      Unix.open_process_full command (Unix.environment ())
+    in
+    Unix.set_close_on_exec @@ Unix.descr_of_in_channel stdout;
+    Unix.set_close_on_exec @@ Unix.descr_of_in_channel stderr;
+    Out_channel.(
+      output_string stdin stdin_string;
+      flush stdin;
+      close stdin);
+    let strout = In_channel.input_all stdout in
+    let strerr = In_channel.input_all stderr |> Caml.String.trim in
+    Unix.close @@ Unix.descr_of_in_channel stdout;
+    Unix.close @@ Unix.descr_of_in_channel stderr;
+    { stdout = strout; stderr = strerr }
+end

engine/utils/phase_debug_webapp/script.js

@@ -193,7 +193,7 @@ async function phases_viewer(state = {index: 0, ast_focus: null, seed: SEED}) {
         header.appendChild(container);
     }
     let last_item = null;
-    let codes = current.rustish.map(({string, map}) => {
+    let codes = [current.rustish].map(({string, map}) => {
         let src = string;
         let code = mk('code', [], ['language-rust']);
         code.innerHTML = Prism.highlight(src, Prism.languages.rust, 'rust');
@@ -263,7 +263,7 @@ async function phases_viewer(state = {index: 0, ast_focus: null, seed: SEED}) {
     let app_root = document.querySelector('#app');
     app_root.childNodes.forEach(old => old.remove());
     app_root.appendChild(main);
-    app_root.onkeydown = (e) => {
+    document.body.onkeydown = (e) => {
         let key = ({'ArrowRight': 'n', 'ArrowLeft': 'p'})[e.key] || e.key;
         (({
             'n': () => phases_viewer({...state, index: state.index + 1, ast_focus: null}),

tests/side-effects/Cargo.toml

@@ -7,4 +7,4 @@ edition = "2021"
 
 [package.metadata.hax-tests]
 into.fstar = {snapshot = "none"}
-into.coq = {snapshot = "none"}
+into.coq = {broken = true, snapshot = "none", issue_id = 134}

tests/side-effects/src/lib.rs

@@ -1,8 +1,8 @@
+#![allow(dead_code)]
 fn add3(x: usize, y: usize, z: usize) -> usize {
     x + y + z
 }
 
-#[allow(dead_code)]
 fn local_mutation(mut x: usize) -> usize {
     let mut y = 0;
     if {
@@ -39,7 +39,6 @@ fn local_mutation(mut x: usize) -> usize {
     }
 }
 
-#[allow(dead_code)]
 fn early_returns(mut x: usize) -> usize {
     return (123
         + if {
@@ -59,7 +58,6 @@ fn early_returns(mut x: usize) -> usize {
         + x;
 }
 
-#[allow(dead_code)]
 fn question_mark(mut x: usize) -> Result<usize, usize> {
     if x > 40usize {
         let mut y = 0;
@@ -78,3 +76,22 @@ fn question_mark(mut x: usize) -> Result<usize, usize> {
     };
     Ok(3 + x)
 }
+
+struct Bar {
+    a: bool,
+    b: ([(bool, bool); 6], bool),
+}
+struct Foo {
+    x: bool,
+    y: (bool, Vec<Bar>),
+    z: [Bar; 6],
+    bar: Bar,
+}
+fn assign_non_trivial_lhs(mut foo: Foo) -> Foo {
+    foo.x = true;
+    foo.bar.a = true;
+    foo.bar.b.0[3].1 = true;
+    foo.z[3].a = true;
+    foo.y.1[3].b.0[5].0 = true;
+    foo
+}