diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | src/Assumed.ml | 3 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 28 | ||||
| -rw-r--r-- | src/PrintPure.ml | 18 | ||||
| -rw-r--r-- | src/Pure.ml | 22 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 6 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 10 | ||||
| -rw-r--r-- | src/main.ml | 13 |
9 files changed, 79 insertions, 35 deletions
@@ -1,9 +1,9 @@ all: build-run-check-trace CHARON_HOME=../charon/charon -CHARON_TESTS_DIR=$(CHARON_HOME)/tests -RS_TEST_FILE=tests/no_nested_borrows.rs -CFIM_TEST_FILE=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim +CHARON_TESTS_DIR=$(CHARON_HOME)/tests/src +RS_TEST_FILE1=tests/src/no_nested_borrows.rs +CFIM_TEST_FILE1=$(CHARON_TESTS_DIR)/no_nested_borrows.cfim DEST_DIR=tests/ # Build the project @@ -14,7 +14,7 @@ build: # Build the project and run the executable .PHONY: build-run build-run: build - dune exec -- src/main.exe $(CFIM_TEST_FILE) -dest $(DEST_DIR) > tests/trace_current.txt + dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) > tests/trace_current.txt # Build the project and run the executable, then check that the behaviour # of the interpreter didn't change by comparing the newly generated trace @@ -33,7 +33,7 @@ regen-trace: generate-cfim build-run .PHONY: generate-cfim generate-cfim: - cd ../charon/charon && cargo run $(RS_TEST_FILE) + cd ../charon/charon && cargo run $(RS_TEST_FILE1) doc: dune build @doc 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; |