summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Assumed.ml3
-rw-r--r--src/ExtractToFStar.ml4
-rw-r--r--src/InterpreterStatements.ml28
-rw-r--r--src/PrintPure.ml18
-rw-r--r--src/Pure.ml22
-rw-r--r--src/PureMicroPasses.ml6
-rw-r--r--src/PureToExtract.ml10
-rw-r--r--src/main.ml13
8 files changed, 74 insertions, 30 deletions
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:15:53 +0000