From 1e6f3fb7d8ac8e72ca38f08d7e4be5c835e3443a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 8 Feb 2022 17:51:04 +0100 Subject: Make progress on implementing support for types and functions like Option and Vec --- src/Assumed.ml | 3 +++ src/ExtractToFStar.ml | 4 +++- src/InterpreterStatements.ml | 28 ++++++++++++++-------------- src/PrintPure.ml | 18 +++++++++++++++++- src/Pure.ml | 22 ++++++++++++---------- src/PureMicroPasses.ml | 6 +++++- src/PureToExtract.ml | 10 +++++++++- src/main.ml | 13 +++++++++++-- 8 files changed, 74 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/Assumed.ml b/src/Assumed.ml index 97cd2c78..5a9fb51b 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -245,6 +245,9 @@ let assumed_sigs : (A.assumed_fun_id * A.fun_sig) list = (VecIndexMut, Sig.vec_index_mut_sig); ] +let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig = + snd (List.find (fun (id', _) -> id = id') assumed_sigs) + let assumed_names : (A.assumed_fun_id * Identifiers.name) list = [ (Replace, [ "core"; "mem"; "replace" ]); diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 636c68d3..db09b316 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -284,6 +284,8 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : (* The "pair" case is frequent enough to have its special treatment *) if List.length tys = 2 then "p" else "t" | Assumed Result -> "r" + | Assumed Option -> "opt" + | Assumed Vec -> "v" | AdtId adt_id -> let def = TypeDefId.Map.find adt_id ctx.type_context.type_defs @@ -719,7 +721,7 @@ let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit let def_id = match pe.pkind with | E.ProjAdt (def_id, None) -> def_id - | E.ProjAdt (_, Some _) | E.ProjTuple _ -> + | E.ProjAdt (_, Some _) | E.ProjOption _ | E.ProjTuple _ -> (* We can't have field accesses on enumerations (variables for * the fields are introduced upon the moment we match over the * enumeration). We also forbid field access on tuples, because diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index c926c63a..375f3dec 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -9,6 +9,7 @@ open TypesUtils open ValuesUtils module Inv = Invariants module S = SynthesizeSymbolic +open Errors open Cps open InterpreterUtils open InterpreterProjectors @@ -350,9 +351,10 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun = comp cf_pop cf_assign (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_replace_concrete (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = - fun cf ctx -> raise Unimplemented +let eval_replace_concrete (_config : C.config) + (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun + = + fun _cf _ctx -> raise Unimplemented (** Auxiliary function - see [eval_non_local_function_call] *) let eval_box_new_concrete (config : C.config) @@ -492,9 +494,10 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) | _ -> failwith "Inconsistent state" (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_vec_function_concrete (config : C.config) (fid : A.assumed_fun id) - (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun = - fun cf ctx -> raise Unimplemented +let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) + (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun + = + fun _cf _ctx -> raise Unimplemented (** Evaluate a non-local function call in concrete mode *) let eval_non_local_function_call_concrete (config : C.config) @@ -549,7 +552,7 @@ let eval_non_local_function_call_concrete (config : C.config) * access to a body. *) let cf_eval_body : cm_fun = match fid with - | A.Replace -> eval_replace config region_params type_params + | A.Replace -> eval_replace_concrete config region_params type_params | BoxNew -> eval_box_new_concrete config region_params type_params | BoxDeref -> eval_box_deref_concrete config region_params type_params | BoxDerefMut -> @@ -1128,13 +1131,10 @@ and eval_non_local_function_call_symbolic (config : C.config) * instantiated signatures, and delegate the work to an auxiliary function *) let inst_sig = match fid with - | A.BoxNew -> instantiate_fun_sig type_params Assumed.box_new_sig - | A.BoxDeref -> - instantiate_fun_sig type_params Assumed.box_deref_shared_sig - | A.BoxDerefMut -> - instantiate_fun_sig type_params Assumed.box_deref_mut_sig - | A.BoxFree -> failwith "Unreachable" - (* should have been treated above *) + | A.BoxFree -> + (* should have been treated above *) + failwith "Unreachable" + | _ -> instantiate_fun_sig type_params (Assumed.get_assumed_sig fid) in (* Evaluate the function call *) diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 5c25f2bd..f0e5df77 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -265,7 +265,23 @@ let adt_g_value_to_string (fmt : value_formatter) else if variant_id = result_fail_id then ( assert (field_values = []); "@Result::Fail") - else failwith "Unreachable: improper variant id for result type") + else failwith "Unreachable: improper variant id for result type" + | Option -> + let variant_id = Option.get variant_id in + if variant_id = option_some_id then + match field_values with + | [ v ] -> "@Option::Some " ^ v + | _ -> failwith "Option::Some takes exactly one value" + else if variant_id = option_none_id then ( + assert (field_values = []); + "@Option::None") + else failwith "Unreachable: improper variant id for result type" + | Vec -> + assert (variant_id = None); + let field_values = + List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values + in + "Vec [" ^ String.concat "; " field_values ^ "]") | _ -> failwith "Inconsistent typed value" let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) : diff --git a/src/Pure.ml b/src/Pure.ml index c773d613..d706a366 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -20,21 +20,23 @@ module VarId = IdGen () type integer_type = T.integer_type [@@deriving show, ord] -type assumed_ty = - | Result - (** The assumed types for the pure AST. - - In comparison with CFIM: - - we removed `Box` (because it is translated as the identity: `Box T == T`) - - we added `Result`, which is the type used in the error monad. This allows - us to have a unified treatment of expressions. - *) -[@@deriving show, ord] +(** The assumed types for the pure AST. + + In comparison with CFIM: + - we removed `Box` (because it is translated as the identity: `Box T == T`) + - we added `Result`, which is the type used in the error monad. This allows + us to have a unified treatment of expressions. + *) +type assumed_ty = Result | Vec | Option [@@deriving show, ord] let result_return_id = VariantId.of_int 0 let result_fail_id = VariantId.of_int 1 +let option_some_id = T.option_some_id + +let option_none_id = T.option_none_id + type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty [@@deriving show, ord] diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index ceee71dd..5ac2af4e 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -730,7 +730,11 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def = | _ -> failwith "Unreachable" in arg.e - | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e) + | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e + | ( ( A.Replace | A.VecNew | A.VecPush | A.VecInsert | A.VecLen + | A.VecIndex | A.VecIndexMut ), + _ ) -> + super#visit_Call env call) | _ -> super#visit_Call env call end in diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index b563ba15..518e0a7d 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -326,6 +326,11 @@ let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = if variant_id = result_return_id then "@result::Return" else if variant_id = result_fail_id then "@result::Fail" else failwith "Unreachable" + | Assumed Option -> + if variant_id = option_some_id then "@option::Some" + else if variant_id = option_none_id then "@option::None" + else failwith "Unreachable" + | Assumed Vec -> failwith "Unreachable" | AdtId id -> ( let def = TypeDefId.Map.find id type_defs in match def.kind with @@ -339,7 +344,10 @@ let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = let field_name = match id with | Tuple -> failwith "Unreachable" - | Assumed Result -> failwith "Unreachable" + | Assumed (Result | Option) -> failwith "Unreachable" + | Assumed Vec -> + (* We can't directly have access to the fields of a vector *) + failwith "Unreachable" | AdtId id -> ( let def = TypeDefId.Map.find id type_defs in match def.kind with diff --git a/src/main.ml b/src/main.ml index 95bebf39..b8673023 100644 --- a/src/main.ml +++ b/src/main.ml @@ -27,6 +27,8 @@ let () = let decompose_monads = ref false in let unfold_monads = ref true in let filter_unused_calls = ref true in + let test_units = ref false in + let test_trans_units = ref false in let spec = [ @@ -48,6 +50,13 @@ let () = ( "-filter-unused-calls", Arg.Set filter_unused_calls, " Filter the unused function calls, when possible" ); + ( "-test-units", + Arg.Set test_units, + " Test the unit functions with the concrete interpreter" ); + ( "-test-trans-units", + Arg.Set test_trans_units, + " Test the translated unit functions with the target theorem prover's \ + normalizer" ); ] in let spec = Arg.align spec in @@ -113,7 +122,7 @@ let () = in (* Test the unit functions with the concrete interpreter *) - I.Test.test_unit_functions config m; + if !test_units then I.Test.test_unit_functions config m; (* Evaluate the symbolic interpreter on the functions, ignoring the * functions which contain loops - TODO: remove *) @@ -121,7 +130,7 @@ let () = I.Test.test_functions_symbolic config synthesize m; (* Translate the functions *) - let test_unit_functions = true in + let test_unit_functions = !test_trans_units in let micro_passes_config = { Micro.decompose_monadic_let_bindings = !decompose_monads; -- cgit v1.2.3