From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Tue, 21 Jun 2022 11:41:09 +0200 Subject: concrete & symbolic evaluation work with new LLBC format --- tests/misc/Constants.fst | 119 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 tests/misc/Constants.fst (limited to 'tests') diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst new file mode 100644 index 00000000..9611c778 --- /dev/null +++ b/tests/misc/Constants.fst @@ -0,0 +1,119 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [constants] *) +module Constants +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [constants::X0] *) +let x0_fwd : result u32 = Return 0 + +(** [core::num::u32::{8}::MAX] *) +assume val core_num_u32_max_fwd : result u32 + +(** [constants::X1] *) +let x1_fwd : result u32 = Return 4294967295 + +(** [constants::X2] *) +let x2_fwd : result u32 = Return 3 + +(** [constants::incr] *) +let incr_fwd (n : u32) : result u32 = + begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end + +(** [constants::X3] *) +let x3_fwd : result u32 = + begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end + +(** [constants::mk_pair0] *) +let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) + +(** [constants::Pair] *) +type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } + +(** [constants::mk_pair1] *) +let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = + Return (Mkpair_t x y) + +(** [constants::P0] *) +let p0_fwd : result (u32 & u32) = + begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end + +(** [constants::P1] *) +let p1_fwd : result (pair_t u32 u32) = + begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end + +(** [constants::P2] *) +let p2_fwd : result (u32 & u32) = Return (0, 1) + +(** [constants::P3] *) +let p3_fwd : result (pair_t u32 u32) = Return (Mkpair_t 0 1) + +(** [constants::Wrap] *) +type wrap_t (t : Type0) = { wrap_val : t; } + +(** [constants::Wrap::{0}::new] *) +let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = + Return (Mkwrap_t val0) + +(** [constants::Y] *) +let y_fwd : result (wrap_t i32) = + begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end + +(** [constants::unwrap_y] *) +let unwrap_y_fwd : result i32 = + begin match y_fwd with | Fail -> Fail | Return w -> Return w.wrap_val end + +(** [constants::YVAL] *) +let yval_fwd : result i32 = + begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end + +(** [constants::get_z1::Z1] *) +let get_z1_z1_fwd : result i32 = Return 3 + +(** [constants::get_z1] *) +let get_z1_fwd : result i32 = + begin match get_z1_z1_fwd with | Fail -> Fail | Return i -> Return i end + +(** [constants::add] *) +let add_fwd (a : i32) (b : i32) : result i32 = + begin match i32_add a b with | Fail -> Fail | Return i -> Return i end + +(** [constants::Q1] *) +let q1_fwd : result i32 = Return 5 + +(** [constants::Q2] *) +let q2_fwd : result i32 = + begin match q1_fwd with | Fail -> Fail | Return i -> Return i end + +(** [constants::Q3] *) +let q3_fwd : result i32 = + begin match q2_fwd with + | Fail -> Fail + | Return i -> + begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end + end + +(** [constants::get_z2] *) +let get_z2_fwd : result i32 = + begin match get_z1_fwd with + | Fail -> Fail + | Return i -> + begin match q3_fwd with + | Fail -> Fail + | Return i0 -> + begin match add_fwd i i0 with + | Fail -> Fail + | Return i1 -> + begin match q1_fwd with + | Fail -> Fail + | Return i2 -> + begin match add_fwd i2 i1 with + | Fail -> Fail + | Return i3 -> Return i3 + end + end + end + end + end + -- cgit v1.3.1 From da118da3e590fbea4e880121837da2ee938837f6 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 23 Jun 2022 15:43:49 +0200 Subject: adapt to new LLBC (without OperandConstantValue) --- src/LlbcOfJson.ml | 30 ++++++++++++------------------ src/main.ml | 30 +++++++++++++++--------------- tests/misc/Constants.fst | 19 +++++++++++++++++++ 3 files changed, 46 insertions(+), 33 deletions(-) (limited to 'tests') diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index a074ed1e..3ff45077 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -381,24 +381,18 @@ let binop_of_json (js : json) : (E.binop, string) result = let constant_value_of_json (js : json) : (V.constant_value, string) result = combine_error_msgs js "constant_value_of_json" (match js with - (* This indirection is because Charon still export the type OperandConstantValue, - * which had other variants than ConstantValue before. - *) - | `Assoc [ ("ConstantValue", `List [ cv ]) ] -> - (match cv with - | `Assoc [ ("Scalar", scalar_value) ] -> - let* scalar_value = scalar_value_of_json scalar_value in - Ok (V.Scalar scalar_value) - | `Assoc [ ("Bool", v) ] -> - let* v = bool_of_json v in - Ok (V.Bool v) - | `Assoc [ ("Char", v) ] -> - let* v = char_of_json v in - Ok (V.Char v) - | `Assoc [ ("String", v) ] -> - let* v = string_of_json v in - Ok (V.String v) - | _ -> Error "") + | `Assoc [ ("Scalar", scalar_value) ] -> + let* scalar_value = scalar_value_of_json scalar_value in + Ok (V.Scalar scalar_value) + | `Assoc [ ("Bool", v) ] -> + let* v = bool_of_json v in + Ok (V.Bool v) + | `Assoc [ ("Char", v) ] -> + let* v = char_of_json v in + Ok (V.Char v) + | `Assoc [ ("String", v) ] -> + let* v = string_of_json v in + Ok (V.String v) | _ -> Error "") let operand_of_json (js : json) : (E.operand, string) result = diff --git a/src/main.ml b/src/main.ml index 93b094fd..6b1083f5 100644 --- a/src/main.ml +++ b/src/main.ml @@ -124,21 +124,21 @@ let () = * command-line arguments *) (* By setting a level for the main_logger_handler, we filter everything *) Easy_logging.Handlers.set_level main_logger_handler EL.Debug; - main_log#set_level EL.Debug; - llbc_of_json_logger#set_level EL.Debug; - pre_passes_log#set_level EL.Debug; - interpreter_log#set_level EL.Debug; - statements_log#set_level EL.Debug; - paths_log#set_level EL.Debug; - expressions_log#set_level EL.Debug; - expansion_log#set_level EL.Debug; - borrows_log#set_level EL.Debug; - invariants_log#set_level EL.Debug; - pure_utils_log#set_level EL.Debug; - symbolic_to_pure_log#set_level EL.Debug; - pure_micro_passes_log#set_level EL.Debug; - pure_to_extract_log#set_level EL.Debug; - translate_log#set_level EL.Debug; + main_log#set_level EL.Info; + llbc_of_json_logger#set_level EL.Info; + pre_passes_log#set_level EL.Info; + interpreter_log#set_level EL.Info; + statements_log#set_level EL.Info; + paths_log#set_level EL.Info; + expressions_log#set_level EL.Info; + expansion_log#set_level EL.Info; + borrows_log#set_level EL.Info; + invariants_log#set_level EL.Info; + pure_utils_log#set_level EL.Info; + symbolic_to_pure_log#set_level EL.Info; + pure_micro_passes_log#set_level EL.Info; + pure_to_extract_log#set_level EL.Info; + translate_log#set_level EL.Info; (* Load the module *) let json = Yojson.Basic.from_file filename in match llbc_module_of_json json with diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index 9611c778..28a9ace7 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -117,3 +117,22 @@ let get_z2_fwd : result i32 = end end +(** [constants::S1] *) +let s1_fwd : result u32 = Return 6 + +(** [constants::S2] *) +let s2_fwd : result u32 = + begin match s1_fwd with + | Fail -> Fail + | Return i -> + begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end + end + +(** [constants::S3] *) +let s3_fwd : result (pair_t u32 u32) = + begin match p3_fwd with | Fail -> Fail | Return p -> Return p end + +(** [constants::S4] *) +let s4_fwd : result (pair_t u32 u32) = + begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end + -- cgit v1.3.1 From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 30 Jun 2022 12:22:14 +0200 Subject: Traduct globals body separately (WIP) --- fstar/Primitives.fst | 3 ++ src/ExtractToFStar.ml | 129 +++++++++++++++++++++++++++++++++++++++++----- src/FunsAnalysis.ml | 77 +++++++++++++++------------ src/Modules.ml | 3 +- src/PrintPure.ml | 10 +++- src/Pure.ml | 3 +- src/PureMicroPasses.ml | 5 +- src/PureToExtract.ml | 18 +++++-- src/PureTypeCheck.ml | 2 +- src/SymbolicToPure.ml | 14 +++-- src/Translate.ml | 7 +-- src/TranslateCore.ml | 6 ++- tests/misc/Constants.fst | 129 +--------------------------------------------- tests/misc/Primitives.fst | 3 ++ 14 files changed, 215 insertions(+), 194 deletions(-) (limited to 'tests') diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index fe351f3a..b3da25c2 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail +// Unwrap a successful result by normalisation (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + (*** Misc *) type char = FStar.Char.char type string = string diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index b89579b5..20b06bfa 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -26,6 +26,14 @@ type type_decl_qualif = *) type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal +let fun_decl_qualif_name (qualif : fun_decl_qualif) : string = + match qualif with + | Let -> "let" + | LetRec -> "let rec" + | And -> "and" + | Val -> "val" + | AssumeVal -> "assume val" + (** Small helper to compute the name of an int type *) let fstar_int_name (int_ty : integer_type) = match int_ty with @@ -305,11 +313,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* Concatenate the elements *) String.concat "_" fname in - let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int) + let fun_name (_fid : A.fun_id) (fname : fun_name) (is_global : bool) (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) : string = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) - let suffix = default_fun_suffix num_rgs rg filter_info in + let suffix = default_fun_suffix is_global num_rgs rg filter_info in (* Concatenate *) fname ^ suffix in @@ -898,12 +906,14 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match qualif.id with | Func fun_id -> extract_function_call ctx fmt inside fun_id qualif.type_args args + | Global global_id -> + let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in + let fun_id = Regular (A.Regular fid, None) in + extract_function_call ctx fmt inside fun_id qualif.type_args args | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> extract_field_projector ctx fmt inside app proj qualif.type_args args - (* TODO | Global global_id -> - extract_global_ref ctx fmt inside global_id*) ) | _ -> (* "Regular" expression *) @@ -1358,14 +1368,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) let is_opaque = Option.is_none def.body in - let qualif = - match qualif with - | Let -> "let" - | LetRec -> "let rec" - | And -> "and" - | Val -> "val" - | AssumeVal -> "assume val" - in + let qualif = fun_decl_qualif_name qualif in F.pp_print_string fmt (qualif ^ " " ^ def_name); F.pp_print_space fmt (); (* Open a box for "(PARAMS) : EFFECT =" *) @@ -1474,6 +1477,108 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 +(* Change the suffix from "_c" to "_body" *) +let global_decl_to_body_name (decl : string) : string = + (* The declaration length without the global suffix *) + let base_len = String.length decl - 2 in + (* TODO: Use String.ends_with instead when a more recent version of OCaml is used *) + assert (String.sub decl base_len 2 = "_c"); + (String.sub decl 0 base_len) ^ "_body" + +(** Print a definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) +let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) + (qualif : fun_decl_qualif) (name : string) (ty : ty) + (extract_body : (F.formatter -> unit) Option.t) + : unit = + let is_opaque = Option.is_none extract_body in + + (* Open the definition box (depth=0) *) + F.pp_open_hvbox fmt ctx.indent_incr; + + (* Open "QUALIF NAME : TYPE =" box (depth=1) *) + F.pp_open_hovbox fmt ctx.indent_incr; + (* Print "QUALIF NAME " *) + F.pp_print_string fmt (fun_decl_qualif_name qualif ^ " " ^ name); + F.pp_print_space fmt (); + + (* Open ": TYPE =" box (depth=2) *) + F.pp_open_hvbox fmt 0; + (* Print ": " *) + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + + (* Open "TYPE" box (depth=3) *) + F.pp_open_hovbox fmt ctx.indent_incr; + (* Print "TYPE" *) + extract_ty ctx fmt false ty; + (* Close "TYPE" box (depth=3) *) + F.pp_close_box fmt (); + + if not is_opaque then ( + (* Print " =" *) + F.pp_print_space fmt (); + F.pp_print_string fmt "="; + ); + (* Close ": TYPE =" box (depth=2) *) + F.pp_close_box fmt (); + (* Close "QUALIF NAME : TYPE =" box (depth=1) *) + F.pp_close_box fmt (); + + if not is_opaque then ( + F.pp_print_space fmt (); + (* Open "BODY" box (depth=1) *) + F.pp_open_hvbox fmt 0; + (* Print "BODY" *) + (Option.get extract_body) fmt; + (* Close "BODY" box (depth=1) *) + F.pp_close_box fmt () + ); + (* Close the definition box (depth=0) *) + F.pp_close_box fmt () + +(** Extract a global declaration. + This has similarity with the function extraction above (without parameters). + However, generate its body separately from its declaration to extract the result value. + + For example, + `let x = 3` + + will be translated to + `let x_body : result int = Return 3` + `let x_c : int = eval_global x_body` + *) +let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) + (qualif : fun_decl_qualif) (def : fun_decl) + : unit = + (* Sanity checks for globals *) + assert (def.is_global); + assert (Option.is_none def.back_id); + assert (List.length def.signature.inputs = 0); + assert (List.length def.signature.doutputs = 1); + assert (List.length def.signature.type_params = 0); + assert (not def.signature.info.effect_info.can_fail); + + (* Add a break then the corresponding Rust definition *) + F.pp_print_break fmt 0 0; + F.pp_print_string fmt ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)"); + F.pp_print_space fmt (); + + let def_name = ctx_get_local_function def.def_id def.back_id ctx in + match def.body with + | None -> + extract_global_definition ctx fmt qualif def_name def.signature.output None + | Some body -> + let body_name = global_decl_to_body_name def_name in + let body_ty = mk_result_ty def.signature.output in + extract_global_definition ctx fmt qualif body_name body_ty (Some (fun fmt -> + extract_texpression ctx fmt false body.body + )); + F.pp_print_break fmt 0 0; + extract_global_definition ctx fmt qualif def_name def.signature.output (Some (fun fmt -> + F.pp_print_string fmt ("eval_global " ^ body_name) + )); + F.pp_print_break fmt 0 0 + (** Extract a unit test, if the function is a unit function (takes no parameters, returns unit). diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index dc205eb9..ca20352f 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -1,6 +1,6 @@ (** Compute various information, including: - can a function fail (by having `Fail` in its body, or transitively - calling a function which can fail) + calling a function which can fail), false for globals - can a function diverge (bu being recursive, containing a loop or transitively calling a function which can diverge) - does a function perform stateful operations (i.e., do we need a state @@ -49,47 +49,56 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) let stateful = ref false in let divergent = ref false in - let obj = - object - inherit [_] iter_statement as super - - method! visit_Assert env a = - can_fail := true; - super#visit_Assert env a - - method! visit_Call env call = - (match call.func with - | Regular id -> - if FunDeclId.Set.mem id fun_ids then divergent := true - else - let info = FunDeclId.Map.find id !infos in - can_fail := !can_fail || info.can_fail; - stateful := !stateful || info.stateful; - divergent := !divergent || info.divergent - | Assumed id -> - (* None of the assumed functions is stateful for now *) - can_fail := !can_fail || Assumed.assumed_can_fail id); - super#visit_Call env call - - method! visit_Panic env = - can_fail := true; - super#visit_Panic env - - method! visit_Loop env loop = - divergent := true; - super#visit_Loop env loop - end - in - let visit_fun (f : fun_decl) : unit = + print_endline ("@ fun: " ^ Print.fun_name_to_string f.name); + let obj = + object (self) + inherit [_] iter_statement as super + + method may_fail b = + if f.is_global then () else + can_fail := !can_fail || b + + method! visit_Assert env a = + self#may_fail true; + super#visit_Assert env a + + method! visit_Call env call = + print_string "@ dep: "; + pp_fun_id Format.std_formatter call.func; + print_newline (); + + (match call.func with + | Regular id -> + if FunDeclId.Set.mem id fun_ids then divergent := true + else + let info = FunDeclId.Map.find id !infos in + self#may_fail info.can_fail; + stateful := !stateful || info.stateful; + divergent := !divergent || info.divergent + | Assumed id -> + (* None of the assumed functions is stateful for now *) + can_fail := !can_fail || Assumed.assumed_can_fail id); + super#visit_Call env call + + method! visit_Panic env = + self#may_fail true; + super#visit_Panic env + + method! visit_Loop env loop = + divergent := true; + super#visit_Loop env loop + end + in match f.body with | None -> (* Opaque function *) - can_fail := true; + obj#may_fail true; stateful := use_state | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; + print_endline ("@ can_fail: " ^ Bool.to_string !can_fail); { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } in diff --git a/src/Modules.ml b/src/Modules.ml index b0e8878d..149de020 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -7,7 +7,8 @@ type 'id g_declaration_group = NonRec of 'id | Rec of 'id list type type_declaration_group = TypeDeclId.id g_declaration_group [@@deriving show] -type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] +type fun_declaration_group = FunDeclId.id g_declaration_group +[@@deriving show] (** Module declaration *) type declaration_group = diff --git a/src/PrintPure.ml b/src/PrintPure.ml index ea9bf2ab..c13f967f 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -44,6 +44,7 @@ type ast_formatter = { TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option; adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option; fun_decl_id_to_string : A.FunDeclId.id -> string; + global_decl_id_to_string : A.GlobalDeclId.id -> string; } let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = @@ -85,7 +86,9 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) while we only need those definitions to lookup proper names for the def ids. *) let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) - (fun_decls : A.fun_decl A.FunDeclId.Map.t) (type_params : type_var list) : + (fun_decls : A.fun_decl A.FunDeclId.Map.t) + (gid_conv : A.global_id_converter) + (type_params : type_var list) : ast_formatter = let type_var_id_to_string vid = let var = T.TypeVarId.nth type_params vid in @@ -112,6 +115,9 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) let def = A.FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in + let global_decl_id_to_string def_id = + fun_decl_id_to_string (A.global_to_fun_id gid_conv def_id) + in { type_var_id_to_string; type_decl_id_to_string; @@ -120,6 +126,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) adt_field_names; adt_field_to_string; fun_decl_id_to_string; + global_decl_id_to_string; } let type_id_to_string (fmt : type_formatter) (id : type_id) : string = @@ -480,6 +487,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) let qualif_s = match qualif.id with | Func fun_id -> fun_id_to_string fmt fun_id + | Global global_id -> fmt.global_decl_id_to_string global_id | AdtCons adt_cons_id -> let variant_s = adt_variant_to_string diff --git a/src/Pure.ml b/src/Pure.ml index 42f56fed..b3be2040 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -302,9 +302,9 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] type qualif_id = | Func of fun_id + | Global of A.GlobalDeclId.id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) - (* TODO | Global of GlobalDeclId.id*) [@@deriving show] type qualif = { id : qualif_id; type_args : ty list } [@@deriving show] @@ -575,5 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; + is_global : bool; body : fun_body option; } diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 826283ae..7927a068 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -611,7 +611,10 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool) | Func (Unop _ | Binop _) -> true (* primitive function call *) | Func (Regular _) -> - false (* non-primitive function call *)) + false (* non-primitive function call *) + | Global _ -> + true (* Global constant or static *) + ) | _ -> filter else false in diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 195eb879..e58fec2a 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -74,6 +74,7 @@ type formatter = { fun_name : A.fun_id -> fun_name -> + bool -> int -> region_group_info option -> bool * int -> @@ -440,11 +441,13 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found -let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) +let ctx_get_function (id : A.fun_id) + (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get (FunId (id, rg)) ctx -let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option) +let ctx_get_local_function (id : A.FunDeclId.id) + (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = ctx_get_function (A.Regular id) rg ctx @@ -596,7 +599,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename def.is_global num_rgs rg_info (keep_fwd, num_backs) in (* Add the function name *) let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in @@ -666,8 +669,12 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = information. TODO: move all those helpers. *) -let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) - ((keep_fwd, num_backs) : bool * int) : string = +let default_fun_suffix + (is_global : bool) + (num_region_groups : int) + (rg : region_group_info option) + ((keep_fwd, num_backs) : bool * int) + : string = (* There are several cases: - [rg] is `Some`: this is a forward function: - we add "_fwd" @@ -683,6 +690,7 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option) we could not add the "_fwd" suffix) to prevent name clashes between definitions (in particular between type and function definitions). *) + if is_global then "_c" else match rg with | None -> "_fwd" | Some rg -> diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml index 8848ff20..90b9ab09 100644 --- a/src/PureTypeCheck.ml +++ b/src/PureTypeCheck.ml @@ -111,7 +111,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = check_texpression ctx body | Qualif qualif -> ( match qualif.id with - | Func _ -> () (* TODO *) + | Func _ | Global _ -> () (* TODO *) | Proj { adt_id = proj_adt_id; field_id } -> (* Note we can only project fields of structures (not enumerations) *) (* Deconstruct the projector type *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 927684bc..84536005 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -144,7 +144,8 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = let type_params = ctx.fun_decl.signature.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - PrintPure.mk_ast_formatter type_decls fun_decls type_params + let gid_conv = ctx.fun_context.gid_conv in + PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in @@ -165,14 +166,16 @@ let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.llbc_type_decls in let fun_decls = ctx.fun_context.llbc_fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_decl_to_string fmt def (* TODO: move *) @@ -482,7 +485,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) let info = A.FunDeclId.Map.find fid fun_infos in let input_state = info.stateful in let output_state = input_state && gid = None in - { can_fail = true; input_state; output_state } + { can_fail = info.can_fail; input_state; output_state } | A.Assumed aid -> { can_fail = Assumed.assumed_can_fail aid; @@ -1663,6 +1666,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) (* Lookup the signature *) let signature = bs_ctx_lookup_local_function_sig def_id bid ctx in (* Translate the body, if there is *) + let is_global = def.A.is_global in let body = match body with | None -> None @@ -1723,7 +1727,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) Some { inputs; inputs_lvs; body } in (* Assemble the declaration *) - let def = { def_id; back_id = bid; basename; signature; body } in + let def = { def_id; back_id = bid; basename; signature; is_global; body } in (* Debugging *) log#ldebug (lazy diff --git a/src/Translate.ml b/src/Translate.ml index d4d79355..9412b8b8 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -495,9 +495,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then - ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause def) + then if def.is_global + then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def + else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def + ) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index ccaa9e22..047219ad 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -40,14 +40,16 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = let type_params = sg.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_sig_to_string fmt sg let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let type_params = def.signature.type_params in let type_decls = ctx.type_context.type_decls in let fun_decls = ctx.fun_context.fun_decls in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in + let gid_conv = ctx.fun_context.gid_conv in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index 28a9ace7..8419ba43 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -5,134 +5,7 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [constants::X0] *) -let x0_fwd : result u32 = Return 0 - -(** [core::num::u32::{8}::MAX] *) -assume val core_num_u32_max_fwd : result u32 - -(** [constants::X1] *) -let x1_fwd : result u32 = Return 4294967295 - -(** [constants::X2] *) -let x2_fwd : result u32 = Return 3 - (** [constants::incr] *) -let incr_fwd (n : u32) : result u32 = +let incr_fwd (n : u32) : u32 = begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end -(** [constants::X3] *) -let x3_fwd : result u32 = - begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end - -(** [constants::mk_pair0] *) -let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) - -(** [constants::Pair] *) -type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } - -(** [constants::mk_pair1] *) -let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = - Return (Mkpair_t x y) - -(** [constants::P0] *) -let p0_fwd : result (u32 & u32) = - begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end - -(** [constants::P1] *) -let p1_fwd : result (pair_t u32 u32) = - begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end - -(** [constants::P2] *) -let p2_fwd : result (u32 & u32) = Return (0, 1) - -(** [constants::P3] *) -let p3_fwd : result (pair_t u32 u32) = Return (Mkpair_t 0 1) - -(** [constants::Wrap] *) -type wrap_t (t : Type0) = { wrap_val : t; } - -(** [constants::Wrap::{0}::new] *) -let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = - Return (Mkwrap_t val0) - -(** [constants::Y] *) -let y_fwd : result (wrap_t i32) = - begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end - -(** [constants::unwrap_y] *) -let unwrap_y_fwd : result i32 = - begin match y_fwd with | Fail -> Fail | Return w -> Return w.wrap_val end - -(** [constants::YVAL] *) -let yval_fwd : result i32 = - begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end - -(** [constants::get_z1::Z1] *) -let get_z1_z1_fwd : result i32 = Return 3 - -(** [constants::get_z1] *) -let get_z1_fwd : result i32 = - begin match get_z1_z1_fwd with | Fail -> Fail | Return i -> Return i end - -(** [constants::add] *) -let add_fwd (a : i32) (b : i32) : result i32 = - begin match i32_add a b with | Fail -> Fail | Return i -> Return i end - -(** [constants::Q1] *) -let q1_fwd : result i32 = Return 5 - -(** [constants::Q2] *) -let q2_fwd : result i32 = - begin match q1_fwd with | Fail -> Fail | Return i -> Return i end - -(** [constants::Q3] *) -let q3_fwd : result i32 = - begin match q2_fwd with - | Fail -> Fail - | Return i -> - begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end - end - -(** [constants::get_z2] *) -let get_z2_fwd : result i32 = - begin match get_z1_fwd with - | Fail -> Fail - | Return i -> - begin match q3_fwd with - | Fail -> Fail - | Return i0 -> - begin match add_fwd i i0 with - | Fail -> Fail - | Return i1 -> - begin match q1_fwd with - | Fail -> Fail - | Return i2 -> - begin match add_fwd i2 i1 with - | Fail -> Fail - | Return i3 -> Return i3 - end - end - end - end - end - -(** [constants::S1] *) -let s1_fwd : result u32 = Return 6 - -(** [constants::S2] *) -let s2_fwd : result u32 = - begin match s1_fwd with - | Fail -> Fail - | Return i -> - begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end - end - -(** [constants::S3] *) -let s3_fwd : result (pair_t u32 u32) = - begin match p3_fwd with | Fail -> Fail | Return p -> Return p end - -(** [constants::S4] *) -let s4_fwd : result (pair_t u32 u32) = - begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end - diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst index fe351f3a..b3da25c2 100644 --- a/tests/misc/Primitives.fst +++ b/tests/misc/Primitives.fst @@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail +// Unwrap a successful result by normalisation (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + (*** Misc *) type char = FStar.Char.char type string = string -- cgit v1.3.1 From eebedf86db68c240fe16cfd74af2cc462b0d9cf9 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Tue, 5 Jul 2022 12:16:36 +0200 Subject: Remove last prints, adapt JSON --- src/FunsAnalysis.ml | 3 - src/LlbcOfJson.ml | 6 +- tests/betree/BetreeMain.Clauses.Template.fst | 24 +- tests/betree/BetreeMain.Funs.fst | 359 ++++++++++++++------------- tests/betree/BetreeMain.Types.fsti | 12 +- tests/betree/Primitives.fst | 3 + 6 files changed, 206 insertions(+), 201 deletions(-) (limited to 'tests') diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index ee4f71c1..5a623450 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -74,9 +74,6 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) can_fail := EU.binop_can_fail bop || !can_fail method! visit_Call env call = - pp_fun_id Format.std_formatter call.func; - print_newline (); - (match call.func with | Regular id -> if FunDeclId.Set.mem id fun_ids then divergent := true diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 3ff45077..c157b667 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -644,13 +644,13 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ [ ("def_id", def_id); ("name", name); - ("type_", type_); + ("ty", ty); ("body", body); ] -> let* global_id = A.GlobalDeclId.id_of_json def_id in let def_id = A.global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name in - let* type_ = ety_of_json type_ in + let* ty = ety_of_json ty in let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in let signature : A.fun_sig = { region_params = []; @@ -658,7 +658,7 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ regions_hierarchy = []; type_params = []; inputs = []; - output = TU.ety_no_regions_to_sty type_; + output = TU.ety_no_regions_to_sty ty; } in Ok { A.def_id; name; signature; body; is_global = true; } | _ -> Error "") diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst index eb26276c..5a9776ab 100644 --- a/tests/betree/BetreeMain.Clauses.Template.fst +++ b/tests/betree/BetreeMain.Clauses.Template.fst @@ -42,18 +42,18 @@ let betree_node_apply_upserts_decreases (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) -unfold -let betree_internal_lookup_in_children_decreases (self : betree_internal_t) - (key : u64) (st : state) : nat = - admit () - (** [betree_main::betree::Node::{5}::lookup]: decreases clause *) unfold let betree_node_lookup_decreases (self : betree_node_t) (key : u64) (st : state) : nat = admit () +(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) +unfold +let betree_internal_lookup_in_children_decreases (self : betree_internal_t) + (key : u64) (st : state) : nat = + admit () + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) unfold let betree_node_lookup_mut_in_bindings_decreases (key : u64) @@ -86,17 +86,17 @@ let betree_node_apply_messages_to_internal_decreases (new_msgs : betree_list_t (u64 & betree_message_t)) : nat = admit () -(** [betree_main::betree::Internal::{4}::flush]: decreases clause *) +(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) unfold -let betree_internal_flush_decreases (self : betree_internal_t) +let betree_node_apply_messages_decreases (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat = + (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = admit () -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) +(** [betree_main::betree::Internal::{4}::flush]: decreases clause *) unfold -let betree_node_apply_messages_decreases (self : betree_node_t) +let betree_internal_flush_decreases (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat = + (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat = admit () diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index 9b960ce5..4761b6a3 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -80,6 +80,10 @@ let betree_node_id_counter_fresh_id_back | Return i -> Return (Mkbetree_node_id_counter_t i) end +(** [core::num::u64::{9}::MAX] *) +let core_num_u64_max_body : result u64 = Return 18446744073709551615 +let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body + (** [betree_main::betree::upsert_update] *) let betree_upsert_update_fwd (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 = @@ -92,16 +96,17 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - begin match u64_sub 18446744073709551615 prev0 with + let i = core_num_u64_max_c in + begin match u64_sub i prev0 with | Fail -> Fail | Return margin -> if margin >= v then begin match u64_add prev0 v with | Fail -> Fail - | Return i -> Return i + | Return i0 -> Return i0 end - else Return 18446744073709551615 + else let i0 = core_num_u64_max_c in Return i0 end | BetreeUpsertFunStateSub v -> if prev0 >= v @@ -468,48 +473,8 @@ let rec betree_node_apply_upserts_back end end -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -let rec betree_internal_lookup_in_children_fwd - (self : betree_internal_t) (key : u64) (st : state) : - Tot (result (state & (option u64))) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - then - begin match betree_node_lookup_fwd self.betree_internal_left key st with - | Fail -> Fail - | Return (st0, opt) -> Return (st0, opt) - end - else - begin match betree_node_lookup_fwd self.betree_internal_right key st with - | Fail -> Fail - | Return (st0, opt) -> Return (st0, opt) - end - -(** [betree_main::betree::Internal::{4}::lookup_in_children] *) -and betree_internal_lookup_in_children_back - (self : betree_internal_t) (key : u64) (st : state) : - Tot (result betree_internal_t) - (decreases (betree_internal_lookup_in_children_decreases self key st)) - = - if key < self.betree_internal_pivot - then - begin match betree_node_lookup_back self.betree_internal_left key st with - | Fail -> Fail - | Return n -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right) - end - else - begin match betree_node_lookup_back self.betree_internal_right key st with - | Fail -> Fail - | Return n -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n) - end - (** [betree_main::betree::Node::{5}::lookup] *) -and betree_node_lookup_fwd +let rec betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : Tot (result (state & (option u64))) (decreases (betree_node_lookup_decreases self key st)) @@ -723,6 +688,46 @@ and betree_node_lookup_back end end +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +and betree_internal_lookup_in_children_fwd + (self : betree_internal_t) (key : u64) (st : state) : + Tot (result (state & (option u64))) + (decreases (betree_internal_lookup_in_children_decreases self key st)) + = + if key < self.betree_internal_pivot + then + begin match betree_node_lookup_fwd self.betree_internal_left key st with + | Fail -> Fail + | Return (st0, opt) -> Return (st0, opt) + end + else + begin match betree_node_lookup_fwd self.betree_internal_right key st with + | Fail -> Fail + | Return (st0, opt) -> Return (st0, opt) + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +and betree_internal_lookup_in_children_back + (self : betree_internal_t) (key : u64) (st : state) : + Tot (result betree_internal_t) + (decreases (betree_internal_lookup_in_children_decreases self key st)) + = + if key < self.betree_internal_pivot + then + begin match betree_node_lookup_back self.betree_internal_left key st with + | Fail -> Fail + | Return n -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right) + end + else + begin match betree_node_lookup_back self.betree_internal_right key st with + | Fail -> Fail + | Return n -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n) + end + (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) let rec betree_node_lookup_mut_in_bindings_fwd (key : u64) (bindings : betree_list_t (u64 & u64)) : @@ -1128,140 +1133,8 @@ let rec betree_node_apply_messages_to_internal_fwd_back | BetreeListNil -> Return msgs end -(** [betree_main::betree::Internal::{4}::flush] *) -let rec betree_internal_flush_fwd - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : - Tot (result (state & (betree_list_t (u64 & betree_message_t)))) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) - = - begin match - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | Fail -> Fail - | Return p -> - let (msgs_left, msgs_right) = p in - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail - | Return len_left -> - if len_left >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (_, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | Fail -> Fail - | Return len_right -> - if len_right >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (st1, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (_, _) -> Return (st1, BetreeListNil) - end - end - else Return (st0, msgs_right) - end - end - end - else - begin match - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (_, _) -> Return (st0, msgs_left) - end - end - end - end - -(** [betree_main::betree::Internal::{4}::flush] *) -and betree_internal_flush_back - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (u64 & betree_message_t)) (st : state) : - Tot (result (betree_internal_t & betree_node_id_counter_t)) - (decreases (betree_internal_flush_decreases self params node_id_cnt content - st)) - = - begin match - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot with - | Fail -> Fail - | Return p -> - let (msgs_left, msgs_right) = p in - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with - | Fail -> Fail - | Return len_left -> - if len_left >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (st0, _) -> - begin match - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st with - | Fail -> Fail - | Return (n, node_id_cnt0) -> - begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right - with - | Fail -> Fail - | Return len_right -> - if len_right >= params.betree_params_min_flush_size - then - begin match - betree_node_apply_messages_back self.betree_internal_right - params node_id_cnt0 msgs_right st0 with - | Fail -> Fail - | Return (n0, node_id_cnt1) -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n n0, node_id_cnt1) - end - else - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot n self.betree_internal_right, - node_id_cnt0) - end - end - end - else - begin match - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st with - | Fail -> Fail - | Return (n, node_id_cnt0) -> - Return (Mkbetree_internal_t self.betree_internal_id - self.betree_internal_pivot self.betree_internal_left n, - node_id_cnt0) - end - end - end - (** [betree_main::betree::Node::{5}::apply_messages] *) -and betree_node_apply_messages_fwd +let rec betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : @@ -1450,6 +1323,138 @@ and betree_node_apply_messages_back end end +(** [betree_main::betree::Internal::{4}::flush] *) +and betree_internal_flush_fwd + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (u64 & betree_message_t)) (st : state) : + Tot (result (state & (betree_list_t (u64 & betree_message_t)))) + (decreases (betree_internal_flush_decreases self params node_id_cnt content + st)) + = + begin match + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot with + | Fail -> Fail + | Return p -> + let (msgs_left, msgs_right) = p in + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with + | Fail -> Fail + | Return len_left -> + if len_left >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (_, node_id_cnt0) -> + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right + with + | Fail -> Fail + | Return len_right -> + if len_right >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (st1, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (_, _) -> Return (st1, BetreeListNil) + end + end + else Return (st0, msgs_right) + end + end + end + else + begin match + betree_node_apply_messages_fwd self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (_, _) -> Return (st0, msgs_left) + end + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +and betree_internal_flush_back + (self : betree_internal_t) (params : betree_params_t) + (node_id_cnt : betree_node_id_counter_t) + (content : betree_list_t (u64 & betree_message_t)) (st : state) : + Tot (result (betree_internal_t & betree_node_id_counter_t)) + (decreases (betree_internal_flush_decreases self params node_id_cnt content + st)) + = + begin match + betree_list_partition_at_pivot_fwd betree_message_t content + self.betree_internal_pivot with + | Fail -> Fail + | Return p -> + let (msgs_left, msgs_right) = p in + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with + | Fail -> Fail + | Return len_left -> + if len_left >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_fwd self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (st0, _) -> + begin match + betree_node_apply_messages_back self.betree_internal_left params + node_id_cnt msgs_left st with + | Fail -> Fail + | Return (n, node_id_cnt0) -> + begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right + with + | Fail -> Fail + | Return len_right -> + if len_right >= params.betree_params_min_flush_size + then + begin match + betree_node_apply_messages_back self.betree_internal_right + params node_id_cnt0 msgs_right st0 with + | Fail -> Fail + | Return (n0, node_id_cnt1) -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n n0, node_id_cnt1) + end + else + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot n self.betree_internal_right, + node_id_cnt0) + end + end + end + else + begin match + betree_node_apply_messages_back self.betree_internal_right params + node_id_cnt msgs_right st with + | Fail -> Fail + | Return (n, node_id_cnt0) -> + Return (Mkbetree_internal_t self.betree_internal_id + self.betree_internal_pivot self.betree_internal_left n, + node_id_cnt0) + end + end + end + (** [betree_main::betree::Node::{5}::apply] *) let betree_node_apply_fwd (self : betree_node_t) (params : betree_params_t) diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti index a937c726..aad9cb43 100644 --- a/tests/betree/BetreeMain.Types.fsti +++ b/tests/betree/BetreeMain.Types.fsti @@ -24,8 +24,13 @@ type betree_message_t = (** [betree_main::betree::Leaf] *) type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; } +(** [betree_main::betree::Node] *) +type betree_node_t = +| BetreeNodeInternal : betree_internal_t -> betree_node_t +| BetreeNodeLeaf : betree_leaf_t -> betree_node_t + (** [betree_main::betree::Internal] *) -type betree_internal_t = +and betree_internal_t = { betree_internal_id : u64; betree_internal_pivot : u64; @@ -33,11 +38,6 @@ type betree_internal_t = betree_internal_right : betree_node_t; } -(** [betree_main::betree::Node] *) -and betree_node_t = -| BetreeNodeInternal : betree_internal_t -> betree_node_t -| BetreeNodeLeaf : betree_leaf_t -> betree_node_t - (** [betree_main::betree::Params] *) type betree_params_t = { diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index fe351f3a..b3da25c2 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/Primitives.fst @@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail +// Unwrap a successful result by normalisation (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + (*** Misc *) type char = FStar.Char.char type string = string -- cgit v1.3.1 From f9015d1e956ace6c875eb6a631caeac49cfb8148 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Fri, 29 Jul 2022 16:04:49 +0200 Subject: Create global declaration group, address PR changes but introduce bugs --- src/ExtractToFStar.ml | 64 ++++++++++---------- src/FunsAnalysis.ml | 13 ++++- src/Interpreter.ml | 4 +- src/InterpreterStatements.ml | 7 ++- src/LlbcOfJson.ml | 37 ++++++------ src/Modules.ml | 27 +++++---- src/PureToExtract.ml | 32 +++++++--- src/PureTypeCheck.ml | 7 +-- src/PureUtils.ml | 5 ++ src/Translate.ml | 21 +++++-- tests/misc/Constants.fst | 135 ------------------------------------------- 11 files changed, 134 insertions(+), 218 deletions(-) (limited to 'tests') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2c53e45b..a2b15ece 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -313,11 +313,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* Concatenate the elements *) String.concat "_" fname in - let fun_name (_fid : A.fun_id) (fname : fun_name) (is_global : bool) (num_rgs : int) + let global_name (name : global_name) : string = + let parts = List.map to_snake_case (get_name name) in + String.concat "_" parts + in + let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) : string = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) - let suffix = default_fun_suffix is_global num_rgs rg filter_info in + let suffix = default_fun_suffix num_rgs rg filter_info in (* Concatenate *) fname ^ suffix in @@ -411,6 +415,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) variant_name; struct_constructor; type_name; + global_name; fun_name; decreases_clause_name; var_basename; @@ -839,6 +844,11 @@ let extract_adt_g_value ctx | _ -> raise (Failure "Inconsistent typed value") +(* Extract globals in the same way as variables *) +let extract_global (ctx : extraction_ctx) (fmt : F.formatter) + (id : A.GlobalDeclId.id) : unit = + F.pp_print_string fmt (ctx_get_global_decl id ctx) + (** [inside]: see [extract_ty]. As an pattern can introduce new variables, we return an extraction context @@ -907,12 +917,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Func fun_id -> extract_function_call ctx fmt inside fun_id qualif.type_args args | Global global_id -> - failwith "TODO ExtractToFStar.ml:911" - (* Previous code: - let fid = A.global_to_fun_id ctx.trans_ctx.fun_context.gid_conv global_id in - let fun_id = Regular (A.Regular fid, None) in - extract_function_call ctx fmt inside fun_id qualif.type_args args - *) + extract_global ctx fmt global_id | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> @@ -1353,6 +1358,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) : unit = + assert (def.is_global_body); (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1551,40 +1557,40 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) `let x_c : int = eval_global x_body` *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (qualif : fun_decl_qualif) (def : fun_decl) - : unit = - (* TODO Lookup LLBC decl *) - (* Sanity checks for globals *) - assert (def.is_global_body); - failwith "TODO ExtractToFStar.ml:1559" - (* Previous code: - assert (Option.is_none def.back_id); - assert (List.length def.signature.inputs = 0); - assert (List.length def.signature.doutputs = 1); - assert (List.length def.signature.type_params = 0); - assert (not def.signature.info.effect_info.can_fail); + (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = + assert (body.is_global_body); + assert (Option.is_none body.back_id); + assert (List.length body.signature.inputs = 0); + assert (List.length body.signature.doutputs = 1); + assert (List.length body.signature.type_params = 0); (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - F.pp_print_string fmt ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)"); + F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); F.pp_print_space fmt (); - let def_name = ctx_get_local_function def.def_id def.back_id ctx in - match def.body with + let decl_name = ctx_get_global_decl global.def_id ctx in + let body_name = ctx_get_global_body global.def_id ctx in + + let decl_ty, body_ty = + let ty = body.signature.output in + if body.signature.info.effect_info.can_fail + then (unwrap_result_ty ty, ty) + else (ty, mk_result_ty ty) + in + match body.body with | None -> - extract_global_definition ctx fmt qualif def_name def.signature.output None + let qualif = if interface then Val else AssumeVal in + extract_global_definition ctx fmt qualif decl_name decl_ty None | Some body -> - let body_name = global_decl_to_body_name def_name in - let body_ty = mk_result_ty def.signature.output in - extract_global_definition ctx fmt qualif body_name body_ty (Some (fun fmt -> + extract_global_definition ctx fmt Let body_name body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body )); F.pp_print_break fmt 0 0; - extract_global_definition ctx fmt qualif def_name def.signature.output (Some (fun fmt -> + extract_global_definition ctx fmt Let decl_name decl_ty (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name) )); F.pp_print_break fmt 0 0 - *) (** Extract a unit test, if the function is a unit function (takes no parameters, returns unit). diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index 3a6ad542..65a130c8 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -1,7 +1,7 @@ (** Compute various information, including: - can a function fail (by having `Fail` in its body, or transitively calling a function which can fail), false for globals - - can a function diverge (bu being recursive, containing a loop or + - can a function diverge (by being recursive, containing a loop or transitively calling a function which can diverge) - does a function perform stateful operations (i.e., do we need a state to translate it) @@ -26,7 +26,9 @@ type fun_info = { type modules_funs_info = fun_info FunDeclId.Map.t (** Various information about a module's functions *) -let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) +let analyze_module (m : llbc_module) + (funs_map : fun_decl FunDeclId.Map.t) + (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : modules_funs_info = let infos = ref FunDeclId.Map.empty in @@ -104,7 +106,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) * syntactically can't fail don't use an error monad. *) in List.iter visit_fun d; - (* Not-failing functions are not handled yet. *) + (* Non-failing functions are not handled yet. *) can_fail := true; { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } in @@ -126,6 +128,11 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) | Fun decl :: decls' -> analyze_fun_decl_group decl; analyze_decl_groups decls' + | Global id :: decls' -> + (* Analyze a global by analyzing its body function *) + let global = GlobalDeclId.Map.find id globals_map in + analyze_fun_decl_group (NonRec global.body_id); + analyze_decl_groups decls' in analyze_decl_groups m.declarations; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3610d486..51144ba2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -15,9 +15,9 @@ let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : C.type_context * C.fun_context * C.global_context = - let type_decls_list, _ = M.split_declarations m.declarations in + let type_decls_list, _, _ = M.split_declarations m.declarations in let type_decls, fun_decls, global_decls = M.compute_defs_maps m in - let type_decls_groups, _funs_defs_groups = + let type_decls_groups, _funs_defs_groups, _globals_defs_groups = M.split_declarations_to_group_maps m.declarations in let type_infos = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 3f6470b9..ffc47741 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,11 +919,16 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (* Treat the global as a function without arguments to call *) (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> + (* + let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in + (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx + *) + failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; (* Treat the global as a fresh symbolic value *) let rty = ety_no_regions_to_rty global.ty in let sval = mk_fresh_symbolic_value V.FunCallRet rty in let sval = mk_typed_value_from_symbolic_value sval in - assign_to_place config sval place (cf Unit) ctx + (assign_to_place config sval place) (cf Unit) ctx (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index f51c15be..be43ff54 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -698,18 +698,18 @@ let fun_declaration_group_of_json (js : json) : combine_error_msgs js "fun_declaration_group_of_json" (g_declaration_group_of_json A.FunDeclId.id_of_json js) -(* TODO Should a global declaration group be converted to its function bodies ? - It does not seems very clean. -*) -let global_declaration_group_of_json (js : json) (gid_conv : global_id_converter) : - (M.fun_declaration_group, string) result = +let global_declaration_group_of_json (js : json) : + (A.GlobalDeclId.id, string) result = combine_error_msgs js "global_declaration_group_of_json" - (g_declaration_group_of_json (fun js -> - let* id = A.GlobalDeclId.id_of_json js in - Ok (global_to_fun_id gid_conv id) - ) js) - -let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result + (match js with + | `Assoc [ ("NonRec", `List [ id ]) ] -> + let* id = A.GlobalDeclId.id_of_json id in + Ok (id) + | `Assoc [ ("Rec", `List [ _ ]) ] -> + Error "got mutually dependent globals" + | _ -> Error "") + +let declaration_group_of_json (js : json) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with @@ -720,8 +720,8 @@ let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M. let* decl = fun_declaration_group_of_json decl in Ok (M.Fun decl) | `Assoc [ ("Global", `List [ decl ]) ] -> - let* decl = global_declaration_group_of_json decl gid_conv in - Ok (M.Fun decl) + let* id = global_declaration_group_of_json decl in + Ok (M.Global id) | _ -> Error "") let length_of_json_list (js: json) : (int, string) result = @@ -741,15 +741,12 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("functions", functions); ("globals", globals); ] -> - let* fun_count = length_of_json_list functions in - let gid_conv = { fun_count } in let* name = string_of_json name in - let* declarations = - list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations - in - let* types = list_of_json type_decl_of_json types in + let* declarations = list_of_json declaration_group_of_json declarations in + let* types = list_of_json type_decl_of_json types in let* functions = list_of_json fun_decl_of_json functions in - let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in + let gid_conv = { fun_count = List.length functions } in + let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in let globals, global_bodies = List.split globals in Ok { M.name; diff --git a/src/Modules.ml b/src/Modules.ml index 2f640636..009e1ba6 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -10,10 +10,11 @@ type type_declaration_group = TypeDeclId.id g_declaration_group type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show] -(** Module declaration *) +(** Module declaration. Globals cannot be mutually dependent. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group + | Global of GlobalDeclId.id [@@deriving show] type llbc_module = { @@ -44,26 +45,29 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types and functions *) +(** Split a module's declarations between types, globals and functions *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list = + type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = let rec split decls = match decls with - | [] -> ([], []) + | [] -> ([], [], []) | d :: decls' -> ( - let types, funs = split decls' in + let types, funs, globals = split decls' in match d with - | Type decl -> (decl :: types, funs) - | Fun decl -> (types, decl :: funs)) + | Type decl -> (decl :: types, funs, globals) + | Fun decl -> (types, decl :: funs, globals) + | Global decl -> (types, funs, decl :: globals) + ) in split decls -(** Split a module's declarations into two maps from type/fun ids to +(** Split a module's declarations into three maps from type/fun/global ids to declaration groups. *) let split_declarations_to_group_maps (decls : declaration_group list) : type_declaration_group TypeDeclId.Map.t - * fun_declaration_group FunDeclId.Map.t = + * fun_declaration_group FunDeclId.Map.t + * GlobalDeclId.Set.t = let module G (M : Map.S) = struct let add_group (map : M.key g_declaration_group M.t) (group : M.key g_declaration_group) : M.key g_declaration_group M.t = @@ -75,9 +79,10 @@ let split_declarations_to_group_maps (decls : declaration_group list) : M.key g_declaration_group M.t = List.fold_left add_group M.empty groups end in - let types, funs = split_declarations decls in + let types, funs, globals = split_declarations decls in let module TG = G (TypeDeclId.Map) in let types = TG.create_map types in let module FG = G (FunDeclId.Map) in let funs = FG.create_map funs in - (types, funs) + let globals = GlobalDeclId.Set.of_list globals in + (types, funs, globals) diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 2d76f348..1dc7eae9 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -32,6 +32,8 @@ type name = Names.name type type_name = Names.type_name +type global_name = Names.global_name + type fun_name = Names.fun_name (* TODO: this should a module we give to a functor! *) @@ -71,10 +73,11 @@ type formatter = { *) type_name : type_name -> string; (** Provided a basename, compute a type name. *) + global_name : global_name -> string; + (** Provided a basename, compute a global name. *) fun_name : A.fun_id -> fun_name -> - bool -> int -> region_group_info option -> bool * int -> @@ -83,7 +86,6 @@ type formatter = { - function id: this is especially useful to identify whether the function is an assumed function or a local function - function basename - - flag indicating if the function is a global - number of region groups - region group information in case of a backward function (`None` if forward function) @@ -186,6 +188,7 @@ type formatter = { (** We use identifiers to look for name clashes *) type id = + | GlobalId of A.GlobalDeclId.id | FunId of A.fun_id * RegionGroupId.id option | DecreasesClauseId of A.fun_id (** The definition which provides the decreases/termination clause. @@ -342,6 +345,7 @@ type extraction_ctx = { (** Debugging function *) let id_to_string (id : id) (ctx : extraction_ctx) : string = + let global_decls = ctx.trans_ctx.global_context.global_decls in let fun_decls = ctx.trans_ctx.fun_context.fun_decls in let type_decls = ctx.trans_ctx.type_context.type_decls in (* TODO: factorize the pretty-printing with what is in PrintPure *) @@ -354,6 +358,9 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | Tuple -> failwith "Unreachable" in match id with + | GlobalId gid -> + let name = (A.GlobalDeclId.Map.find gid global_decls).name in + "global name: " ^ Print.global_name_to_string name | FunId (fid, rg_id) -> let fun_name = match fid with @@ -442,6 +449,12 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found +let ctx_get_global_decl (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx ^ "_c" + +let ctx_get_global_body (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx ^ "_body" + let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = @@ -572,6 +585,10 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx +let ctx_add_global_decl (def : A.global_decl) (ctx : extraction_ctx) : + extraction_ctx = + ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx + let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = (* Lookup the LLBC def to compute the region group information *) @@ -600,11 +617,12 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let def_id = A.Regular def_id in let name = - ctx.fmt.fun_name def_id def.basename def.is_global_body num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in - (* Add the function name *) - let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in - ctx + (* Add the function name if it's not a global *) + if def.is_global_body + then ctx + else ctx_add (FunId (def_id, def.back_id)) name ctx type names_map_init = { keywords : string list; @@ -671,7 +689,6 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string = TODO: move all those helpers. *) let default_fun_suffix - (is_global_body : bool) (num_region_groups : int) (rg : region_group_info option) ((keep_fwd, num_backs) : bool * int) @@ -691,7 +708,6 @@ let default_fun_suffix we could not add the "_fwd" suffix) to prevent name clashes between definitions (in particular between type and function definitions). *) - if is_global_body then "_body" else match rg with | None -> "_fwd" | Some rg -> diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml index c63814eb..39fb5073 100644 --- a/src/PureTypeCheck.ml +++ b/src/PureTypeCheck.ml @@ -112,11 +112,8 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = check_texpression ctx body | Qualif qualif -> ( match qualif.id with - | Func _ -> () (* TODO *) - | Global id -> - let global = A.GlobalDeclId.Map.find id ctx.global_decls in - (* TODO: something like assert (global.ty = e.ty) *) - failwith "PureTypeCheck.ml:118" + | Func _ -> () (* TODO *) + | Global _ -> () (* TODO *) | Proj { adt_id = proj_adt_id; field_id } -> (* Note we can only project fields of structures (not enumerations) *) (* Deconstruct the projector type *) diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 8d3b5258..8a1c074d 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -399,6 +399,11 @@ let type_decl_is_enum (def : T.type_decl) : bool = let mk_state_ty : ty = Adt (Assumed State, []) let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) +let unwrap_result_ty (ty : ty) : ty = + match ty with + | Adt (Assumed Result, [ ty ]) -> ty + | _ -> failwith "not a result" + let mk_result_fail_texpression (ty : ty) : texpression = let type_args = [ ty ] in let ty = Adt (Assumed Result, type_args) in diff --git a/src/Translate.ml b/src/Translate.ml index a6477e7f..a936d626 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -298,7 +298,7 @@ let translate_module_to_pure (config : C.partial_config) (* Compute the type and function contexts *) let type_context, fun_context, global_context = compute_type_fun_contexts m in - let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in + let fun_infos = FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls use_state in let fun_context = { fun_decls = fun_context.fun_decls; fun_infos; @@ -498,9 +498,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) - then if def.is_global_body - then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt qualif def - else ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def + then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif has_decr_clause def ) fls); (* Insert unit tests if necessary *) @@ -512,6 +510,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) pure_ls in + (* TODO: Check correct behaviour with opaque globals *) + let export_global (id : A.GlobalDeclId.id) : unit = + let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in + let global = A.GlobalDeclId.Map.find id global_decls in + let (_, (body, body_backs)) = A.FunDeclId.Map.find global.body_id ctx.trans_funs in + assert (List.length body_backs = 0); + + let is_opaque = Option.is_none body.Pure.body in + if ((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque) + then ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body config.interface + in + let export_state_type () : unit = let qualif = if config.interface then ExtractToFStar.TypeVal @@ -547,6 +558,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) in (* Translate *) export_functions true pure_funs + | Global id -> + export_global id in (* If we need to export the state type: we try to export it after we defined diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index 06425e64..e1a942a0 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -4,138 +4,3 @@ module Constants open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [constants::X0] *) -let x0_body : result u32 = Return 0 -let x0_c : u32 = eval_global x0_body - -(** [core::num::u32::{8}::MAX] *) -let core_num_u32_max_body : result u32 = Return 4294967295 -let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body - -(** [constants::X1] *) -let x1_body : result u32 = let i = core_num_u32_max_c in Return i -let x1_c : u32 = eval_global x1_body - -(** [constants::X2] *) -let x2_body : result u32 = Return 3 -let x2_c : u32 = eval_global x2_body - -(** [constants::incr] *) -let incr_fwd (n : u32) : result u32 = - begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end - -(** [constants::X3] *) -let x3_body : result u32 = - begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end -let x3_c : u32 = eval_global x3_body - -(** [constants::mk_pair0] *) -let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) - -(** [constants::Pair] *) -type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } - -(** [constants::mk_pair1] *) -let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = - Return (Mkpair_t x y) - -(** [constants::P0] *) -let p0_body : result (u32 & u32) = - begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end -let p0_c : (u32 & u32) = eval_global p0_body - -(** [constants::P1] *) -let p1_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end -let p1_c : pair_t u32 u32 = eval_global p1_body - -(** [constants::P2] *) -let p2_body : result (u32 & u32) = Return (0, 1) -let p2_c : (u32 & u32) = eval_global p2_body - -(** [constants::P3] *) -let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1) -let p3_c : pair_t u32 u32 = eval_global p3_body - -(** [constants::Wrap] *) -type wrap_t (t : Type0) = { wrap_val : t; } - -(** [constants::Wrap::{0}::new] *) -let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = - Return (Mkwrap_t val0) - -(** [constants::Y] *) -let y_body : result (wrap_t i32) = - begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end -let y_c : wrap_t i32 = eval_global y_body - -(** [constants::unwrap_y] *) -let unwrap_y_fwd : result i32 = let w = y_c in Return w.wrap_val - -(** [constants::YVAL] *) -let yval_body : result i32 = - begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end -let yval_c : i32 = eval_global yval_body - -(** [constants::get_z1::Z1] *) -let get_z1_z1_body : result i32 = Return 3 -let get_z1_z1_c : i32 = eval_global get_z1_z1_body - -(** [constants::get_z1] *) -let get_z1_fwd : result i32 = let i = get_z1_z1_c in Return i - -(** [constants::add] *) -let add_fwd (a : i32) (b : i32) : result i32 = - begin match i32_add a b with | Fail -> Fail | Return i -> Return i end - -(** [constants::Q1] *) -let q1_body : result i32 = Return 5 -let q1_c : i32 = eval_global q1_body - -(** [constants::Q2] *) -let q2_body : result i32 = let i = q1_c in Return i -let q2_c : i32 = eval_global q2_body - -(** [constants::Q3] *) -let q3_body : result i32 = - let i = q2_c in - begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end -let q3_c : i32 = eval_global q3_body - -(** [constants::get_z2] *) -let get_z2_fwd : result i32 = - begin match get_z1_fwd with - | Fail -> Fail - | Return i -> - let i0 = q3_c in - begin match add_fwd i i0 with - | Fail -> Fail - | Return i1 -> - let i2 = q1_c in - begin match add_fwd i2 i1 with - | Fail -> Fail - | Return i3 -> Return i3 - end - end - end - -(** [constants::S1] *) -let s1_body : result u32 = Return 6 -let s1_c : u32 = eval_global s1_body - -(** [constants::S2] *) -let s2_body : result u32 = - let i = s1_c in - begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end -let s2_c : u32 = eval_global s2_body - -(** [constants::S3] *) -let s3_body : result (pair_t u32 u32) = let p = p3_c in Return p -let s3_c : pair_t u32 u32 = eval_global s3_body - -(** [constants::S4] *) -let s4_body : result (pair_t u32 u32) = - begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end -let s4_c : pair_t u32 u32 = eval_global s4_body - -- cgit v1.3.1 From 3c5fb260012ee8bb8b9fd90bc4624d893ac7678a Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 8 Aug 2022 15:16:14 +0200 Subject: Register global names, one error remaining --- src/ExtractToFStar.ml | 5 +++++ src/InterpreterStatements.ml | 8 ++++++-- src/SymbolicToPure.ml | 8 +++++++- src/Translate.ml | 6 +++++- tests/misc/Constants.fst | 10 ++++++++++ 5 files changed, 33 insertions(+), 4 deletions(-) (limited to 'tests') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index a2b15ece..c915aede 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -794,6 +794,11 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (* Return *) ctx +(** Simply add the global name to the context. *) +let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) + : extraction_ctx = + ctx_add_global_decl def ctx + (** The following function factorizes the extraction of ADT values. Note that patterns can introduce new variables: we thus return an extraction diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index ffc47741..31c3aabb 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -919,16 +919,20 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (* Treat the global as a function without arguments to call *) (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> + (* Treat the global as a fresh symbolic value *) + (* let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx - *) + failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; - (* Treat the global as a fresh symbolic value *) + *) + let rty = ety_no_regions_to_rty global.ty in let sval = mk_fresh_symbolic_value V.FunCallRet rty in let sval = mk_typed_value_from_symbolic_value sval in (assign_to_place config sval place) (cf Unit) ctx + (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 83cce3e9..16e48aef 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -687,7 +687,13 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) : List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = - V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var + try (V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var) with + Not_found -> + print_endline ("Missing " ^ Print.V.show_symbolic_value sv); + V.SymbolicValueId.Map.iter (fun id (v : var) -> + print_endline (" -- " ^ (Option.value v.basename ~default:"")) + ) ctx.sv_to_var; + raise Not_found (** Peel boxes as long as the value is of the form `Box` *) let rec unbox_typed_value (v : V.typed_value) : V.typed_value = diff --git a/src/Translate.ml b/src/Translate.ml index a936d626..fdd6d05f 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -655,7 +655,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) m.declarations)) in - (* Register unique names for all the top-level types and functions. + (* Register unique names for all the top-level types, functions and globals. * Note that the order in which we generate the names doesn't matter: * we just need to generate a mapping from identifier to name, and make * sure there are no name clashes. *) @@ -677,6 +677,10 @@ let translate_module (filename : string) (dest_dir : string) (config : config) ctx trans_funs in + let ctx = List.fold_left + ExtractToFStar.extract_global_decl_register_names ctx m.globals + in + (* Open the output file *) (* First compute the filename by replacing the extension and converting the * case (rust module names are snake case) *) diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index e1a942a0..f5bd41cb 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -4,3 +4,13 @@ module Constants open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [constants::X0] *) +let x0_body : result u32 = Return 0 +let x0_c : u32 = eval_global x0_body + +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** [constants::X1] *) \ No newline at end of file -- cgit v1.3.1 From cd754eabe3af025ca3465c5fc6d8cb48da66a1ae Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 10 Aug 2022 18:56:25 +0200 Subject: Corrected translation without using functions, remaining bug in hashmap translation --- src/ExtractToFStar.ml | 2 +- src/InterpreterBorrows.ml | 2 +- src/InterpreterStatements.ml | 17 +--- src/InterpreterUtils.ml | 4 +- src/SymbolicAst.ml | 2 + src/SymbolicToPure.ml | 21 +++-- src/SynthesizeSymbolic.ml | 6 ++ src/Values.ml | 1 + tests/hashmap/Hashmap.Clauses.Template.fst | 4 + tests/hashmap/Hashmap.Funs.fst | 19 +++-- tests/hashmap/Hashmap.Types.fst | 4 + tests/misc/Constants.fst | 123 ++++++++++++++++++++++++++++- 12 files changed, 170 insertions(+), 35 deletions(-) (limited to 'tests') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index c915aede..f2c481c0 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1363,7 +1363,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) : unit = - assert (def.is_global_body); + assert (not def.is_global_body); (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index a13ac786..6b920a51 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -436,7 +436,7 @@ let give_back_symbolic_value (_config : C.config) assert (sv.sv_id <> nsv.sv_id); (match nsv.sv_kind with | V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> () - | V.FunCallRet | V.SynthInput -> failwith "Unrechable"); + | V.FunCallRet | V.SynthInput | V.Global -> failwith "Unrechable"); (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 31c3aabb..48620439 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -920,19 +920,10 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx | SymbolicMode -> (* Treat the global as a fresh symbolic value *) - - (* - let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in - (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx - - failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value"; - *) - - let rty = ety_no_regions_to_rty global.ty in - let sval = mk_fresh_symbolic_value V.FunCallRet rty in - let sval = mk_typed_value_from_symbolic_value sval in - (assign_to_place config sval place) (cf Unit) ctx - + let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in + let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in + let e = cc (cf Unit) ctx in + S.synthesize_global_eval gid sval e (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 47323cc2..6ef66f1d 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -238,8 +238,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx) raise Found else () | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack - | V.SynthRetGivenBack -> - () + | V.SynthRetGivenBack -> () + | V.Global -> () end in (* We use exceptions *) diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 9cab092d..fd490e43 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -65,6 +65,8 @@ type expression = | Panic | FunCall of call * expression | EndAbstraction of V.abs * expression + | EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression + (** A fresh symbolic value for the global *) | Expansion of mplace option * V.symbolic_value * expansion (** Expansion of a symbolic value. diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 16e48aef..81af6a8b 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -687,13 +687,7 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) : List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = - try (V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var) with - Not_found -> - print_endline ("Missing " ^ Print.V.show_symbolic_value sv); - V.SymbolicValueId.Map.iter (fun id (v : var) -> - print_endline (" -- " ^ (Option.value v.basename ~default:"")) - ) ctx.sv_to_var; - raise Not_found + V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var (** Peel boxes as long as the value is of the form `Box` *) let rec unbox_typed_value (v : V.typed_value) : V.typed_value = @@ -1080,6 +1074,7 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx) | Panic -> translate_panic ctx | FunCall (call, e) -> translate_function_call config call e ctx | EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx + | EvalGlobal (gid, sv, e) -> translate_global_eval config gid sv e ctx | Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx | Meta (meta, e) -> translate_meta config meta e ctx @@ -1466,6 +1461,18 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) mk_let monadic given_back (mk_texpression_from_var input_var) e) given_back_inputs next_e +and translate_global_eval (config : config) (gid : A.GlobalDeclId.id) + (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) + : texpression = + let (ctx, var) = fresh_var_for_symbolic_value sval ctx in + let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in + let global_expr = { id = Global gid; type_args = [] } in + (* We use translate_fwd_ty to translate the global type *) + let ty = ctx_translate_fwd_ty ctx decl.ty in + let gval = { e = Qualif global_expr; ty } in + let e = translate_expression config e ctx in + mk_let false (mk_typed_pattern_from_var var None) gval e + and translate_expansion (config : config) (p : S.mplace option) (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression = (* Translate the scrutinee *) diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml index 95da38e6..fa244649 100644 --- a/src/SynthesizeSymbolic.ml +++ b/src/SynthesizeSymbolic.ml @@ -114,6 +114,12 @@ let synthesize_function_call (call_id : call_id) in Some (FunCall (call, expr)) +let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (expr : expression option) + : expression option = + match expr with + | None -> None + | Some e -> Some (EvalGlobal (gid, dest, e)) + let synthesize_regular_function_call (fun_id : A.fun_id) (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list) (type_params : T.ety list) (args : V.typed_value list) diff --git a/src/Values.ml b/src/Values.ml index 4585b443..13cd2580 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -65,6 +65,7 @@ type sv_kind = *) | SynthInputGivenBack (** The value was given back upon ending one of the input abstractions *) + | Global (** The value is a global *) [@@deriving show] type symbolic_value = { diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst index c1549e6b..2a3d9cb9 100644 --- a/tests/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/hashmap/Hashmap.Clauses.Template.fst @@ -24,6 +24,10 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : list_t t) : nat = admit () +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold let hash_map_move_elements_from_list_decreases (t : Type0) diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index 921ed142..397ee720 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -248,24 +248,23 @@ let rec hash_map_move_elements_fwd_back (** [hashmap::HashMap::{0}::try_resize] *) let hash_map_try_resize_fwd_back (t : Type0) (self : hash_map_t t) : result (hash_map_t t) = - let i = core_num_u32_max_c in - begin match scalar_cast U32 Usize i with + begin match scalar_cast U32 Usize core_num_u32_max_c with | Fail -> Fail | Return max_usize -> let capacity = vec_len (list_t t) self.hash_map_slots in begin match usize_div max_usize 2 with | Fail -> Fail | Return n1 -> - let (i0, i1) = self.hash_map_max_load_factor in - begin match usize_div n1 i0 with + let (i, i0) = self.hash_map_max_load_factor in + begin match usize_div n1 i with | Fail -> Fail - | Return i2 -> - if capacity <= i2 + | Return i1 -> + if capacity <= i1 then begin match usize_mul capacity 2 with | Fail -> Fail - | Return i3 -> - begin match hash_map_new_with_capacity_fwd t i3 i0 i1 with + | Return i2 -> + begin match hash_map_new_with_capacity_fwd t i2 i i0 with | Fail -> Fail | Return ntable -> begin match @@ -273,13 +272,13 @@ let hash_map_try_resize_fwd_back with | Fail -> Fail | Return (ntable0, _) -> - Return (Mkhash_map_t self.hash_map_num_entries (i0, i1) + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) ntable0.hash_map_max_load ntable0.hash_map_slots) end end end else - Return (Mkhash_map_t self.hash_map_num_entries (i0, i1) + Return (Mkhash_map_t self.hash_map_num_entries (i, i0) self.hash_map_max_load self.hash_map_slots) end end diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst index 91ee26c6..f81f4185 100644 --- a/tests/hashmap/Hashmap.Types.fst +++ b/tests/hashmap/Hashmap.Types.fst @@ -19,3 +19,7 @@ type hash_map_t (t : Type0) = hash_map_slots : vec (list_t t); } +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index f5bd41cb..5cfb82d6 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -13,4 +13,125 @@ let x0_c : u32 = eval_global x0_body let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body -(** [constants::X1] *) \ No newline at end of file +(** [constants::X1] *) +let x1_body : result u32 = Return core_num_u32_max_c +let x1_c : u32 = eval_global x1_body + +(** [constants::X2] *) +let x2_body : result u32 = Return 3 +let x2_c : u32 = eval_global x2_body + +(** [constants::incr] *) +let incr_fwd (n : u32) : result u32 = + begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end + +(** [constants::X3] *) +let x3_body : result u32 = + begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end +let x3_c : u32 = eval_global x3_body + +(** [constants::mk_pair0] *) +let mk_pair0_fwd (x : u32) (y0 : u32) : result (u32 & u32) = Return (x, y0) + +(** [constants::Pair] *) +type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } + +(** [constants::mk_pair1] *) +let mk_pair1_fwd (x : u32) (y0 : u32) : result (pair_t u32 u32) = + Return (Mkpair_t x y0) + +(** [constants::P0] *) +let p0_body : result (u32 & u32) = + begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end +let p0_c : (u32 & u32) = eval_global p0_body + +(** [constants::P1] *) +let p1_body : result (pair_t u32 u32) = + begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end +let p1_c : pair_t u32 u32 = eval_global p1_body + +(** [constants::P2] *) +let p2_body : result (u32 & u32) = Return (0, 1) +let p2_c : (u32 & u32) = eval_global p2_body + +(** [constants::P3] *) +let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1) +let p3_c : pair_t u32 u32 = eval_global p3_body + +(** [constants::Wrap] *) +type wrap_t (t : Type0) = { wrap_val : t; } + +(** [constants::Wrap::{0}::new] *) +let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = + Return (Mkwrap_t val0) + +(** [constants::Y] *) +let y_body : result (wrap_t i32) = + begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end +let y_c : wrap_t i32 = eval_global y_body + +(** [constants::unwrap_y] *) +let unwrap_y_fwd : result i32 = Return y_c.wrap_val + +(** [constants::YVAL] *) +let yval_body : result i32 = + begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end +let yval_c : i32 = eval_global yval_body + +(** [constants::get_z1::Z1] *) +let get_z1_z1_body : result i32 = Return 3 +let get_z1_z1_c : i32 = eval_global get_z1_z1_body + +(** [constants::get_z1] *) +let get_z1_fwd : result i32 = Return get_z1_z1_c + +(** [constants::add] *) +let add_fwd (a : i32) (b : i32) : result i32 = + begin match i32_add a b with | Fail -> Fail | Return i -> Return i end + +(** [constants::Q1] *) +let q1_body : result i32 = Return 5 +let q1_c : i32 = eval_global q1_body + +(** [constants::Q2] *) +let q2_body : result i32 = Return q1_c +let q2_c : i32 = eval_global q2_body + +(** [constants::Q3] *) +let q3_body : result i32 = + begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end +let q3_c : i32 = eval_global q3_body + +(** [constants::get_z2] *) +let get_z2_fwd : result i32 = + begin match get_z1_fwd with + | Fail -> Fail + | Return i -> + begin match add_fwd i q3_c with + | Fail -> Fail + | Return i0 -> + begin match add_fwd q1_c i0 with + | Fail -> Fail + | Return i1 -> Return i1 + end + end + end + +(** [constants::S1] *) +let s1_body : result u32 = Return 6 +let s1_c : u32 = eval_global s1_body + +(** [constants::S2] *) +let s2_body : result u32 = + begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end +let s2_c : u32 = eval_global s2_body + +(** [constants::S3] *) +let s3_body : result (pair_t u32 u32) = Return p3_c +let s3_c : pair_t u32 u32 = eval_global s3_body + +(** [constants::S4] *) +let s4_body : result (pair_t u32 u32) = + begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end +let s4_c : pair_t u32 u32 = eval_global s4_body + -- cgit v1.3.1 From fa491861faed3ba5ed4fe806b55bea663a29579c Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 11 Aug 2022 10:39:04 +0200 Subject: Correct assertion for stateless globals --- src/FunsAnalysis.ml | 2 +- tests/betree/BetreeMain.Clauses.Template.fst | 4 ++++ tests/betree/BetreeMain.Funs.fst | 7 +++---- tests/betree/BetreeMain.Types.fsti | 4 ++++ .../HashmapMain.Clauses.Template.fst | 4 ++++ tests/hashmap_on_disk/HashmapMain.Funs.fst | 21 ++++++++++----------- tests/hashmap_on_disk/HashmapMain.Types.fsti | 4 ++++ 7 files changed, 30 insertions(+), 16 deletions(-) (limited to 'tests') diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index 65a130c8..39fa316d 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -94,7 +94,7 @@ let analyze_module (m : llbc_module) super#visit_Loop env loop end in - assert (not f.is_global_body || not use_state); + assert (not f.is_global_body || not !stateful); (match f.body with | None -> (* Opaque function *) diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst index 5a9776ab..c2412775 100644 --- a/tests/betree/BetreeMain.Clauses.Template.fst +++ b/tests/betree/BetreeMain.Clauses.Template.fst @@ -6,6 +6,10 @@ open BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** [core::num::u64::{9}::MAX] *) +let core_num_u64_max_body : result u64 = Return 18446744073709551615 +let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body + (** [betree_main::betree::List::{1}::len]: decreases clause *) unfold let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : nat = diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index 4761b6a3..e80e96a6 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -96,17 +96,16 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - let i = core_num_u64_max_c in - begin match u64_sub i prev0 with + begin match u64_sub core_num_u64_max_c prev0 with | Fail -> Fail | Return margin -> if margin >= v then begin match u64_add prev0 v with | Fail -> Fail - | Return i0 -> Return i0 + | Return i -> Return i end - else let i0 = core_num_u64_max_c in Return i0 + else Return core_num_u64_max_c end | BetreeUpsertFunStateSub v -> if prev0 >= v diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti index aad9cb43..f0ca1d9e 100644 --- a/tests/betree/BetreeMain.Types.fsti +++ b/tests/betree/BetreeMain.Types.fsti @@ -55,6 +55,10 @@ type betree_be_tree_t = betree_be_tree_root : betree_node_t; } +(** [core::num::u64::{9}::MAX] *) +let core_num_u64_max_body : result u64 = Return 18446744073709551615 +let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body + (** The state type used in the state-error monad *) val state : Type0 diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst index 3c5ee819..0cf876d9 100644 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -24,6 +24,10 @@ let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : nat = admit () +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *) unfold let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index 1d8ee3da..83bf80d1 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -261,24 +261,23 @@ let rec hashmap_hash_map_move_elements_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) let hashmap_hash_map_try_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - let i = core_num_u32_max_c in - begin match scalar_cast U32 Usize i with + begin match scalar_cast U32 Usize core_num_u32_max_c with | Fail -> Fail | Return max_usize -> let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in begin match usize_div max_usize 2 with | Fail -> Fail | Return n1 -> - let (i0, i1) = self.hashmap_hash_map_max_load_factor in - begin match usize_div n1 i0 with + let (i, i0) = self.hashmap_hash_map_max_load_factor in + begin match usize_div n1 i with | Fail -> Fail - | Return i2 -> - if capacity <= i2 + | Return i1 -> + if capacity <= i1 then begin match usize_mul capacity 2 with | Fail -> Fail - | Return i3 -> - begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 with + | Return i2 -> + begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with | Fail -> Fail | Return ntable -> begin match @@ -287,14 +286,14 @@ let hashmap_hash_map_try_resize_fwd_back | Fail -> Fail | Return (ntable0, _) -> Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries - (i0, i1) ntable0.hashmap_hash_map_max_load + (i, i0) ntable0.hashmap_hash_map_max_load ntable0.hashmap_hash_map_slots) end end end else - Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i0, - i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) + Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, + i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots) end end end diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti index e289174b..370844db 100644 --- a/tests/hashmap_on_disk/HashmapMain.Types.fsti +++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti @@ -19,6 +19,10 @@ type hashmap_hash_map_t (t : Type0) = hashmap_hash_map_slots : vec (hashmap_list_t t); } +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + (** The state type used in the state-error monad *) val state : Type0 -- cgit v1.3.1 From e7f76a4e46f24f54e5b49efee40e33e11128f49c Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 11 Aug 2022 18:04:10 +0200 Subject: Correct last PR remarks --- src/ExtractToFStar.ml | 24 ++++++++---------------- src/PureToExtract.ml | 16 +++++++++------- tests/misc/Constants.fst | 6 +++--- 3 files changed, 20 insertions(+), 26 deletions(-) (limited to 'tests') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index f2c481c0..7f271f02 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -797,7 +797,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (** Simply add the global name to the context. *) let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) : extraction_ctx = - ctx_add_global_decl def ctx + ctx_add_global_decl_body def ctx (** The following function factorizes the extraction of ADT values. @@ -852,7 +852,7 @@ let extract_adt_g_value (* Extract globals in the same way as variables *) let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global_decl id ctx) + F.pp_print_string fmt (ctx_get_global id ctx) (** [inside]: see [extract_ty]. @@ -1491,16 +1491,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 -(* Change the suffix from "_c" to "_body" *) -let global_decl_to_body_name (decl : string) : string = - (* The declaration length without the global suffix *) - let base_len = String.length decl - 2 in - (* TODO: Use String.ends_with instead when a more recent version of OCaml is used *) - assert (String.sub decl base_len 2 = "_c"); - (String.sub decl 0 base_len) ^ "_body" - (** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) -let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) +let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (name : string) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) : unit = @@ -1574,8 +1566,8 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); F.pp_print_space fmt (); - let decl_name = ctx_get_global_decl global.def_id ctx in - let body_name = ctx_get_global_body global.def_id ctx in + let decl_name = ctx_get_global global.def_id ctx in + let body_name = ctx_get_function (Regular global.body_id) None ctx in let decl_ty, body_ty = let ty = body.signature.output in @@ -1586,13 +1578,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) match body.body with | None -> let qualif = if interface then Val else AssumeVal in - extract_global_definition ctx fmt qualif decl_name decl_ty None + extract_global_decl_body ctx fmt qualif decl_name decl_ty None | Some body -> - extract_global_definition ctx fmt Let body_name body_ty (Some (fun fmt -> + extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body )); F.pp_print_break fmt 0 0; - extract_global_definition ctx fmt Let decl_name decl_ty (Some (fun fmt -> + extract_global_decl_body ctx fmt Let decl_name decl_ty (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name) )); F.pp_print_break fmt 0 0 diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 1dc7eae9..b7d45deb 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -449,12 +449,9 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found -let ctx_get_global_decl (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (GlobalId id) ctx ^ "_c" +let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx -let ctx_get_global_body (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (GlobalId id) ctx ^ "_body" - let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = @@ -585,9 +582,14 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx -let ctx_add_global_decl (def : A.global_decl) (ctx : extraction_ctx) : +let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = - ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx + let name = ctx.fmt.global_name def.name in + let decl = GlobalId def.def_id in + let body = FunId (Regular def.body_id, None) in + let ctx = ctx_add decl (name ^ "_c") ctx in + let ctx = ctx_add body (name ^ "_body") ctx in + ctx let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index 5cfb82d6..4a9a0e48 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -31,14 +31,14 @@ let x3_body : result u32 = let x3_c : u32 = eval_global x3_body (** [constants::mk_pair0] *) -let mk_pair0_fwd (x : u32) (y0 : u32) : result (u32 & u32) = Return (x, y0) +let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) (** [constants::Pair] *) type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } (** [constants::mk_pair1] *) -let mk_pair1_fwd (x : u32) (y0 : u32) : result (pair_t u32 u32) = - Return (Mkpair_t x y0) +let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = + Return (Mkpair_t x y) (** [constants::P0] *) let p0_body : result (u32 & u32) = -- cgit v1.3.1 From e18bf82b0931a7fd8a357a8516ef8618d77d42cf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:27:24 +0200 Subject: Regenerate the translated files --- tests/betree/Primitives.fst | 2 +- tests/hashmap/Primitives.fst | 2 +- tests/hashmap_on_disk/Primitives.fst | 2 +- tests/misc/Primitives.fst | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) (limited to 'tests') diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/Primitives.fst @@ -34,7 +34,7 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail -// Unwrap a successful result by normalisation (used for globals). +// Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x (*** Misc *) diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/hashmap/Primitives.fst +++ b/tests/hashmap/Primitives.fst @@ -34,7 +34,7 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail -// Unwrap a successful result by normalisation (used for globals). +// Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x (*** Misc *) diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/hashmap_on_disk/Primitives.fst +++ b/tests/hashmap_on_disk/Primitives.fst @@ -34,7 +34,7 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail -// Unwrap a successful result by normalisation (used for globals). +// Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x (*** Misc *) diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/misc/Primitives.fst +++ b/tests/misc/Primitives.fst @@ -34,7 +34,7 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = // Monadic assert(...) let massert (b:bool) : result unit = if b then Return () else Fail -// Unwrap a successful result by normalisation (used for globals). +// Normalize and unwrap a successful result (used for globals). let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x (*** Misc *) -- cgit v1.3.1