From e33eb98ea517791d1c2bbde16aff735cae2faa6c Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Mon, 5 Jun 2023 19:26:50 +0200 Subject: [PATCH 01/14] added array update --- engine/lib/import_thir.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index a680efe29..0ef154f25 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -254,6 +254,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 = @@ -528,7 +544,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 ] From 5efb75f5eeee48e7e8ffb783aeaa827e8bf8b012 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 8 Jun 2023 15:16:24 +0200 Subject: [PATCH 02/14] Fix performance and process limit issue with `--debug-engine` --- engine/lib/diagnostics.ml | 8 +------- engine/lib/phase_utils.ml | 10 +++++----- engine/lib/print_rust.ml | 21 +++++++++------------ engine/lib/print_rust.mli | 1 + engine/lib/utils.ml | 20 ++++++++++++++++++++ engine/utils/phase_debug_webapp/script.js | 2 +- 6 files changed, 37 insertions(+), 25 deletions(-) diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 1940333e4..6785a5bd1 100644 --- a/engine/lib/diagnostics.ml +++ b/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 diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml index e0ec0d675..af8c965c0 100644 --- a/engine/lib/phase_utils.ml +++ b/engine/lib/phase_utils.ml @@ -172,7 +172,7 @@ 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 [ @@ -180,14 +180,14 @@ end = struct ("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 diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index 7cd3598f5..91a182815 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -337,16 +337,9 @@ 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 @@ -354,9 +347,9 @@ let rustfmt (s : string) : string = #######################################################\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 = diff --git a/engine/lib/print_rust.mli b/engine/lib/print_rust.mli index bda7da3c3..f2746458f 100644 --- a/engine/lib/print_rust.mli +++ b/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 diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index aa51c0b2e..e694660a2 100644 --- a/engine/lib/utils.ml +++ b/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 diff --git a/engine/utils/phase_debug_webapp/script.js b/engine/utils/phase_debug_webapp/script.js index eb2dd4fa4..41424f62e 100644 --- a/engine/utils/phase_debug_webapp/script.js +++ b/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'); From 992db21e7a7b52e08f81534fd192adb6df1f6f33 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 8 Jun 2023 15:23:41 +0200 Subject: [PATCH 03/14] add documentation for `--debug-engine` --- engine/DEV.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/engine/DEV.md b/engine/DEV.md index ce3da2ae1..9a5c4ba53 100644 --- a/engine/DEV.md +++ b/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`. From 79095502c207f656c5bbed852eb59ba7eb3bd2d2 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 8 Jun 2023 15:25:48 +0200 Subject: [PATCH 04/14] Fix right left arrows in debug webapp --- engine/utils/phase_debug_webapp/script.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/utils/phase_debug_webapp/script.js b/engine/utils/phase_debug_webapp/script.js index 41424f62e..ebc7c6ac7 100644 --- a/engine/utils/phase_debug_webapp/script.js +++ b/engine/utils/phase_debug_webapp/script.js @@ -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}), From 7f878b096958a68a80eacac774f72dc2257cefda Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 8 Jun 2023 15:17:28 +0200 Subject: [PATCH 05/14] wip --- .../lib/phases/phase_trivialize_assign_lhs.ml | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index a01fe3c53..94aeeb5b7 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/engine/lib/phases/phase_trivialize_assign_lhs.ml @@ -60,12 +60,24 @@ 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 - | LhsArrayAccessor { e; typ = _; index; _ } -> + | LhsFieldAccessor { e; typ; field; _ } -> let lhs = expr_of_lhs e span in - let rhs = + (match lhs.typ with + | TApp {ident; args} -> + let rhs' = + B.Construct { + constructor = ident; + constructs_record = true; + fields = [(field,rhs)]; + base = Some lhs; + } 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 = UB.call "core" "ops" [ "index"; "IndexMut"; "update_at" ] [ lhs; dexpr index; rhs ] From fca1f94dd15a83a952192c889426b35739dc9fa3 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 8 Jun 2023 23:37:57 +0200 Subject: [PATCH 06/14] field update working - needs testing --- engine/backends/fstar/fstar_backend.ml | 18 ++++++++++++++++-- .../lib/phases/phase_trivialize_assign_lhs.ml | 5 +++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 0be7f5acf..36eb8a63f 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -214,6 +214,20 @@ 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 (`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 @@ -388,7 +402,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 +450,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 -> diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index 94aeeb5b7..76142dcc1 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/engine/lib/phases/phase_trivialize_assign_lhs.ml @@ -62,6 +62,11 @@ module%inlined_contents Make (F : Features.T) = struct | LhsLocalVar { var; typ } -> ((var, dty span typ), rhs) | 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' = From 16f802a8b13462d5d38fb01ec4a0c1df77341dbf Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 09:12:35 +0200 Subject: [PATCH 07/14] dune fmt --- engine/backends/fstar/fstar_backend.ml | 8 +++---- .../lib/phases/phase_trivialize_assign_lhs.ml | 23 ++++++++++--------- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 36eb8a63f..1bc166052 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -215,10 +215,11 @@ struct >> pglobal_ident span (* This is a bit too fiddly. TODO: simplify *) - let pfield_concrete_ident (id:concrete_ident) = + 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 = + 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 (`Concrete cid) -> pfield_concrete_ident cid @@ -227,7 +228,6 @@ struct ("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 diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index 76142dcc1..de2d79453 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/engine/lib/phases/phase_trivialize_assign_lhs.ml @@ -60,29 +60,30 @@ 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 { e; typ; field; _ } -> + | 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} -> + match lhs.typ with + | TApp { ident; args } -> let rhs' = - B.Construct { + B.Construct + { constructor = ident; constructs_record = true; - fields = [(field,rhs)]; + fields = [ (field, rhs) ]; base = Some lhs; - } in - let rhs = {B.e = rhs'; typ = lhs.typ; span} in + } + in + let rhs = { B.e = rhs'; typ = lhs.typ; span } in updater_of_lhs e rhs span - | _ -> - Error.raise { kind = ArbitraryLHS; span }) + | _ -> Error.raise { kind = ArbitraryLHS; span }) | LhsArrayAccessor { e; typ = _; index; _ } -> - let lhs = expr_of_lhs e span in - let rhs = + let lhs = expr_of_lhs e span in + let rhs = UB.call "core" "ops" [ "index"; "IndexMut"; "update_at" ] [ lhs; dexpr index; rhs ] From b388edaace9d16c6a967ca2a4b37c4ada4fa0060 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 09:14:32 +0200 Subject: [PATCH 08/14] Fix so that it uses `construct_base` feature --- engine/lib/phases/phase_trivialize_assign_lhs.ml | 5 ++++- engine/lib/phases/phase_trivialize_assign_lhs.mli | 1 + 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index de2d79453..0369b9487 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/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) @@ -75,7 +78,7 @@ module%inlined_contents Make (F : Features.T) = struct constructor = ident; constructs_record = true; fields = [ (field, rhs) ]; - base = Some lhs; + base = Some (lhs, Features.On.construct_base); } in let rhs = { B.e = rhs'; typ = lhs.typ; span } in diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.mli b/engine/lib/phases/phase_trivialize_assign_lhs.mli index 7265bbfb2..3860c3ae6 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.mli +++ b/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) From 06dcb1d123b5f0a5ad034ace45f7c9b7832e41f7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 10:39:28 +0200 Subject: [PATCH 09/14] Print fields for tuples --- engine/backends/fstar/fstar_backend.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 1bc166052..77a057a05 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -222,6 +222,8 @@ struct 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 From 810aa2a8b6780eb88ae693267bc2f49b3c4336e3 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 10:40:16 +0200 Subject: [PATCH 10/14] Translate any LHS projector as a projection, not only concrete fields --- engine/lib/import_thir.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index c323f2189..46e6ff386 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -597,7 +597,7 @@ module Exn = struct { f = { - e = GlobalVar (`Projector (`Concrete _) as field); + e = GlobalVar (`Projector _ as field); typ = TArrow ([ _ ], _); span = _; }; From 136becba4f0f6d3197e887143a4a33bfe5e8bc1e Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 10:40:33 +0200 Subject: [PATCH 11/14] Fix bad refinement on arrays --- engine/backends/fstar/fstar_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 77a057a05..5ce21c47b 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -314,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 From dd5886e1e7d895b3dfaceab017c88d6179035d09 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 10:44:41 +0200 Subject: [PATCH 12/14] Add examples of `assign`s on non trivial LHS --- tests/side-effects/src/lib.rs | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs index 47c084b60..eb60c66ff 100644 --- a/tests/side-effects/src/lib.rs +++ b/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 { if x > 40usize { let mut y = 0; @@ -78,3 +76,22 @@ fn question_mark(mut x: usize) -> Result { }; Ok(3 + x) } + +struct Bar { + a: bool, + b: ([(bool, bool); 6], bool), +} +struct Foo { + x: bool, + y: (bool, Vec), + 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 +} From cc6f6fc9673d3f575024231b838b53e07255c779 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 10:59:49 +0200 Subject: [PATCH 13/14] coq backend: handle more errors --- engine/backends/coq/coq/coq_backend.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 56ba7556c..8907e4293 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/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 } -> From a4967a48c99d8e8624f33094be239ecda5e8d92f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 9 Jun 2023 11:34:47 +0200 Subject: [PATCH 14/14] Coq fails at LHS assignments, update example accordingly See issue #134 --- tests/side-effects/Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/side-effects/Cargo.toml b/tests/side-effects/Cargo.toml index a408d7051..065f2845f 100644 --- a/tests/side-effects/Cargo.toml +++ b/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}