diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 5 | ||||
| -rw-r--r-- | src/FunIdentifier.ml | 1 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 114 | ||||
| -rw-r--r-- | src/Print.ml | 1 | ||||
| -rw-r--r-- | src/Pure.ml | 1 |
6 files changed, 75 insertions, 54 deletions
@@ -31,8 +31,8 @@ build: .PHONY: test test: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ - trans-external trans-nll-betree_nll \ - trans-nll-betree_main + trans-external trans-constants \ + trans-nll-betree_nll trans-nll-betree_main \ # Add specific options to some tests trans-no_nested_borrows trans-paper: \ @@ -48,6 +48,9 @@ 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: SUBDIR:=misc + trans-external: TRANS_OPTIONS += trans-external: SUBDIR:=misc diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 9766ddaf..b85c146b 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -902,7 +902,10 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | 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 + (* TODO | Global global_id -> + extract_global_ref ctx fmt inside global_id*) + ) | _ -> (* "Regular" expression *) (* Open parentheses *) diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml index dd7e9318..956fce3f 100644 --- a/src/FunIdentifier.ml +++ b/src/FunIdentifier.ml @@ -1,2 +1,3 @@ open Identifiers module FunDeclId = IdGen () +module GlobalDeclId = IdGen () diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 4549365d..ee26d00d 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -1,5 +1,6 @@ module T = Types module V = Values +module LA = LlbcAst open Scalars module E = Expressions open Errors @@ -71,53 +72,67 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool) comp cc read_place cf ctx (** Convert an operand constant operand value to a typed value *) -let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) - (cv : E.operand_constant_value) : V.typed_value = - (* Check the type while converting - we actually need some information - * contained in the type *) - log#ldebug - (lazy - ("operand_constant_value_to_typed_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 - (* Compute the field values *) - let field_values = - List.map - (fun (ty, v) -> operand_constant_value_to_typed_value ctx ty v) +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) - in - (* Put together *) - let value = V.Adt { variant_id; field_values } in - { value; ty } - (* Scalar, boolean... *) - | T.Bool, ConstantValue (Bool v) -> { V.value = V.Concrete (Bool v); ty } - | T.Char, ConstantValue (Char v) -> { V.value = V.Concrete (Char v); ty } - | T.Str, ConstantValue (String v) -> { V.value = V.Concrete (String v); ty } - | 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); - { 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) *) - | _, ConstantAdt _ | _, ConstantValue _ -> - failwith "Improperly typed constant value" + 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" (** Prepare the evaluation of an operand. @@ -157,8 +172,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand) fun ctx -> match op with | Expressions.Constant (ty, cv) -> - let v = operand_constant_value_to_typed_value ctx ty cv in - cf v ctx + eval_operand_constant_value ty cv cf ctx | Expressions.Copy p -> (* Access the value *) let access = Read in @@ -191,9 +205,7 @@ let eval_operand (config : C.config) (op : E.operand) ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | Expressions.Constant (ty, cv) -> - let v = operand_constant_value_to_typed_value ctx ty cv in - cf v ctx + | Expressions.Constant (ty, cv) -> eval_operand_constant_value ty cv cf ctx | Expressions.Copy p -> (* Access the value *) let access = Read in diff --git a/src/Print.ml b/src/Print.ml index 28040181..9e2ff3cd 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -863,6 +863,7 @@ module LlbcAst = struct 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 diff --git a/src/Pure.ml b/src/Pure.ml index 05f78e35..256a872a 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -305,6 +305,7 @@ type qualif_id = | Func of fun_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] |