summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml115
-rw-r--r--compiler/InterpreterBorrows.ml4
-rw-r--r--compiler/InterpreterExpressions.ml19
-rw-r--r--compiler/InterpreterStatements.ml7
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/Invariants.ml16
-rw-r--r--compiler/Print.ml6
-rw-r--r--compiler/PureTypeCheck.ml22
-rw-r--r--compiler/Values.ml2
-rw-r--r--compiler/ValuesUtils.ml3
10 files changed, 139 insertions, 57 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index bcfe4369..9ee94db2 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -218,44 +218,53 @@ let keywords () =
List.concat [ named_unops; named_binops; misc ]
let assumed_adts () : (assumed_ty * string) list =
- List.map
- (fun (t, s) ->
- if !backend = Lean then
- ( t,
- Printf.sprintf "%c%s"
- (Char.uppercase_ascii s.[0])
- (String.sub s 1 (String.length s - 1)) )
- else (t, s))
- (match !backend with
- | Lean ->
- [
- (State, "State");
- (Result, "Result");
- (Error, "Error");
- (Fuel, "Nat");
- (Option, "Option");
- (Vec, "Vec");
- ]
- | Coq | FStar ->
- [
- (State, "state");
- (Result, "result");
- (Error, "error");
- (Fuel, "nat");
- (Option, "option");
- (Vec, "vec");
- ]
- | HOL4 ->
- [
- (State, "state");
- (Result, "result");
- (Error, "error");
- (Fuel, "num");
- (Option, "option");
- (Vec, "vec");
- ])
+ match !backend with
+ | Lean ->
+ [
+ (State, "State");
+ (Result, "Result");
+ (Error, "Error");
+ (Fuel, "Nat");
+ (Option, "Option");
+ (Vec, "Vec");
+ (Array, "Array");
+ (Slice, "Slice");
+ (Str, "Str");
+ (Range, "Range");
+ ]
+ | Coq | FStar ->
+ [
+ (State, "state");
+ (Result, "result");
+ (Error, "error");
+ (Fuel, "nat");
+ (Option, "option");
+ (Vec, "vec");
+ (Array, "array");
+ (Slice, "slice");
+ (Str, "str");
+ (Range, "range");
+ ]
+ | HOL4 ->
+ [
+ (State, "state");
+ (Result, "result");
+ (Error, "error");
+ (Fuel, "num");
+ (Option, "option");
+ (Vec, "vec");
+ (Array, "array");
+ (Slice, "slice");
+ (Str, "str");
+ (Range, "range");
+ ]
-let assumed_structs : (assumed_ty * string) list = []
+let assumed_struct_constructors () : (assumed_ty * string) list =
+ match !backend with
+ | Lean -> [ (Range, "Range.mk"); (Array, "Array.mk") ]
+ | Coq -> [ (Range, "range.mk"); (Array, "array.mk") ]
+ | FStar -> [ (Range, "mkrange"); (Array, "mkarray") ]
+ | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
@@ -320,6 +329,21 @@ let assumed_llbc_functions () :
(VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
(VecIndexMut, None, "vec_index_mut_fwd");
(VecIndexMut, rg0, "vec_index_mut_back");
+ (ArraySharedIndex, None, "array_shared_index");
+ (ArrayMutIndex, None, "array_mut_index_fwd");
+ (ArrayMutIndex, rg0, "array_mut_index_back");
+ (ArrayToSharedSlice, None, "array_to_shared_slice");
+ (ArrayToMutSlice, None, "array_to_mut_slice_fwd");
+ (ArrayToMutSlice, rg0, "array_to_mut_slice_back");
+ (ArraySharedSubslice, None, "array_shared_subslice");
+ (ArrayMutSubslice, None, "array_mut_subslice_fwd");
+ (ArrayMutSubslice, rg0, "array_mut_subslice_back");
+ (SliceSharedIndex, None, "slice_shared_index");
+ (SliceMutIndex, None, "slice_mut_index_fwd");
+ (SliceMutIndex, rg0, "slice_mut_index_back");
+ (SliceSharedSubslice, None, "slice_shared_subslice");
+ (SliceMutSubslice, None, "slice_mut_subslice_fwd");
+ (SliceMutSubslice, rg0, "slice_mut_subslice_back");
]
| Lean ->
[
@@ -335,6 +359,21 @@ let assumed_llbc_functions () :
(VecIndex, rg0, "Vec.index_back") (* shouldn't be used *);
(VecIndexMut, None, "Vec.index_mut");
(VecIndexMut, rg0, "Vec.index_mut_back");
+ (ArraySharedIndex, None, "Array.shared_index");
+ (ArrayMutIndex, None, "Array.mut_index");
+ (ArrayMutIndex, rg0, "Array.mut_index_back");
+ (ArrayToSharedSlice, None, "Array.to_shared_slice");
+ (ArrayToMutSlice, None, "Array.to_mut_slice");
+ (ArrayToMutSlice, rg0, "Array.to_mut_slice_back");
+ (ArraySharedSubslice, None, "Array.shared_subslice");
+ (ArrayMutSubslice, None, "Array.mut_subslice");
+ (ArrayMutSubslice, rg0, "Array.mut_subslice_back");
+ (SliceSharedIndex, None, "Slice.shared_index");
+ (SliceMutIndex, None, "Slice.mut_index");
+ (SliceMutIndex, rg0, "Slice.mut_index_back");
+ (SliceSharedSubslice, None, "Slice.shared_subslice");
+ (SliceMutSubslice, None, "Slice.mut_subslice");
+ (SliceMutSubslice, rg0, "Slice.mut_subslice_back");
]
let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
@@ -361,7 +400,7 @@ let names_map_init () : names_map_init =
{
keywords = keywords ();
assumed_adts = assumed_adts ();
- assumed_structs;
+ assumed_structs = assumed_struct_constructors ();
assumed_variants = assumed_variants ();
assumed_llbc_functions = assumed_llbc_functions ();
assumed_pure_functions = assumed_pure_functions ();
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 3d258b32..4d67a4e4 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,8 +452,8 @@ let give_back_symbolic_value (_config : C.config)
| V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
->
()
- | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin ->
- raise (Failure "Unrechable"));
+ | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+ raise (Failure "Unreachable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c3ff8d4f..0834cfe2 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -713,17 +713,30 @@ let eval_rvalue_aggregate (config : C.config)
let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
(* Call the continuation *)
cf aggregated ctx
- | E.AggregatedArray (ety, cg) ->
+ | E.AggregatedArray (ety, cg) -> (
(* Sanity check: all the values have the proper type *)
assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
(* Sanity check: the number of values is consistent with the length *)
let len = (literal_as_scalar (const_generic_as_literal cg)).value in
- assert (Z.to_int len = List.length values);
+ assert (len = Z.of_int (List.length values));
let v = V.Adt { variant_id = None; field_values = values } in
let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in
let aggregated : V.typed_value = { V.value = v; ty } in
+ (* In order to generate a better AST, we introduce a symbolic
+ value equal to the array. The reason is that otherwise, the
+ array we introduce here might be duplicated in the generated
+ code: by introducing a symbolic value we introduce a let-binding
+ in the generated code. *)
+ let saggregated =
+ mk_fresh_symbolic_typed_value_from_ety V.Aggregate ty
+ in
(* Call the continuation *)
- cf aggregated ctx
+ match cf saggregated ctx with
+ | None -> None
+ | Some e ->
+ (* Introduce the symbolic value in the AST *)
+ let sv = ValuesUtils.value_as_symbolic saggregated.value in
+ Some (SymbolicAst.IntroSymbolic (ctx, None, sv, aggregated, e)))
in
(* Compose and apply *)
comp eval_ops compute cf
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 79fe79e7..207acef6 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1051,12 +1051,10 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
(** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
- (region_args : T.erased_region list) (type_args : T.ety list)
+ (_region_args : T.erased_region list) (type_args : T.ety list)
(cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
st_cm_fun =
fun cf ctx ->
- assert (region_args = []);
-
(* Retrieve the (correctly instantiated) body *)
let def = C.ctx_lookup_fun_decl ctx fid in
(* We can evaluate the function call only if it is not opaque *)
@@ -1157,11 +1155,10 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
*)
and eval_function_call_symbolic_from_inst_sig (config : C.config)
(fid : A.fun_id) (inst_sg : A.inst_fun_sig)
- (region_args : T.erased_region list) (type_args : T.ety list)
+ (_region_args : T.erased_region list) (type_args : T.ety list)
(cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
st_cm_fun =
fun cf ctx ->
- assert (region_args = []);
(* Generate a fresh symbolic value for the return value *)
let ret_sv_ty = inst_sg.A.output in
let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index a50bb7ac..7bd37550 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -255,7 +255,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
raise Found
else ()
| V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
- | V.SynthRetGivenBack | V.Global | V.LoopGivenBack ->
+ | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate ->
()
end
in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index e73c09c4..f29c7f88 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -459,8 +459,20 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
assert (v0.V.ty = inner_ty);
assert (v1.V.ty = inner_ty)
- | (T.Array | T.Slice | T.Str), _, _, _, _ ->
- raise (Failure "Unexpected")
+ | T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
+ (* *)
+ assert (
+ List.for_all
+ (fun (v : V.typed_value) -> v.V.ty = inner_ty)
+ inner_values);
+ (* The length is necessarily concrete *)
+ let len =
+ (PrimitiveValuesUtils.literal_as_scalar
+ (TypesUtils.const_generic_as_literal cg))
+ .value
+ in
+ assert (Z.of_int (List.length inner_values) = len)
+ | (T.Slice | T.Str), _, _, _, _ -> raise (Failure "Unexpected")
| _ -> raise (Failure "Erroneous type"))
| V.Bottom, _ -> (* Nothing to check *) ()
| V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7d7e8549..9aa73d7c 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -126,7 +126,11 @@ module Values = struct
else raise (Failure "Unreachable")
| Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
| Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
- | _ -> raise (Failure "Inconsistent value"))
+ | Array, _ ->
+ (* Happens when we aggregate values *)
+ "@Array[" ^ String.concat ", " field_values ^ "]"
+ | _ ->
+ raise (Failure ("Inconsistent value: " ^ V.show_typed_value v)))
| _ -> raise (Failure "Inconsistent typed value"))
| Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
| Borrow bc -> borrow_content_to_string fmt bc
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 0f64720e..8f5b5df4 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -3,7 +3,11 @@
open Pure
open PureUtils
-(** Utility function, used for type checking *)
+(** Utility function, used for type checking.
+
+ We need the number of fields for cases like `Slice`, when the number of fields
+ varies.
+ *)
let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
(type_id : type_id) (variant_id : VariantId.id option) (tys : ty list)
(cgs : const_generic list) : ty list =
@@ -51,10 +55,18 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
let ty = Collections.List.to_cons_nil tys in
assert (variant_id = None);
[ ty; ty ]
- | Vec | Array | Slice | Str ->
- raise
- (Failure
- "Unreachable: trying to access the fields of an opaque type"))
+ | Array ->
+ let ty = Collections.List.to_cons_nil tys in
+ let cg = Collections.List.to_cons_nil cgs in
+ let len =
+ (PrimitiveValuesUtils.literal_as_scalar
+ (TypesUtils.const_generic_as_literal cg))
+ .value
+ in
+ let len = Z.to_int len in
+ Collections.List.repeat len ty
+ | Vec | Slice | Str ->
+ raise (Failure "Attempting to access the fields of an opaque type"))
type tc_ctx = {
type_decls : type_decl TypeDeclId.Map.t; (** The type declarations *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index f70b9b4b..d884c319 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -50,6 +50,8 @@ type sv_kind =
(** A value given back by a loop (when ending abstractions while going backwards) *)
| LoopJoin
(** The result of a loop join (when computing loop fixed points) *)
+ | Aggregate
+ (** A symbolic value we introduce in place of an aggregate value *)
[@@deriving show, ord]
(** Ancestor for {!symbolic_value} iter visitor *)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index d748cc2e..527434c1 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -17,6 +17,9 @@ let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
let mk_abottom (ty : rty) : typed_avalue = { value = ABottom; ty }
let mk_aignored (ty : rty) : typed_avalue = { value = AIgnored; ty }
+let value_as_symbolic (v : value) : symbolic_value =
+ match v with Symbolic v -> v | _ -> raise (Failure "Unexpected")
+
(** Box a value *)
let mk_box_value (v : typed_value) : typed_value =
let box_ty = mk_box_ty v.ty in
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 23:38:47 +0000