From ba61ed50e7b2fdc78690de92d734a3747029f903 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 8 Jun 2022 12:32:14 +0200 Subject: read globals from LLBC JSON into functions --- src/Modules.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Modules.ml') diff --git a/src/Modules.ml b/src/Modules.ml index f52983c6..6d0cf70c 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,5 +1,6 @@ open Types open LlbcAst +open FunIdentifier type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] -- cgit v1.3.1 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 --- Makefile | 2 +- src/Contexts.ml | 11 ++- src/Expressions.ml | 23 +----- src/ExtractToFStar.ml | 3 +- src/FunIdentifier.ml | 3 - src/FunsAnalysis.ml | 1 - src/Interpreter.ml | 7 +- src/InterpreterExpressions.ml | 83 +++++--------------- src/InterpreterStatements.ml | 16 +++- src/InterpreterUtils.ml | 2 - src/LlbcAst.ml | 27 ++++++- src/LlbcAstUtils.ml | 1 - src/LlbcOfJson.ml | 173 ++++++++++++++++++++---------------------- src/Modules.ml | 2 +- src/Print.ml | 78 +++++++++---------- src/PrintPure.ml | 7 +- src/Pure.ml | 3 +- src/PureToExtract.ml | 13 ++-- src/Substitute.ml | 11 +-- src/SymbolicToPure.ml | 27 ++++--- src/Translate.ml | 36 +++++---- src/TranslateCore.ml | 10 +-- src/main.ml | 30 ++++---- tests/misc/Constants.fst | 119 +++++++++++++++++++++++++++++ 24 files changed, 380 insertions(+), 308 deletions(-) delete mode 100644 src/FunIdentifier.ml create mode 100644 tests/misc/Constants.fst (limited to 'src/Modules.ml') diff --git a/Makefile b/Makefile index 4dc1475b..0fc3fcf4 100644 --- a/Makefile +++ b/Makefile @@ -48,7 +48,7 @@ trans-hashmap_main: SUBDIR:=hashmap_on_disk trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses trans-nll-betree_nll: SUBDIR:=misc -trans-constants: TRANS_OPTIONS += -no-split-files -no-state -no-decreases-clauses +trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += diff --git a/src/Contexts.ml b/src/Contexts.ml index bbf5b8f3..1fbc916b 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -1,7 +1,6 @@ open Types open Values open LlbcAst -open FunIdentifier module V = Values open ValuesUtils module M = Modules @@ -218,7 +217,11 @@ type type_context = { } [@@deriving show] -type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show] +type fun_context = { + fun_decls : fun_decl FunDeclId.Map.t; + gid_conv : global_id_converter; +} +[@@deriving show] type eval_ctx = { type_context : type_context; @@ -256,6 +259,10 @@ let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl = let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = FunDeclId.Map.find fid ctx.fun_context.fun_decls +(** TODO: make this more efficient with maps *) +let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl = + ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid) + (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = (* We take care to stop at the end of current frame: different variables diff --git a/src/Expressions.ml b/src/Expressions.ml index f1a4a8c3..6645a77f 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -1,6 +1,5 @@ open Types open Values -open FunIdentifier type field_proj_kind = | ProjAdt of TypeDeclId.id * VariantId.id option @@ -73,31 +72,11 @@ let all_binops = Shr; ] -(** Constant value for an operand - - It is a bit annoying, but rustc treats some ADT and tuple instances as - constants when generating MIR: - - an enumeration with one variant and no fields is a constant. - - a structure with no field is a constant. - - sometimes, Rust stores the initialization of an ADT as a constant - (if all the fields are constant) rather than as an aggregated value - - For our translation, we use the following enumeration to encode those - special cases in assignments. They are converted to "normal" values - when evaluating the assignment (which is why we don't put them in the - [ConstantValue] enumeration). - *) -type operand_constant_value = - | ConstantValue of constant_value - | ConstantId of FunDeclId.id - | ConstantAdt of VariantId.id option * operand_constant_value list -[@@deriving show] - (* TODO: symplify the operand constant values *) type operand = | Copy of place | Move of place - | Constant of ety * operand_constant_value + | Constant of ety * constant_value [@@deriving show] (** An aggregated ADT. diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index b85c146b..b89579b5 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -6,7 +6,6 @@ open PureUtils open TranslateCore open PureToExtract open StringUtils -open FunIdentifier module F = Format (** A qualifier for a type definition. @@ -315,7 +314,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ suffix in - let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string = + let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) let suffix = "_decreases" in diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml deleted file mode 100644 index 956fce3f..00000000 --- a/src/FunIdentifier.ml +++ /dev/null @@ -1,3 +0,0 @@ -open Identifiers -module FunDeclId = IdGen () -module GlobalDeclId = IdGen () diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index cf2e0bd6..dc205eb9 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -9,7 +9,6 @@ open LlbcAst open Modules -open FunIdentifier type fun_info = { can_fail : bool; diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 702aeea6..5affea4c 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,5 +1,4 @@ open Cps -open FunIdentifier open InterpreterUtils open InterpreterProjectors open InterpreterBorrows @@ -25,7 +24,7 @@ let compute_type_fun_contexts (m : M.llbc_module) : TypesAnalysis.analyze_type_declarations type_decls type_decls_list in let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls } in + let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in (type_context, fun_context) let initialize_eval_context (type_context : C.type_context) @@ -256,9 +255,9 @@ module Test = struct environment. *) let test_unit_function (config : C.partial_config) (m : M.llbc_module) - (fid : FunDeclId.id) : unit = + (fid : A.FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = FunDeclId.nth m.functions fid in + let fdef = A.FunDeclId.nth m.functions fid in let body = Option.get fdef.body in (* Debug *) diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index ee26d00d..57ee0526 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -71,68 +71,23 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool) in comp cc read_place cf ctx -(** Convert an operand constant operand value to a typed value *) -let rec eval_operand_constant_value (ty : T.ety) - (cv : E.operand_constant_value) (cf : V.typed_value -> m_fun) : m_fun = - fun ctx -> - (* Check the type while converting - we actually need some information - * contained in the type *) - log#ldebug - (lazy - ("eval_operand_constant_value:" ^ "\n- ty: " - ^ ety_to_string ctx ty ^ "\n- cv: " - ^ operand_constant_value_to_string ctx cv)); - match (ty, cv) with - (* Adt *) - | ( T.Adt (adt_id, region_params, type_params), - ConstantAdt (variant_id, field_values) ) -> - assert (region_params = []); - (* Compute the types of the fields *) - let field_tys = - match adt_id with - | T.AdtId def_id -> - let def = C.ctx_lookup_type_decl ctx def_id in - assert (def.region_params = []); - Subst.type_decl_get_instantiated_field_etypes def variant_id - type_params - | T.Tuple -> type_params - | T.Assumed _ -> failwith "Unreachable" - in - let adt_cf = fun fields ctx -> - let value = V.Adt { variant_id; field_values = fields } in - cf { value; ty } ctx - in - (* Map the field values & types to the continuation above *) - fold_left_apply_continuation - (fun (ty, v) cf ctx -> eval_operand_constant_value ty v cf ctx) - (List.combine field_tys field_values) - adt_cf ctx - (* Scalar, boolean... *) - | T.Bool, ConstantValue (Bool v) -> cf { V.value = V.Concrete (Bool v); ty } ctx - | T.Char, ConstantValue (Char v) -> cf { V.value = V.Concrete (Char v); ty } ctx - | T.Str, ConstantValue (String v) -> cf { V.value = V.Concrete (String v); ty } ctx - | T.Integer int_ty, ConstantValue (V.Scalar v) -> - (* Check the type and the ranges *) - assert (int_ty = v.int_ty); - assert (check_scalar_value_in_range v); - cf { V.value = V.Concrete (V.Scalar v); ty } ctx - (* Constant expression identifier *) - | ty, ConstantId id -> - let dest = mk_fresh_symbolic_value V.FunCallRet (ety_no_regions_to_rty ty) in - - (* Call the continuation *) - let expr = cf (mk_typed_value_from_symbolic_value dest) ctx in - - (* TODO Should it really be a new call ID ? *) - let call = SA.Fun (LA.Regular id, C.fresh_fun_call_id ()) in - - S.synthesize_function_call call [] [] [] [] - dest None(*TODO meta-info*) expr - - (* Remaining cases (invalid) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, ConstantAdt _ | _, ConstantValue _ -> - failwith "Improperly typed constant value" +(** Convert a constant operand value to a typed value *) +let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_value = + (* Check the type while converting - + * we actually need some information contained in the type *) + match (ty, cv) with + (* Scalar, boolean... *) + | T.Bool, (Bool v) -> { V.value = V.Concrete (Bool v); ty } + | T.Char, (Char v) -> { V.value = V.Concrete (Char v); ty } + | T.Str, (String v) -> { V.value = V.Concrete (String v); ty } + | T.Integer int_ty, (V.Scalar v) -> + (* Check the type and the ranges *) + assert (int_ty = v.int_ty); + assert (check_scalar_value_in_range v); + { V.value = V.Concrete (V.Scalar v); ty } + (* Remaining cases (invalid) - listing as much as we can on purpose + (allows to catch errors at compilation if the definitions change) *) + | _, _ -> failwith "Improperly typed constant value" (** Prepare the evaluation of an operand. @@ -172,7 +127,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand) fun ctx -> match op with | Expressions.Constant (ty, cv) -> - eval_operand_constant_value ty cv cf ctx + cf (typecheck_constant_value ty cv) ctx | Expressions.Copy p -> (* Access the value *) let access = Read in @@ -205,7 +160,7 @@ let eval_operand (config : C.config) (op : E.operand) ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | Expressions.Constant (ty, cv) -> eval_operand_constant_value ty cv cf ctx + | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx | Expressions.Copy p -> (* Access the value *) let access = Read in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c7308720..e5564d59 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -7,7 +7,6 @@ module A = LlbcAst module L = Logging open TypesUtils open ValuesUtils -open FunIdentifier module Inv = Invariants module S = SynthesizeSymbolic open Errors @@ -822,6 +821,15 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx + | A.AssignGlobal { dst; global } -> + let call : A.call = { + func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global); + region_args = []; + type_args = []; + args = []; + dest = { var_id = dst; projection = [] }; + } in + eval_function_call config call cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare = prepare_rplace config expand_prim_copy Read p in @@ -1002,7 +1010,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = call.args call.dest (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) -and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1080,7 +1088,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -1301,7 +1309,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) -and eval_local_function_call (config : C.config) (fid : FunDeclId.id) +and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id) (region_args : T.erased_region list) (type_args : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = match config.mode with diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 7a2e22f7..47323cc2 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -33,8 +33,6 @@ let typed_value_to_string = PA.typed_value_to_string let typed_avalue_to_string = PA.typed_avalue_to_string -let operand_constant_value_to_string = PA.operand_constant_value_to_string - let place_to_string = PA.place_to_string let operand_to_string = PA.operand_to_string diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index 4324586d..16733e20 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -2,7 +2,21 @@ open Names open Types open Values open Expressions -open FunIdentifier +open Identifiers + +module FunDeclId = IdGen () +module GlobalDeclId = IdGen () + +(* Strict type for the number of function declarations (see [global_to_fun_id] below) *) +type global_id_converter = { fun_count : int } +[@@deriving show] + +(** Converts a global id to its corresponding function id. + To do so, it adds the global id to the number of function declarations : + We have the bijection `global_id <=> fun_id + fun_id_count`. +*) +let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id = + FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count) type var = { index : VarId.id; (** Unique variable identifier *) @@ -34,6 +48,12 @@ type assumed_fun_id = type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id [@@deriving show, ord] +type assign_global = { + dst : VarId.id; + global : GlobalDeclId.id; +} +[@@deriving show] + type assertion = { cond : operand; expected : bool } [@@deriving show] type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group @@ -75,6 +95,8 @@ class ['self] iter_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter + method visit_assign_global : 'env -> assign_global -> unit = fun _ _ -> () + method visit_place : 'env -> place -> unit = fun _ _ -> () method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> () @@ -97,6 +119,8 @@ class ['self] map_statement_base = object (_self : 'self) inherit [_] VisitorsRuntime.map + method visit_assign_global : 'env -> assign_global -> assign_global = fun _ x -> x + method visit_place : 'env -> place -> place = fun _ x -> x method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x @@ -118,6 +142,7 @@ class ['self] map_statement_base = type statement = | Assign of place * rvalue + | AssignGlobal of assign_global | FakeRead of place | SetDiscriminant of place * VariantId.id | Drop of place diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml index bc4236cf..84e8e00f 100644 --- a/src/LlbcAstUtils.ml +++ b/src/LlbcAstUtils.ml @@ -1,6 +1,5 @@ open LlbcAst open Utils -open FunIdentifier module T = Types (** Check if a [statement] contains loops *) diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 14333088..a074ed1e 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -11,7 +11,6 @@ open Yojson.Basic open Names open OfJsonBasic -open FunIdentifier module T = Types module V = Values module S = Scalars @@ -19,6 +18,7 @@ module M = Modules module E = Expressions module A = LlbcAst module TU = TypesUtils +module AU = LlbcAstUtils (* The default logger *) let log = Logging.llbc_of_json_logger @@ -227,14 +227,6 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result = } | _ -> Error "") -(* Converts a global ID to its corresponding function ID. - To do so, it adds the global ID to the number of function declarations. -*) -let global_id_of_json (js: json) (fun_count: int) : (FunDeclId.id, string) result = - combine_error_msgs js "global_id_of_json" - (let* gid = FunDeclId.id_of_json js in - Ok (FunDeclId.of_int ((FunDeclId.to_int gid) + fun_count))) - let var_of_json (js : json) : (A.var, string) result = combine_error_msgs js "var_of_json" (match js with @@ -308,23 +300,6 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result = raise (Failure ("Scalar value not in range: " ^ V.show_scalar_value sv))); res -let constant_value_of_json (js : json) : (V.constant_value, string) result = - combine_error_msgs js "constant_value_of_json" - (match js 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 "") - let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result = combine_error_msgs js "field_proj_kind_of_json" (match js with @@ -403,25 +378,30 @@ let binop_of_json (js : json) : (E.binop, string) result = | `String "Shr" -> Ok E.Shr | _ -> Error ("binop_of_json failed on:" ^ show js) -let rec operand_constant_value_of_json (js : json) (fun_count : int) : - (E.operand_constant_value, string) result = - combine_error_msgs js "operand_constant_value_of_json" +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 ]) ] -> - let* cv = constant_value_of_json cv in - Ok (E.ConstantValue cv) - | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] -> - let* variant_id = option_of_json T.VariantId.id_of_json variant_id in - let* field_values = - list_of_json (fun js -> operand_constant_value_of_json js fun_count) field_values - in - Ok (E.ConstantAdt (variant_id, field_values)) - | `Assoc [ ("ConstantIdentifier", `List [gid]) ] -> - let* id = global_id_of_json gid fun_count in - Ok (E.ConstantId id) - | _ -> Error "") - -let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result = + (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 "") + | _ -> Error "") + +let operand_of_json (js : json) : (E.operand, string) result = combine_error_msgs js "operand_of_json" (match js with | `Assoc [ ("Copy", place) ] -> @@ -432,7 +412,7 @@ let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result = Ok (E.Move place) | `Assoc [ ("Const", `List [ ty; cv ]) ] -> let* ty = ety_of_json ty in - let* cv = operand_constant_value_of_json cv fun_count in + let* cv = constant_value_of_json cv in Ok (E.Constant (ty, cv)) | _ -> Error "") @@ -455,11 +435,11 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys)) | _ -> Error "") -let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result = +let rvalue_of_json (js : json) : (E.rvalue, string) result = combine_error_msgs js "rvalue_of_json" (match js with | `Assoc [ ("Use", op) ] -> - let* op = operand_of_json op fun_count in + let* op = operand_of_json op in Ok (E.Use op) | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] -> let* place = place_of_json place in @@ -467,19 +447,19 @@ let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result = Ok (E.Ref (place, borrow_kind)) | `Assoc [ ("UnaryOp", `List [ unop; op ]) ] -> let* unop = unop_of_json unop in - let* op = operand_of_json op fun_count in + let* op = operand_of_json op in Ok (E.UnaryOp (unop, op)) | `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] -> let* binop = binop_of_json binop in - let* op1 = operand_of_json op1 fun_count in - let* op2 = operand_of_json op2 fun_count in + let* op1 = operand_of_json op1 in + let* op2 = operand_of_json op2 in Ok (E.BinaryOp (binop, op1, op2)) | `Assoc [ ("Discriminant", place) ] -> let* place = place_of_json place in Ok (E.Discriminant place) | `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] -> let* aggregate_kind = aggregate_kind_of_json aggregate_kind in - let* ops = list_of_json (fun js -> operand_of_json js fun_count) ops in + let* ops = list_of_json operand_of_json ops in Ok (E.Aggregate (aggregate_kind, ops)) | _ -> Error "") @@ -502,18 +482,18 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result = combine_error_msgs js "fun_id_of_json" (match js with | `Assoc [ ("Regular", id) ] -> - let* id = FunDeclId.id_of_json id in + let* id = A.FunDeclId.id_of_json id in Ok (A.Regular id) | `Assoc [ ("Assumed", fid) ] -> let* fid = assumed_fun_id_of_json fid in Ok (A.Assumed fid) | _ -> Error "") -let assertion_of_json (js : json) (fun_count : int) : (A.assertion, string) result = +let assertion_of_json (js : json) : (A.assertion, string) result = combine_error_msgs js "assertion_of_json" (match js with | `Assoc [ ("cond", cond); ("expected", expected) ] -> - let* cond = operand_of_json cond fun_count in + let* cond = operand_of_json cond in let* expected = bool_of_json expected in Ok { A.cond; expected } | _ -> Error "") @@ -547,7 +527,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result = } | _ -> Error "") -let call_of_json (js : json) (fun_count : int) : (A.call, string) result = +let call_of_json (js : json) : (A.call, string) result = combine_error_msgs js "call_of_json" (match js with | `Assoc @@ -561,18 +541,22 @@ let call_of_json (js : json) (fun_count : int) : (A.call, string) result = let* func = fun_id_of_json func in let* region_args = list_of_json erased_region_of_json region_args in let* type_args = list_of_json ety_of_json type_args in - let* args = list_of_json (fun js -> operand_of_json js fun_count) args in + let* args = list_of_json operand_of_json args in let* dest = place_of_json dest in Ok { A.func; region_args; type_args; args; dest } | _ -> Error "") -let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) result = +let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result = combine_error_msgs js "statement_of_json" (match js with | `Assoc [ ("Assign", `List [ place; rvalue ]) ] -> let* place = place_of_json place in - let* rvalue = rvalue_of_json rvalue fun_count in + let* rvalue = rvalue_of_json rvalue in Ok (A.Assign (place, rvalue)) + | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] -> + let* dst = V.VarId.id_of_json dst in + let* global = A.GlobalDeclId.id_of_json global in + Ok (A.AssignGlobal { dst; global }) | `Assoc [ ("FakeRead", place) ] -> let* place = place_of_json place in Ok (A.FakeRead place) @@ -584,10 +568,10 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) let* place = place_of_json place in Ok (A.Drop place) | `Assoc [ ("Assert", assertion) ] -> - let* assertion = assertion_of_json assertion fun_count in + let* assertion = assertion_of_json assertion in Ok (A.Assert assertion) | `Assoc [ ("Call", call) ] -> - let* call = call_of_json call fun_count in + let* call = call_of_json call in Ok (A.Call call) | `String "Panic" -> Ok A.Panic | `String "Return" -> Ok A.Return @@ -599,48 +583,48 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) Ok (A.Continue i) | `String "Nop" -> Ok A.Nop | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 fun_count in - let* st2 = statement_of_json st2 fun_count in + let* st1 = statement_of_json st1 gid_conv in + let* st2 = statement_of_json st2 gid_conv in Ok (A.Sequence (st1, st2)) | `Assoc [ ("Switch", `List [ op; tgt ]) ] -> - let* op = operand_of_json op fun_count in - let* tgt = switch_targets_of_json tgt fun_count in + let* op = operand_of_json op in + let* tgt = switch_targets_of_json tgt gid_conv in Ok (A.Switch (op, tgt)) | `Assoc [ ("Loop", st) ] -> - let* st = statement_of_json st fun_count in + let* st = statement_of_json st gid_conv in Ok (A.Loop st) | _ -> Error "") -and switch_targets_of_json (js : json) (fun_count : int) : (A.switch_targets, string) result = +and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result = combine_error_msgs js "switch_targets_of_json" (match js with | `Assoc [ ("If", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 fun_count in - let* st2 = statement_of_json st2 fun_count in + let* st1 = statement_of_json st1 gid_conv in + let* st2 = statement_of_json st2 gid_conv in Ok (A.If (st1, st2)) | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = list_of_json (pair_of_json (list_of_json scalar_value_of_json) - (fun js -> statement_of_json js fun_count)) + (fun js -> statement_of_json js gid_conv)) tgts in - let* otherwise = statement_of_json otherwise fun_count in + let* otherwise = statement_of_json otherwise gid_conv in Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") -let fun_body_of_json (js : json) (fun_count : int) : (A.fun_body, string) result = +let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result = combine_error_msgs js "fun_body_of_json" (match js with | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] -> let* arg_count = int_of_json arg_count in let* locals = list_of_json var_of_json locals in - let* body = statement_of_json body fun_count in + let* body = statement_of_json body gid_conv in Ok { A.arg_count; locals; body } | _ -> Error "") -let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result = +let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = combine_error_msgs js "fun_decl_of_json" (match js with | `Assoc @@ -650,20 +634,16 @@ let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result ("signature", signature); ("body", body); ] -> - let* def_id = FunDeclId.id_of_json def_id in + let* def_id = A.FunDeclId.id_of_json def_id in let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in - let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in + let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in Ok { A.def_id; name; signature; body; is_global = false; } | _ -> Error "") - (* Converts a global declaration to a function declaration. - -A.fun_sig -ety_no_regions_to_rty -*) -let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) result = + *) +let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = combine_error_msgs js "global_decl_of_json" (match js with | `Assoc @@ -673,10 +653,11 @@ let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) resu ("type_", type_); ("body", body); ] -> - let* def_id = global_id_of_json def_id fun_count in + 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* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in + let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in let signature : A.fun_sig = { region_params = []; num_early_bound_regions = 0; @@ -708,14 +689,17 @@ let type_declaration_group_of_json (js : json) : let fun_declaration_group_of_json (js : json) : (M.fun_declaration_group, string) result = combine_error_msgs js "fun_declaration_group_of_json" - (g_declaration_group_of_json FunDeclId.id_of_json js) + (g_declaration_group_of_json A.FunDeclId.id_of_json js) -let global_declaration_group_of_json (js : json) (fun_count: int) : +let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.fun_declaration_group, string) result = combine_error_msgs js "global_declaration_group_of_json" - (g_declaration_group_of_json (fun js -> global_id_of_json js fun_count) js) + (g_declaration_group_of_json (fun js -> + let* id = A.GlobalDeclId.id_of_json js in + Ok (A.global_to_fun_id gid_conv id) + ) js) -let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result +let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with @@ -726,7 +710,7 @@ let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_grou 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 fun_count in + let* decl = global_declaration_group_of_json decl gid_conv in Ok (M.Fun decl) | _ -> Error "") @@ -748,12 +732,19 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("globals", globals); ] -> let* fun_count = length_of_json_list functions in + let gid_conv = { A.fun_count = fun_count } in let* name = string_of_json name in let* declarations = - list_of_json (fun js -> declaration_group_of_json js fun_count) 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* functions = list_of_json (fun js -> fun_decl_of_json js fun_count) functions in - let* globals = list_of_json (fun js -> global_decl_of_json js fun_count) globals in - Ok { M.name; declarations; types; functions = functions @ globals } + let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in + let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in + Ok { + M.name; + declarations; + types; + functions = functions @ globals; + gid_conv; + } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index 6d0cf70c..b0e8878d 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,6 +1,5 @@ open Types open LlbcAst -open FunIdentifier type 'id g_declaration_group = NonRec of 'id | Rec of 'id list [@@deriving show] @@ -21,6 +20,7 @@ type llbc_module = { declarations : declaration_group list; types : type_decl list; functions : fun_decl list; + gid_conv : global_id_converter; } (** LLBC module - TODO: rename to crate *) diff --git a/src/Print.ml b/src/Print.ml index 9e2ff3cd..722f76ce 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1,5 +1,4 @@ open Names -open FunIdentifier module T = Types module TU = TypesUtils module V = Values @@ -686,7 +685,8 @@ module LlbcAst = struct var_id_to_string : V.VarId.id -> string; adt_field_names : T.TypeDeclId.id -> T.VariantId.id option -> string list option; - fun_decl_id_to_string : FunDeclId.id -> string; + fun_decl_id_to_string : A.FunDeclId.id -> string; + global_decl_id_to_string : A.GlobalDeclId.id -> string; } let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter = @@ -743,6 +743,9 @@ module LlbcAst = struct let def = C.ctx_lookup_fun_decl ctx def_id 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 ctx.fun_context.gid_conv def_id) + in { rvar_to_string = ctx_fmt.PV.rvar_to_string; r_to_string = ctx_fmt.PV.r_to_string; @@ -753,10 +756,14 @@ module LlbcAst = struct adt_field_names = ctx_fmt.PV.adt_field_names; adt_field_to_string; fun_decl_id_to_string; + global_decl_id_to_string; } - let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t) - (fun_decls : A.fun_decl FunDeclId.Map.t) (fdef : A.fun_decl) : + let fun_decl_to_ast_formatter + (type_decls : T.type_decl T.TypeDeclId.Map.t) + (fun_decls : A.fun_decl A.FunDeclId.Map.t) + (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (fdef : A.fun_decl) : ast_formatter = let rvar_to_string r = let rvar = T.RegionVarId.nth fdef.signature.region_params r in @@ -782,9 +789,12 @@ module LlbcAst = struct let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in let fun_decl_id_to_string def_id = - let def = FunDeclId.Map.find def_id fun_decls in + 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 (global_to_fun_id def_id) + in { rvar_to_string; r_to_string; @@ -795,6 +805,7 @@ module LlbcAst = struct adt_field_names; adt_field_to_string; fun_decl_id_to_string; + global_decl_id_to_string; } let rec projection_to_string (fmt : ast_formatter) (inside : string) @@ -860,36 +871,13 @@ module LlbcAst = struct | E.Shl -> "<<" | E.Shr -> ">>" - let rec operand_constant_value_to_string (fmt : ast_formatter) - (cv : E.operand_constant_value) : string = - match cv with - | E.ConstantId id -> fmt.fun_decl_id_to_string id - | E.ConstantValue cv -> PV.constant_value_to_string cv - | E.ConstantAdt (variant_id, field_values) -> - (* This is a bit annoying, because we don't have context information - * to convert the ADT to a value, so we do the best we can in the - * simplest manner. Anyway, those printing utilitites are only used - * for debugging, and complex constant values are not common. - * We might want to store type information in the operand constant values - * in the future. - *) - let variant_id = option_to_string T.VariantId.to_string variant_id in - let field_values = - List.map (operand_constant_value_to_string fmt) field_values - in - "ConstantAdt " ^ variant_id ^ " {" - ^ String.concat ", " field_values - ^ "}" - let operand_to_string (fmt : ast_formatter) (op : E.operand) : string = match op with | E.Copy p -> "copy " ^ place_to_string fmt p | E.Move p -> "move " ^ place_to_string fmt p | E.Constant (ty, cv) -> - (* For clarity, we also print the typing information: see the comment in - * [operand_constant_value_to_string] *) "(" - ^ operand_constant_value_to_string fmt cv + ^ PV.constant_value_to_string cv ^ " : " ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty ^ ")" @@ -950,6 +938,8 @@ module LlbcAst = struct match st with | A.Assign (p, rv) -> indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv + | A.AssignGlobal { dst; global } -> + indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global | A.FakeRead p -> "fake_read " ^ place_to_string fmt p | A.SetDiscriminant (p, variant_id) -> (* TODO: improve this to lookup the variant name by using the def id *) @@ -1139,8 +1129,11 @@ module Module = struct (** Generate an [ast_formatter] by using a definition context in combination with the variables local to a function's definition *) - let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t) - (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : + let def_ctx_to_ast_formatter + (type_context : T.type_decl T.TypeDeclId.Map.t) + (fun_context : A.fun_decl A.FunDeclId.Map.t) + (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (def : A.fun_decl) : PA.ast_formatter = let rvar_to_string vid = let var = T.RegionVarId.nth def.signature.region_params vid in @@ -1159,9 +1152,12 @@ module Module = struct name_to_string def.name in let fun_decl_id_to_string def_id = - let def = FunDeclId.Map.find def_id fun_context in + let def = A.FunDeclId.Map.find def_id fun_context in fun_name_to_string def.name in + let global_decl_id_to_string def_id = + fun_decl_id_to_string (global_to_fun_id def_id) + in let var_id_to_string vid = let var = V.VarId.nth (Option.get def.body).locals vid in PA.var_to_string var @@ -1183,13 +1179,17 @@ module Module = struct var_id_to_string; adt_field_names; fun_decl_id_to_string; + global_decl_id_to_string; } (** This function pretty-prints a function definition by using a definition context *) - let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) - (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : string = - let fmt = def_ctx_to_ast_formatter type_context fun_context def in + let fun_decl_to_string + (type_context : T.type_decl T.TypeDeclId.Map.t) + (fun_context : A.fun_decl A.FunDeclId.Map.t) + (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (def : A.fun_decl) : string = + let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in PA.fun_decl_to_string fmt "" " " def let module_to_string (m : M.llbc_module) : string = @@ -1200,7 +1200,8 @@ module Module = struct (* The functions *) let fun_decls = - List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions + let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in + List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions in (* Put everything together *) @@ -1257,11 +1258,6 @@ module EvalCtxLlbcAst = struct let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.typed_avalue_to_string fmt v - let operand_constant_value_to_string (ctx : C.eval_ctx) - (cv : E.operand_constant_value) : string = - let fmt = PA.eval_ctx_to_ast_formatter ctx in - PA.operand_constant_value_to_string fmt cv - let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.place_to_string fmt op diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 8864dafe..ea9bf2ab 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -2,7 +2,6 @@ open Pure open PureUtils -open FunIdentifier module T = Types module V = Values module E = Expressions @@ -44,7 +43,7 @@ type ast_formatter = { adt_field_to_string : 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 : FunDeclId.id -> string; + fun_decl_id_to_string : A.FunDeclId.id -> string; } let ast_to_value_formatter (fmt : ast_formatter) : value_formatter = @@ -86,7 +85,7 @@ 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 FunDeclId.Map.t) (type_params : type_var list) : + (fun_decls : A.fun_decl A.FunDeclId.Map.t) (type_params : type_var list) : ast_formatter = let type_var_id_to_string vid = let var = T.TypeVarId.nth type_params vid in @@ -110,7 +109,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls in let fun_decl_id_to_string def_id = - let def = FunDeclId.Map.find def_id fun_decls in + let def = A.FunDeclId.Map.find def_id fun_decls in fun_name_to_string def.name in { diff --git a/src/Pure.ml b/src/Pure.ml index 256a872a..42f56fed 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -1,6 +1,5 @@ open Identifiers open Names -open FunIdentifier module T = Types module V = Values module E = Expressions @@ -567,7 +566,7 @@ type fun_body = { } type fun_decl = { - def_id : FunDeclId.id; + def_id : A.FunDeclId.id; back_id : T.RegionGroupId.id option; basename : fun_name; (** The "base" name of the function. diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 55a8853a..195eb879 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -6,7 +6,6 @@ open Pure open TranslateCore -open FunIdentifier module C = Contexts module RegionVarId = T.RegionVarId module F = Format @@ -93,7 +92,7 @@ type formatter = { (`None` if forward function) TODO: use the fun id for the assumed functions. *) - decreases_clause_name : FunDeclId.id -> fun_name -> string; + decreases_clause_name : A.FunDeclId.id -> fun_name -> string; (** Generates the name of the definition used to prove/reason about termination. The generated code uses this clause where needed, but its body must be defined by the user. @@ -357,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Regular fid -> - Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name + Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name | A.Assumed aid -> A.show_assumed_fun_id aid in let fun_kind = @@ -370,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let fun_name = match fid with | A.Regular fid -> - Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name + Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name | A.Assumed aid -> A.show_assumed_fun_id aid in "decreases clause for function: " ^ fun_name @@ -445,7 +444,7 @@ 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 : 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 @@ -476,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id) (ctx : extraction_ctx) : string = ctx_get (VariantId (def_id, variant_id)) ctx -let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) : +let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (ctx : extraction_ctx) : string = ctx_get (DecreasesClauseId (A.Regular def_id)) ctx @@ -574,7 +573,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (* Lookup the LLBC def to compute the region group information *) let def_id = def.def_id in let llbc_def = - FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls + A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls in let sg = llbc_def.signature in let num_rgs = List.length sg.regions_hierarchy in diff --git a/src/Substitute.ml b/src/Substitute.ml index 711e438b..4b0a04ca 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -210,12 +210,6 @@ let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place (* There is nothing to do *) p -(** Apply a type substitution to an operand constant value *) -let operand_constant_value_substitute (_tsubst : T.TypeVarId.id -> T.ety) - (op : E.operand_constant_value) : E.operand_constant_value = - (* There is nothing to do *) - op - (** Apply a type substitution to an operand *) let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) : E.operand = @@ -225,9 +219,7 @@ let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) : | E.Move p -> E.Move (p_subst p) | E.Constant (ety, cv) -> let rsubst x = x in - E.Constant - ( ty_substitute rsubst tsubst ety, - operand_constant_value_substitute tsubst cv ) + E.Constant ( ty_substitute rsubst tsubst ety, cv ) (** Apply a type substitution to an rvalue *) let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) : @@ -289,6 +281,7 @@ let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety) let p = place_substitute tsubst p in let rvalue = rvalue_substitute tsubst rvalue in A.Assign (p, rvalue) + | A.AssignGlobal g -> A.AssignGlobal g | A.FakeRead p -> let p = place_substitute tsubst p in A.FakeRead p diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 2b416cc1..927684bc 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -2,7 +2,6 @@ open Errors open LlbcAstUtils open Pure open PureUtils -open FunIdentifier module Id = Identifiers module M = Modules module S = SymbolicAst @@ -68,9 +67,10 @@ type fun_sig_named_outputs = { } type fun_context = { - llbc_fun_decls : A.fun_decl FunDeclId.Map.t; + llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *) - fun_infos : FA.fun_info FunDeclId.Map.t; + fun_infos : FA.fun_info A.FunDeclId.Map.t; + gid_conv : A.global_id_converter; } type call_info = { @@ -134,8 +134,11 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = (* TODO: move *) let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter = - Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls - ctx.fun_context.llbc_fun_decls ctx.fun_decl + Print.LlbcAst.fun_decl_to_ast_formatter + ctx.type_context.llbc_type_decls + ctx.fun_context.llbc_fun_decls + (A.global_to_fun_id ctx.fun_context.gid_conv) + ctx.fun_decl let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter = let type_params = ctx.fun_decl.signature.type_params in @@ -196,12 +199,12 @@ let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl = TypeDeclId.Map.find id ctx.type_context.llbc_type_decls -let bs_ctx_lookup_llbc_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl +let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl = - FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls + A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls (* TODO: move *) -let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id) +let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id) (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig = let id = (A.Regular def_id, back_id) in (RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg @@ -472,11 +475,11 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids (** Small utility. *) -let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t) +let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info = match fun_id with | A.Regular fid -> - let info = FunDeclId.Map.find fid fun_infos in + 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 } @@ -494,7 +497,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t) name (outputs for backward functions come from borrows in the inputs of the forward function). *) -let translate_fun_sig (fun_infos : FA.fun_info FunDeclId.Map.t) +let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t) (fun_id : A.fun_id) (types_infos : TA.type_infos) (sg : A.fun_sig) (input_names : string option list) (bid : T.RegionGroupId.id option) : fun_sig_named_outputs = @@ -1744,7 +1747,7 @@ let translate_type_decls (type_decls : T.type_decl list) : type_decl list = - optional names for the outputs values (we derive them for the backward functions) *) -let translate_fun_signatures (fun_infos : FA.fun_info FunDeclId.Map.t) +let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t) (types_infos : TA.type_infos) (functions : (A.fun_id * string option list * A.fun_sig) list) : fun_sig_named_outputs RegularFunIdMap.t = diff --git a/src/Translate.ml b/src/Translate.ml index 1577753c..d4d79355 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -1,6 +1,5 @@ open InterpreterStatements open Interpreter -open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -65,7 +64,10 @@ let translate_function_to_symbolics (config : C.partial_config) ^ Print.fun_name_to_string fdef.A.name)); let { type_context; fun_context } = trans_ctx in - let fun_context = { C.fun_decls = fun_context.fun_decls } in + let fun_context = { + C.fun_decls = fun_context.fun_decls; + C.gid_conv = fun_context.gid_conv; + } in match fdef.body with | None -> None @@ -100,7 +102,8 @@ let translate_function_to_symbolics (config : C.partial_config) let translate_function_to_pure (config : C.partial_config) (mp_config : Micro.config) (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) - (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) + (fdef : A.fun_decl) : pure_fun_translation = (* Debug *) log#ldebug @@ -139,6 +142,7 @@ let translate_function_to_pure (config : C.partial_config) SymbolicToPure.llbc_fun_decls = fun_context.fun_decls; fun_sigs; fun_infos = fun_context.fun_infos; + gid_conv = fun_context.gid_conv; } in let ctx = @@ -291,7 +295,11 @@ let translate_module_to_pure (config : C.partial_config) (* Compute the type and function contexts *) let type_context, fun_context = compute_type_fun_contexts m in let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in - let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in + let fun_context = { + fun_decls = fun_context.fun_decls; + fun_infos; + gid_conv = m.gid_conv; + } in let trans_ctx = { type_context; fun_context } in (* Translate all the type definitions *) @@ -352,8 +360,8 @@ type gen_ctx = { m : M.llbc_module; extract_ctx : PureToExtract.extraction_ctx; trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; - trans_funs : (bool * pure_fun_translation) FunDeclId.Map.t; - functions_with_decreases_clause : FunDeclId.Set.t; + trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t; + functions_with_decreases_clause : A.FunDeclId.Set.t; } (** Extraction context *) @@ -389,7 +397,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = ctx.trans_types in let has_opaque_funs = - FunDeclId.Map.exists + A.FunDeclId.Map.exists (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) -> Option.is_none t_fwd.body) ctx.trans_funs @@ -428,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = - FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause + A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause in (* In case of (non-mutually) recursive functions, we use a simple procedure to @@ -524,14 +532,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ids | Fun (NonRec id) -> (* Lookup *) - let pure_fun = FunDeclId.Map.find id ctx.trans_funs in + let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in (* Translate *) export_functions false [ pure_fun ] | Fun (Rec ids) -> (* General case of mutually recursive functions *) (* Lookup *) let pure_funs = - List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids + List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids in (* Translate *) export_functions true pure_funs @@ -623,7 +631,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) let rec_functions = - FunDeclId.Set.of_list + A.FunDeclId.Set.of_list (List.concat (List.map (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> []) @@ -645,7 +653,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (fun ctx (keep_fwd, def) -> (* Note that we generate a decrease clause for all the recursive functions *) let gen_decr_clause = - FunDeclId.Set.mem (fst def).Pure.def_id rec_functions + A.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions in ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause def) @@ -675,7 +683,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types) in let trans_funs = - FunDeclId.Map.of_list + A.FunDeclId.Map.of_list (List.map (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) -> (fd.def_id, (keep_fwd, (fd, bdl)))) @@ -762,7 +770,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the template clauses *) let needs_clauses_module = config.extract_decreases_clauses - && not (FunDeclId.Set.is_empty rec_functions) + && not (A.FunDeclId.Set.is_empty rec_functions) in (if needs_clauses_module && config.extract_template_decreases_clauses then let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 3d3887ce..ccaa9e22 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -1,7 +1,6 @@ (** Some utilities for the translation *) open InterpreterStatements -open FunIdentifier module L = Logging module T = Types module A = LlbcAst @@ -15,8 +14,9 @@ let log = L.translate_log type type_context = C.type_context [@@deriving show] type fun_context = { - fun_decls : A.fun_decl FunDeclId.Map.t; - fun_infos : FA.fun_info FunDeclId.Map.t; + fun_decls : A.fun_decl A.FunDeclId.Map.t; + fun_infos : FA.fun_info A.FunDeclId.Map.t; + gid_conv : A.global_id_converter; } [@@deriving show] @@ -50,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string = let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in PrintPure.fun_decl_to_string fmt def -let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string = +let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string = Print.fun_name_to_string - (FunDeclId.Map.find id ctx.fun_context.fun_decls).name + (A.FunDeclId.Map.find id ctx.fun_context.fun_decls).name diff --git a/src/main.ml b/src/main.ml index 6b1083f5..93b094fd 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.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; + 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; (* 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 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 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 'src/Modules.ml') 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 f9b324be57708e9496ca6e9ac0b7e68ffd9e7108 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 18 Jul 2022 16:27:00 +0200 Subject: Address much stuff of the PR, throw exceptions at remaining places --- src/Contexts.ml | 11 +++++-- src/ExtractToFStar.ml | 11 +++++-- src/FunsAnalysis.ml | 6 ++-- src/Interpreter.ml | 44 +++++++++++++++----------- src/InterpreterStatements.ml | 3 +- src/LlbcAst.ml | 21 ++++++------- src/LlbcOfJson.ml | 73 +++++++++++++++++++++++++++----------------- src/Modules.ml | 11 +++++-- src/Names.ml | 2 ++ src/Print.ml | 23 ++++++++------ src/PrintPure.ml | 9 ++++-- src/Pure.ml | 2 +- src/PureToExtract.ml | 7 +++-- src/SymbolicToPure.ml | 23 ++++++++------ src/Translate.ml | 21 +++++++------ src/TranslateCore.ml | 17 +++++++---- 16 files changed, 172 insertions(+), 112 deletions(-) (limited to 'src/Modules.ml') diff --git a/src/Contexts.ml b/src/Contexts.ml index 1fbc916b..4f1e1506 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -219,13 +219,18 @@ type type_context = { type fun_context = { fun_decls : fun_decl FunDeclId.Map.t; - gid_conv : global_id_converter; +} +[@@deriving show] + +type global_context = { + global_decls : global_decl GlobalDeclId.Map.t; } [@@deriving show] type eval_ctx = { type_context : type_context; fun_context : fun_context; + global_context : global_context; type_vars : type_var list; env : env; ended_regions : RegionId.Set.t; @@ -260,8 +265,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl = FunDeclId.Map.find fid ctx.fun_context.fun_decls (** TODO: make this more efficient with maps *) -let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl = - ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid) +let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl = + GlobalDeclId.Map.find gid ctx.global_context.global_decls (** Retrieve a variable's value in an environment *) let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 5b39b0b7..2c53e45b 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -907,9 +907,12 @@ 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 + *) | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> @@ -1485,7 +1488,7 @@ let global_decl_to_body_name (decl : string) : string = 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 *) +(** 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) (qualif : fun_decl_qualif) (name : string) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) @@ -1550,8 +1553,11 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) 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); + 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); @@ -1578,6 +1584,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) 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 b1b8ccc2..034575c0 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -61,7 +61,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) * (we check that it is successful in the extracted code: if it is * not, it leads to a type-checking error in the generated files) *) - if f.is_global then () else + if f.is_global_body then () else can_fail := !can_fail || b method! visit_Assert env a = @@ -98,7 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) super#visit_Loop env loop end in - assert (not f.is_global || not use_state); + assert (not f.is_global_body || not use_state); (match f.body with | None -> (* Opaque function *) @@ -108,7 +108,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) (* We ignore on purpose functions that cannot fail: the result of the analysis * is not used yet to adjust the translation so that the functions which * syntactically can't fail don't use an error monad. *) - can_fail := not f.is_global + can_fail := not f.is_global_body in List.iter visit_fun d; { can_fail = !can_fail; stateful = !stateful; divergent = !divergent } diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f4f01ff8..3610d486 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -14,9 +14,9 @@ module SA = SymbolicAst let log = L.interpreter_log let compute_type_fun_contexts (m : M.llbc_module) : - C.type_context * C.fun_context = + C.type_context * C.fun_context * C.global_context = let type_decls_list, _ = M.split_declarations m.declarations in - let type_decls, fun_decls = M.compute_defs_maps m in + let type_decls, fun_decls, global_decls = M.compute_defs_maps m in let type_decls_groups, _funs_defs_groups = M.split_declarations_to_group_maps m.declarations in @@ -24,15 +24,20 @@ let compute_type_fun_contexts (m : M.llbc_module) : TypesAnalysis.analyze_type_declarations type_decls type_decls_list in let type_context = { C.type_decls_groups; type_decls; type_infos } in - let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in - (type_context, fun_context) - -let initialize_eval_context (type_context : C.type_context) - (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx = + let fun_context = { C.fun_decls } in + let global_context = { C.global_decls } in + (type_context, fun_context, global_context) + +let initialize_eval_context + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (type_vars : T.type_var list) : C.eval_ctx = C.reset_global_counters (); { C.type_context; C.fun_context; + C.global_context; C.type_vars; C.env = [ C.Frame ]; C.ended_regions = T.RegionId.Set.empty; @@ -51,8 +56,11 @@ let initialize_eval_context (type_context : C.type_context) - the list of symbolic values introduced for the input values - the instantiated function signature *) -let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_context : C.fun_context) (fdef : A.fun_decl) : +let initialize_symbolic_context_for_fun + (type_context : C.type_context) + (fun_context : C.fun_context) + (global_context : C.global_context) + (fdef : A.fun_decl) : C.eval_ctx * V.symbolic_value list * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us @@ -67,7 +75,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context type_context fun_context sg.type_params in + let ctx = initialize_eval_context type_context fun_context global_context sg.type_params in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in let inst_sg = instantiate_fun_sig type_params sg in @@ -204,7 +212,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return - the symbolic AST generated by the symbolic execution *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) : V.symbolic_value list * SA.expression option = (* Debug *) @@ -218,7 +226,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (* Create the evaluation context *) let ctx, input_svs, inst_sg = - initialize_symbolic_context_for_fun type_context fun_context fdef + initialize_symbolic_context_for_fun type_context fun_context global_context fdef in (* Create the continuation to finish the evaluation *) @@ -285,8 +293,8 @@ module Test = struct assert (body.A.arg_count = 0); (* Create the evaluation context *) - let type_context, fun_context = compute_type_fun_contexts m in - let ctx = initialize_eval_context type_context fun_context [] in + let type_context, fun_context, global_context = compute_type_fun_contexts m in + let ctx = initialize_eval_context type_context fun_context global_context [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx body.A.locals in @@ -330,7 +338,7 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (type_context : C.type_context) (fun_context : C.fun_context) + (type_context : C.type_context) (fun_context : C.fun_context) (global_context : C.global_context) (fdef : A.fun_decl) : unit = (* Debug *) log#ldebug @@ -338,7 +346,7 @@ module Test = struct (* Evaluate *) let evaluate = - evaluate_function_symbolic config synthesize type_context fun_context fdef + evaluate_function_symbolic config synthesize type_context fun_context global_context fdef in (* Execute the forward function *) let _ = evaluate None in @@ -368,12 +376,12 @@ module Test = struct in (* Filter the opaque functions *) let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in - let type_context, fun_context = compute_type_fun_contexts m in + let type_context, fun_context, global_context = compute_type_fun_contexts m in let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize type_context fun_context def + test_function_symbolic config synthesize type_context fun_context global_context def in List.iter test_fun no_loop_funs end diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 8f981174..6a0b81f3 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -832,8 +832,9 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx | A.AssignGlobal { dst; global } -> + (* What codegen do we want ? *) let call : A.call = { - func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global); + func = A.Regular (failwith "TODO InterpretStatements.ml:837"); region_args = []; type_args = []; args = []; diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml index 16733e20..aa9b0665 100644 --- a/src/LlbcAst.ml +++ b/src/LlbcAst.ml @@ -7,17 +7,6 @@ open Identifiers module FunDeclId = IdGen () module GlobalDeclId = IdGen () -(* Strict type for the number of function declarations (see [global_to_fun_id] below) *) -type global_id_converter = { fun_count : int } -[@@deriving show] - -(** Converts a global id to its corresponding function id. - To do so, it adds the global id to the number of function declarations : - We have the bijection `global_id <=> fun_id + fun_id_count`. -*) -let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id = - FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count) - type var = { index : VarId.id; (** Unique variable identifier *) name : string option; @@ -201,6 +190,14 @@ type fun_decl = { name : fun_name; signature : fun_sig; body : fun_body option; - is_global : bool; + is_global_body : bool; +} +[@@deriving show] + +type global_decl = { + def_id : GlobalDeclId.id; + body_id: FunDeclId.id; + name : global_name; + ty: ety; } [@@deriving show] diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index c157b667..f51c15be 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -540,7 +540,7 @@ let call_of_json (js : json) : (A.call, string) result = Ok { A.func; region_args; type_args; args; dest } | _ -> Error "") -let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result = +let rec statement_of_json (js : json) : (A.statement, string) result = combine_error_msgs js "statement_of_json" (match js with | `Assoc [ ("Assign", `List [ place; rvalue ]) ] -> @@ -577,48 +577,49 @@ let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.st Ok (A.Continue i) | `String "Nop" -> Ok A.Nop | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 gid_conv in - let* st2 = statement_of_json st2 gid_conv in + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 in Ok (A.Sequence (st1, st2)) | `Assoc [ ("Switch", `List [ op; tgt ]) ] -> let* op = operand_of_json op in - let* tgt = switch_targets_of_json tgt gid_conv in + let* tgt = switch_targets_of_json tgt in Ok (A.Switch (op, tgt)) | `Assoc [ ("Loop", st) ] -> - let* st = statement_of_json st gid_conv in + let* st = statement_of_json st in Ok (A.Loop st) | _ -> Error "") -and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result = +and switch_targets_of_json (js : json) : (A.switch_targets, string) result = combine_error_msgs js "switch_targets_of_json" (match js with | `Assoc [ ("If", `List [ st1; st2 ]) ] -> - let* st1 = statement_of_json st1 gid_conv in - let* st2 = statement_of_json st2 gid_conv in + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 in Ok (A.If (st1, st2)) | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = - list_of_json (pair_of_json + list_of_json ( + pair_of_json (list_of_json scalar_value_of_json) - (fun js -> statement_of_json js gid_conv)) + statement_of_json) tgts in - let* otherwise = statement_of_json otherwise gid_conv in + let* otherwise = statement_of_json otherwise in Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") -let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result = +let fun_body_of_json (js : json) : (A.fun_body, string) result = combine_error_msgs js "fun_body_of_json" (match js with | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] -> let* arg_count = int_of_json arg_count in let* locals = list_of_json var_of_json locals in - let* body = statement_of_json body gid_conv in + let* body = statement_of_json body in Ok { A.arg_count; locals; body } | _ -> Error "") -let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = +let fun_decl_of_json (js : json) : (A.fun_decl, string) result = combine_error_msgs js "fun_decl_of_json" (match js with | `Assoc @@ -631,13 +632,24 @@ let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_dec let* def_id = A.FunDeclId.id_of_json def_id in let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in - let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in - Ok { A.def_id; name; signature; body; is_global = false; } + let* body = option_of_json fun_body_of_json body in + Ok { A.def_id; name; signature; body; is_global_body = false; } | _ -> Error "") +(* Strict type for the number of function declarations (see [global_to_fun_id] below) *) +type global_id_converter = { fun_count : int } +[@@deriving show] + +(** Converts a global id to its corresponding function id. + To do so, it adds the global id to the number of function declarations : + We have the bijection `global_id <=> fun_id + fun_id_count`. +*) +let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id = + A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count) + (* Converts a global declaration to a function declaration. *) -let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result = +let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result = combine_error_msgs js "global_decl_of_json" (match js with | `Assoc @@ -648,10 +660,10 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ ("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 fun_id = global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name 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* body = option_of_json fun_body_of_json body in let signature : A.fun_sig = { region_params = []; num_early_bound_regions = 0; @@ -660,7 +672,8 @@ let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_ inputs = []; output = TU.ety_no_regions_to_sty ty; } in - Ok { A.def_id; name; signature; body; is_global = true; } + Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; }, + { A.def_id = fun_id; name; signature; body; is_global_body = true; }) | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) @@ -685,15 +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) -let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : +(* 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 = 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 (A.global_to_fun_id gid_conv id) + Ok (global_to_fun_id gid_conv id) ) js) -let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result +let declaration_group_of_json (js : json) (gid_conv : global_id_converter) : (M.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with @@ -726,19 +742,20 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("globals", globals); ] -> let* fun_count = length_of_json_list functions in - let gid_conv = { A.fun_count = fun_count } 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* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions 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 globals, global_bodies = List.split globals in Ok { M.name; declarations; types; - functions = functions @ globals; - gid_conv; + functions = functions @ global_bodies; + globals; } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index 149de020..2f640636 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -21,12 +21,12 @@ type llbc_module = { declarations : declaration_group list; types : type_decl list; functions : fun_decl list; - gid_conv : global_id_converter; + globals : global_decl list; } (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t = + type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -37,7 +37,12 @@ let compute_defs_maps (m : llbc_module) : (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m) FunDeclId.Map.empty m.functions in - (types_map, funs_map) + let globals_map = + List.fold_left + (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m) + GlobalDeclId.Map.empty m.globals + in + (types_map, funs_map, globals_map) (** Split a module's declarations between types and functions *) let split_declarations (decls : declaration_group list) : diff --git a/src/Names.ml b/src/Names.ml index 1308eccc..0db5291a 100644 --- a/src/Names.ml +++ b/src/Names.ml @@ -54,6 +54,8 @@ type type_name = name [@@deriving show, ord] type fun_name = name [@@deriving show, ord] +type global_name = name [@@deriving show, ord] + (** Filter the disambiguators equal to 0 in a name *) let filter_disambiguators_zero (n : name) : name = let pred (pe : path_elem) : bool = diff --git a/src/Print.ml b/src/Print.ml index 337116ec..6b11a3ff 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -13,6 +13,7 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string = let name_to_string (name : name) : string = Names.name_to_string name let fun_name_to_string (name : fun_name) : string = name_to_string name +let global_name_to_string (name : global_name) : string = name_to_string name (** Pretty-printing for types *) module Types = struct @@ -744,7 +745,8 @@ module LlbcAst = struct 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 ctx.fun_context.gid_conv def_id) + let def = C.ctx_lookup_global_decl ctx def_id in + global_name_to_string def.name in { rvar_to_string = ctx_fmt.PV.rvar_to_string; @@ -762,7 +764,7 @@ module LlbcAst = struct let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t) (fun_decls : A.fun_decl A.FunDeclId.Map.t) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) : ast_formatter = let rvar_to_string r = @@ -793,7 +795,8 @@ module LlbcAst = struct fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (global_to_fun_id def_id) + let def = A.GlobalDeclId.Map.find def_id global_decls in + global_name_to_string def.name in { rvar_to_string; @@ -1132,7 +1135,7 @@ module Module = struct let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t) (fun_context : A.fun_decl A.FunDeclId.Map.t) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) : PA.ast_formatter = let rvar_to_string vid = @@ -1156,7 +1159,8 @@ module Module = struct fun_name_to_string def.name in let global_decl_id_to_string def_id = - fun_decl_id_to_string (global_to_fun_id def_id) + let def = A.GlobalDeclId.Map.find def_id global_context in + global_name_to_string def.name in let var_id_to_string vid = let var = V.VarId.nth (Option.get def.body).locals vid in @@ -1187,21 +1191,20 @@ module Module = struct let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t) (fun_context : A.fun_decl A.FunDeclId.Map.t) - (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id) + (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) : string = - let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in + let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in PA.fun_decl_to_string fmt "" " " def let module_to_string (m : M.llbc_module) : string = - let types_defs_map, funs_defs_map = M.compute_defs_maps m in + let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in (* The types *) let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in (* The functions *) let fun_decls = - let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in - List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions + List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions in (* Put everything together *) diff --git a/src/PrintPure.ml b/src/PrintPure.ml index c13f967f..597330bf 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -62,6 +62,7 @@ let ast_to_type_formatter (fmt : ast_formatter) : type_formatter = let name_to_string = Print.name_to_string let fun_name_to_string = Print.fun_name_to_string +let global_name_to_string = Print.global_name_to_string let option_to_string = Print.option_to_string let type_var_to_string = Print.Types.type_var_to_string let integer_type_to_string = Print.Types.integer_type_to_string @@ -85,9 +86,10 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t) functions (there is a difference between the forward/backward functions...) 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) +let mk_ast_formatter + (type_decls : T.type_decl TypeDeclId.Map.t) (fun_decls : A.fun_decl A.FunDeclId.Map.t) - (gid_conv : A.global_id_converter) + (global_decls : A.global_decl A.GlobalDeclId.Map.t) (type_params : type_var list) : ast_formatter = let type_var_id_to_string vid = @@ -116,7 +118,8 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t) 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) + let def = A.GlobalDeclId.Map.find def_id global_decls in + global_name_to_string def.name in { type_var_id_to_string; diff --git a/src/Pure.ml b/src/Pure.ml index b3be2040..5244b0bc 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -575,6 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; - is_global : bool; + is_global_body : bool; body : fun_body option; } diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index e58fec2a..7a10bb6b 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -83,14 +83,15 @@ 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) - pair: - do we generate the forward function (it may have been filtered)? - the number of extracted backward functions (not necessarily equal to the number of region groups, because we may have filtered some of them) - - region group information in case of a backward function - (`None` if forward function) TODO: use the fun id for the assumed functions. *) decreases_clause_name : A.FunDeclId.id -> fun_name -> string; @@ -599,7 +600,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 def.is_global num_rgs rg_info (keep_fwd, num_backs) + ctx.fmt.fun_name def_id def.basename def.is_global_body 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 diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a057b015..7d9e2906 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -70,7 +70,10 @@ type fun_context = { llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *) fun_infos : FA.fun_info A.FunDeclId.Map.t; - gid_conv : A.global_id_converter; +} + +type global_context = { + llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t; } type call_info = { @@ -96,6 +99,7 @@ type call_info = { type bs_ctx = { type_context : type_context; fun_context : fun_context; + global_context : global_context; fun_decl : A.fun_decl; bid : T.RegionGroupId.id option; (** TODO: rename *) sg : fun_sig; @@ -137,15 +141,15 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter = Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls ctx.fun_context.llbc_fun_decls - (A.global_to_fun_id ctx.fun_context.gid_conv) + ctx.global_context.llbc_global_decls ctx.fun_decl 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 - let gid_conv = ctx.fun_context.gid_conv in - PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params + let global_decls = ctx.global_context.llbc_global_decls in + PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in @@ -166,16 +170,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 gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.llbc_global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls 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 gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.llbc_global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_decl_to_string fmt def (* TODO: move *) @@ -1666,7 +1670,6 @@ 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 @@ -1727,7 +1730,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; is_global; body } in + let def = { def_id; back_id = bid; basename; signature; is_global_body = def.is_global_body; body } in (* Debugging *) log#ldebug (lazy diff --git a/src/Translate.ml b/src/Translate.ml index 9412b8b8..a6477e7f 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -63,10 +63,9 @@ let translate_function_to_symbolics (config : C.partial_config) ("translate_function_to_symbolics: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context } = trans_ctx in + let { type_context; fun_context; global_context } = trans_ctx in let fun_context = { C.fun_decls = fun_context.fun_decls; - C.gid_conv = fun_context.gid_conv; } in match fdef.body with @@ -76,7 +75,8 @@ let translate_function_to_symbolics (config : C.partial_config) let synthesize = true in let evaluate gid = let inputs, symb = - evaluate_function_symbolic config synthesize type_context fun_context + evaluate_function_symbolic config synthesize + type_context fun_context global_context fdef gid in (inputs, Option.get symb) @@ -110,7 +110,7 @@ let translate_function_to_pure (config : C.partial_config) (lazy ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name)); - let { type_context; fun_context } = trans_ctx in + let { type_context; fun_context; global_context } = trans_ctx in let def_id = fdef.def_id in (* Compute the symbolic ASTs, if the function is transparent *) @@ -142,7 +142,10 @@ let translate_function_to_pure (config : C.partial_config) SymbolicToPure.llbc_fun_decls = fun_context.fun_decls; fun_sigs; fun_infos = fun_context.fun_infos; - gid_conv = fun_context.gid_conv; + } + in + let global_context = { + SymbolicToPure.llbc_global_decls = global_context.global_decls } in let ctx = @@ -156,6 +159,7 @@ let translate_function_to_pure (config : C.partial_config) state_var; type_context; fun_context; + global_context; fun_decl = fdef; forward_inputs = []; (* Empty for now *) @@ -293,14 +297,13 @@ let translate_module_to_pure (config : C.partial_config) log#ldebug (lazy "translate_module_to_pure"); (* Compute the type and function contexts *) - let type_context, fun_context = compute_type_fun_contexts m in + 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_context = { fun_decls = fun_context.fun_decls; fun_infos; - gid_conv = m.gid_conv; } in - let trans_ctx = { type_context; fun_context } in + let trans_ctx = { type_context; fun_context; global_context } in (* Translate all the type definitions *) let type_decls = SymbolicToPure.translate_type_decls m.types in @@ -495,7 +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 + 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 ) diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 047219ad..e77445cd 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -16,11 +16,16 @@ type type_context = C.type_context [@@deriving show] type fun_context = { fun_decls : A.fun_decl A.FunDeclId.Map.t; fun_infos : FA.fun_info A.FunDeclId.Map.t; - gid_conv : A.global_id_converter; } [@@deriving show] -type trans_ctx = { type_context : type_context; fun_context : fun_context } +type global_context = C.global_context [@@deriving show] + +type trans_ctx = { + type_context : type_context; + fun_context : fun_context; + global_context : global_context +} type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list @@ -40,16 +45,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 gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls 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 gid_conv = ctx.fun_context.gid_conv in - let fmt = PrintPure.mk_ast_formatter type_decls fun_decls gid_conv type_params in + let global_decls = ctx.global_context.global_decls in + let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in PrintPure.fun_decl_to_string fmt def let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : 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 'src/Modules.ml') 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 f106fd4ad0a221611c840bf0af0b1c2ff23f3d0f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:44:04 +0200 Subject: Make minor modifications --- src/ExtractToFStar.ml | 56 +++++++++++----------- src/InterpreterExpressions.ml | 15 +++--- src/InterpreterStatements.ml | 26 +++++++---- src/LlbcOfJson.ml | 105 +++++++++++++++++++++++------------------- src/Modules.ml | 20 ++++---- src/PureUtils.ml | 2 +- 6 files changed, 117 insertions(+), 107 deletions(-) (limited to 'src/Modules.ml') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 06f82ac4..eb88b916 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -314,6 +314,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) String.concat "_" fname in let global_name (name : global_name) : string = + (* Converting to snake case also lowercases the letters (in Rust, global + * names are written in capital letters). *) let parts = List.map to_snake_case (get_name name) in String.concat "_" parts in @@ -326,7 +328,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) fname ^ suffix in - let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string = + let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string + = let fname = fun_name_to_snake_case fname in (* Compute the suffix *) let suffix = "_decreases" in @@ -795,8 +798,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) ctx (** Simply add the global name to the context. *) -let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) - : extraction_ctx = +let extract_global_decl_register_names (ctx : extraction_ctx) + (def : A.global_decl) : extraction_ctx = ctx_add_global_decl_body def ctx (** The following function factorizes the extraction of ADT values. @@ -851,7 +854,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 = + (id : A.GlobalDeclId.id) : unit = F.pp_print_string fmt (ctx_get_global id ctx) (** [inside]: see [extract_ty]. @@ -921,13 +924,11 @@ 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 -> - extract_global ctx fmt global_id + | Global global_id -> 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 -> - extract_field_projector ctx fmt inside app proj qualif.type_args args - ) + extract_field_projector ctx fmt inside app proj qualif.type_args args) | _ -> (* "Regular" expression *) (* Open parentheses *) @@ -1493,9 +1494,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) 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 = + (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) *) @@ -1505,7 +1505,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; (* Print "QUALIF NAME " *) F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name); - F.pp_print_space fmt (); + F.pp_print_space fmt (); (* Open ": TYPE =" box (depth=2) *) F.pp_open_hvbox fmt 0; @@ -1523,8 +1523,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) if not is_opaque then ( (* Print " =" *) F.pp_print_space fmt (); - F.pp_print_string fmt "="; - ); + F.pp_print_string fmt "="); (* Close ": TYPE =" box (depth=2) *) F.pp_close_box fmt (); (* Close "QUALIF NAME : TYPE =" box (depth=1) *) @@ -1537,8 +1536,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (* Print "BODY" *) (Option.get extract_body) fmt; (* Close "BODY" box (depth=1) *) - F.pp_close_box fmt () - ); + F.pp_close_box fmt ()); (* Close the definition box (depth=0) *) F.pp_close_box fmt () @@ -1554,39 +1552,37 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = - assert (body.is_global_body); + 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.global_name_to_string global.name ^ "] *)"); - F.pp_print_space fmt (); + F.pp_print_break fmt 0 0; + F.pp_print_string fmt + ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); + F.pp_print_space fmt (); 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 - if body.signature.info.effect_info.can_fail - then (unwrap_result_ty ty, ty) - else (ty, mk_result_ty ty) + 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 -> let qualif = if interface then Val else AssumeVal in extract_global_decl_body ctx fmt qualif decl_name decl_ty None | Some body -> - extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt -> - extract_texpression ctx fmt false body.body - )); + 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_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 + 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 (** Extract a unit test, if the function is a unit function (takes no parameters, returns unit). diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 4598895e..4a4f3353 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -110,14 +110,13 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) ctx (** Convert an operand constant operand value to a typed value *) -let constant_to_typed_value (ty : T.ety) - (cv : V.constant_value) : V.typed_value = +let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value + = (* Check the type while converting - we actually need some information - * contained in the type *) + * contained in the type *) log#ldebug (lazy - ("constant_to_typed_value:" ^ "\n- cv: " - ^ PV.constant_value_to_string cv)); + ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty } @@ -128,10 +127,8 @@ let constant_to_typed_value (ty : T.ety) assert (int_ty = v.int_ty); assert (check_scalar_value_in_range v); { V.value = V.Concrete (V.Scalar v); ty } - (* Remaining cases (invalid) - listing as much as we can on purpose - (allows to catch errors at compilation if the definitions change) *) - | _, _ -> - failwith "Improperly typed constant value" + (* Remaining cases (invalid) *) + | _, _ -> failwith "Improperly typed constant value" (** Reorganize the environment in preparation for the evaluation of an operand. diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 48620439..34310ea1 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -831,8 +831,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cf_eval_rvalue cf_assign cf ctx - | A.AssignGlobal { dst; global } -> - eval_global config dst global cf ctx + | A.AssignGlobal { dst; global } -> eval_global config dst global cf ctx | A.FakeRead p -> let expand_prim_copy = false in let cf_prepare cf = @@ -910,20 +909,27 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (* Compose and apply *) comp cc cf_eval_st cf ctx -and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.id) : st_cm_fun = +and eval_global (config : C.config) (dest : V.VarId.id) + (gid : LA.GlobalDeclId.id) : st_cm_fun = fun cf ctx -> let global = C.ctx_lookup_global_decl ctx gid in let place = { E.var_id = dest; projection = [] } in match config.mode with | ConcreteMode -> - (* Treat the global as a function without arguments to call *) - (eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx + (* Treat the evaluation of the global as a call to the global body (without arguments) *) + (eval_local_function_call_concrete config global.body_id [] [] [] place) + cf ctx | SymbolicMode -> - (* Treat the global as a fresh symbolic value *) - 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 + (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be + * defined as equal to the value of the global (see `S.synthesize_global_eval`). *) + 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/LlbcOfJson.ml b/src/LlbcOfJson.ml index be43ff54..846d7232 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -394,7 +394,7 @@ let constant_value_of_json (js : json) : (V.constant_value, string) result = let* v = string_of_json v in Ok (V.String v) | _ -> Error "") - + let operand_of_json (js : json) : (E.operand, string) result = combine_error_msgs js "operand_of_json" (match js with @@ -599,10 +599,8 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result = | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = - list_of_json ( - pair_of_json - (list_of_json scalar_value_of_json) - statement_of_json) + list_of_json + (pair_of_json (list_of_json scalar_value_of_json) statement_of_json) tgts in let* otherwise = statement_of_json otherwise in @@ -633,47 +631,47 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result = let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in let* body = option_of_json fun_body_of_json body in - Ok { A.def_id; name; signature; body; is_global_body = false; } + Ok { A.def_id; name; signature; body; is_global_body = false } | _ -> Error "") (* Strict type for the number of function declarations (see [global_to_fun_id] below) *) -type global_id_converter = { fun_count : int } -[@@deriving show] +type global_id_converter = { fun_count : int } [@@deriving show] (** Converts a global id to its corresponding function id. To do so, it adds the global id to the number of function declarations : - We have the bijection `global_id <=> fun_id + fun_id_count`. + We have the bijection `global_fun_id <=> global_id + fun_id_count`. *) -let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : A.FunDeclId.id = - A.FunDeclId.of_int ((A.GlobalDeclId.to_int gid) + conv.fun_count) +let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) : + A.FunDeclId.id = + A.FunDeclId.of_int (A.GlobalDeclId.to_int gid + conv.fun_count) (* Converts a global declaration to a function declaration. *) -let global_decl_of_json (js : json) (gid_conv : global_id_converter) : (A.global_decl * A.fun_decl, string) result = +let global_decl_of_json (js : json) (gid_conv : global_id_converter) : + (A.global_decl * A.fun_decl, string) result = combine_error_msgs js "global_decl_of_json" (match js with - | `Assoc - [ - ("def_id", def_id); - ("name", name); - ("ty", ty); - ("body", body); - ] -> + | `Assoc [ ("def_id", def_id); ("name", name); ("ty", ty); ("body", body) ] + -> let* global_id = A.GlobalDeclId.id_of_json def_id in let fun_id = global_to_fun_id gid_conv global_id in let* name = fun_name_of_json name in let* ty = ety_of_json ty in let* body = option_of_json fun_body_of_json body in - let signature : A.fun_sig = { - region_params = []; - num_early_bound_regions = 0; - regions_hierarchy = []; - type_params = []; - inputs = []; - output = TU.ety_no_regions_to_sty ty; - } in - Ok ({ A.def_id = global_id; body_id = fun_id; name; ty; }, - { A.def_id = fun_id; name; signature; body; is_global_body = true; }) + let signature : A.fun_sig = + { + region_params = []; + num_early_bound_regions = 0; + regions_hierarchy = []; + type_params = []; + inputs = []; + output = TU.ety_no_regions_to_sty ty; + } + in + Ok + ( { A.def_id = global_id; body_id = fun_id; name; ty }, + { A.def_id = fun_id; name; signature; body; is_global_body = true } + ) | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) @@ -701,13 +699,12 @@ let fun_declaration_group_of_json (js : json) : let global_declaration_group_of_json (js : json) : (A.GlobalDeclId.id, string) result = combine_error_msgs js "global_declaration_group_of_json" - (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 "") + (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 = @@ -724,11 +721,11 @@ let declaration_group_of_json (js : json) : (M.declaration_group, string) result Ok (M.Global id) | _ -> Error "") -let length_of_json_list (js: json) : (int, string) result = +let length_of_json_list (js : json) : (int, string) result = combine_error_msgs js "get_json_list_len" (match js with - | `List jsl -> Ok (List.length jsl) - | _ -> Error ("not a list: " ^ show js)) + | `List jsl -> Ok (List.length jsl) + | _ -> Error ("not a list: " ^ show js)) let llbc_module_of_json (js : json) : (M.llbc_module, string) result = combine_error_msgs js "llbc_module_of_json" @@ -741,18 +738,30 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = ("functions", functions); ("globals", globals); ] -> + (* We first deserialize the declaration groups (which simply contain ids) + * and all the declarations *butù* the globals *) let* name = string_of_json name in - let* declarations = list_of_json declaration_group_of_json declarations 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 + (* When deserializing the globals, we split the global declarations + * between the globals themselves and their bodies, which are simply + * functions with no arguments. We add the global bodies to the list + * of function declarations: the (fresh) ids we use for those bodies + * are simply given by: `num_functions + global_id` *) 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 = + 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; - declarations; - types; - functions = functions @ global_bodies; - globals; - } + Ok + { + M.name; + declarations; + types; + functions = functions @ global_bodies; + globals; + } | _ -> Error "") diff --git a/src/Modules.ml b/src/Modules.ml index 009e1ba6..7f372d09 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -7,10 +7,9 @@ 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. Globals cannot be mutually dependent. *) +(** Module declaration. Globals cannot be mutually recursive. *) type declaration_group = | Type of type_declaration_group | Fun of fun_declaration_group @@ -27,7 +26,9 @@ type llbc_module = { (** LLBC module - TODO: rename to crate *) let compute_defs_maps (m : llbc_module) : - type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = + type_decl TypeDeclId.Map.t + * fun_decl FunDeclId.Map.t + * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) @@ -45,9 +46,11 @@ let compute_defs_maps (m : llbc_module) : in (types_map, funs_map, globals_map) -(** Split a module's declarations between types, globals and functions *) +(** Split a module's declarations between types, functions and globals *) let split_declarations (decls : declaration_group list) : - type_declaration_group list * fun_declaration_group list * GlobalDeclId.id list = + type_declaration_group list + * fun_declaration_group list + * GlobalDeclId.id list = let rec split decls = match decls with | [] -> ([], [], []) @@ -56,8 +59,7 @@ let split_declarations (decls : declaration_group list) : match d with | Type decl -> (decl :: types, funs, globals) | Fun decl -> (types, decl :: funs, globals) - | Global decl -> (types, funs, decl :: globals) - ) + | Global decl -> (types, funs, decl :: globals)) in split decls @@ -66,7 +68,7 @@ let split_declarations (decls : declaration_group list) : *) 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) diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 8a1c074d..e72ff9d7 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -402,7 +402,7 @@ 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" + | _ -> failwith "not a result type" let mk_result_fail_texpression (ty : ty) : texpression = let type_args = [ ty ] in -- cgit v1.3.1