summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Expressions.ml2
-rw-r--r--compiler/ExtractToFStar.ml14
-rw-r--r--compiler/InterpreterExpansion.ml7
-rw-r--r--compiler/InterpreterExpressions.ml69
-rw-r--r--compiler/InterpreterPaths.ml4
-rw-r--r--compiler/InterpreterProjectors.ml8
-rw-r--r--compiler/InterpreterStatements.ml13
-rw-r--r--compiler/Invariants.ml13
-rw-r--r--compiler/LlbcOfJson.ml42
-rw-r--r--compiler/PrimitiveValues.ml41
-rw-r--r--compiler/Print.ml8
-rw-r--r--compiler/PrintPure.ml4
-rw-r--r--compiler/Pure.ml22
-rw-r--r--compiler/PureToExtract.ml2
-rw-r--r--compiler/PureTypeCheck.ml10
-rw-r--r--compiler/PureUtils.ml10
-rw-r--r--compiler/SymbolicToPure.ml10
-rw-r--r--compiler/SynthesizeSymbolic.ml9
-rw-r--r--compiler/Values.ml49
-rw-r--r--compiler/dune2
20 files changed, 183 insertions, 156 deletions
diff --git a/compiler/Expressions.ml b/compiler/Expressions.ml
index e2eaf1e7..1fca7284 100644
--- a/compiler/Expressions.ml
+++ b/compiler/Expressions.ml
@@ -75,7 +75,7 @@ let all_binops =
type operand =
| Copy of place
| Move of place
- | Constant of ety * constant_value
+ | Constant of ety * primitive_value
[@@deriving show]
(** An aggregated ADT.
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index 5d212941..a77e3df3 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -392,10 +392,10 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
basename ^ string_of_int i
in
- let extract_constant_value (fmt : F.formatter) (_inside : bool)
- (cv : constant_value) : unit =
+ let extract_primitive_value (fmt : F.formatter) (_inside : bool)
+ (cv : primitive_value) : unit =
match cv with
- | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.V.value)
+ | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value)
| Bool b ->
let b = if b then "true" else "false" in
F.pp_print_string fmt b
@@ -424,7 +424,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
var_basename;
type_var_basename;
append_index;
- extract_constant_value;
+ extract_primitive_value;
extract_unop = fstar_extract_unop;
extract_binop = fstar_extract_binop;
}
@@ -865,8 +865,8 @@ let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
(inside : bool) (v : typed_pattern) : extraction_ctx =
match v.value with
- | PatConcrete cv ->
- ctx.fmt.extract_constant_value fmt inside cv;
+ | PatConstant cv ->
+ ctx.fmt.extract_primitive_value fmt inside cv;
ctx
| PatVar (v, _) ->
let vname =
@@ -899,7 +899,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
| Var var_id ->
let var_name = ctx_get_var var_id ctx in
F.pp_print_string fmt var_name
- | Const cv -> ctx.fmt.extract_constant_value fmt inside cv
+ | Const cv -> ctx.fmt.extract_primitive_value fmt inside cv
| App _ ->
let app, args = destruct_apps e in
extract_App ctx fmt inside app args
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 0ca34b43..8caa828e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -4,6 +4,7 @@
* using indices to identify the values for instance). *)
module T = Types
+module PV = PrimitiveValues
module V = Values
module E = Expressions
module C = Contexts
@@ -477,8 +478,8 @@ let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
let rty = original_sv.V.sv_ty in
assert (rty = T.Bool);
(* Expand the symbolic value to true or false and continue execution *)
- let see_true = V.SeConcrete (V.Bool true) in
- let see_false = V.SeConcrete (V.Bool false) in
+ let see_true = V.SePrimitive (PV.Bool true) in
+ let see_false = V.SePrimitive (PV.Bool false) in
let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
(* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
apply_branching_symbolic_expansions_non_borrow config original_sv
@@ -629,7 +630,7 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
* (optional expansion, statement to execute)
*)
let tgts =
- List.map (fun (v, cf) -> (Some (V.SeConcrete (V.Scalar v)), cf)) tgts
+ List.map (fun (v, cf) -> (Some (V.SePrimitive (PV.Scalar v)), cf)) tgts
in
let tgts = List.append tgts [ (None, otherwise) ] in
(* Then expand and evaluate - this generates the proper symbolic AST *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 62d9b80b..d74ee85f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -1,4 +1,5 @@
module T = Types
+module PV = PrimitiveValues
module V = Values
module LA = LlbcAst
open Scalars
@@ -7,7 +8,6 @@ open Errors
module C = Contexts
module Subst = Substitute
module L = Logging
-module PV = Print.Values
open TypesUtils
open ValuesUtils
module Inv = Invariants
@@ -110,23 +110,24 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
ctx
(** Convert an operand constant operand value to a typed value *)
-let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value
+let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) : V.typed_value
=
(* Check the type while converting - we actually need some information
* contained in the type *)
log#ldebug
(lazy
- ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv));
+ ("primitive_to_typed_value:" ^ "\n- cv: "
+ ^ Print.Values.primitive_value_to_string cv));
match (ty, cv) with
(* Scalar, boolean... *)
- | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty }
- | T.Char, Char v -> { V.value = V.Concrete (Char v); ty }
- | T.Str, String v -> { V.value = V.Concrete (String v); ty }
- | T.Integer int_ty, V.Scalar v ->
+ | T.Bool, Bool v -> { V.value = V.Primitive (Bool v); ty }
+ | T.Char, Char v -> { V.value = V.Primitive (Char v); ty }
+ | T.Str, String v -> { V.value = V.Primitive (String v); ty }
+ | T.Integer int_ty, PV.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 }
+ { V.value = V.Primitive (PV.Scalar v); ty }
(* Remaining cases (invalid) *)
| _, _ -> failwith "Improperly typed constant value"
@@ -173,7 +174,7 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
match op with
| Expressions.Constant (ty, cv) ->
(* No need to reorganize the context *)
- constant_to_typed_value ty cv |> ignore;
+ primitive_to_typed_value ty cv |> ignore;
cf ctx
| Expressions.Copy p ->
(* Access the value *)
@@ -201,7 +202,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
(* Evaluate *)
match op with
- | Expressions.Constant (ty, cv) -> cf (constant_to_typed_value ty cv) ctx
+ | Expressions.Constant (ty, cv) -> cf (primitive_to_typed_value ty cv) ctx
| Expressions.Copy p ->
(* Access the value *)
let access = Read in
@@ -299,21 +300,21 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
(* Apply the unop *)
let apply cf (v : V.typed_value) : m_fun =
match (unop, v.V.value) with
- | E.Not, V.Concrete (Bool b) ->
- cf (Ok { v with V.value = V.Concrete (Bool (not b)) })
- | E.Neg, V.Concrete (V.Scalar sv) -> (
- let i = Z.neg sv.V.value in
+ | E.Not, V.Primitive (Bool b) ->
+ cf (Ok { v with V.value = V.Primitive (Bool (not b)) })
+ | E.Neg, V.Primitive (PV.Scalar sv) -> (
+ let i = Z.neg sv.PV.value in
match mk_scalar sv.int_ty i with
| Error _ -> cf (Error EPanic)
- | Ok sv -> cf (Ok { v with V.value = V.Concrete (V.Scalar sv) }))
- | E.Cast (src_ty, tgt_ty), V.Concrete (V.Scalar sv) -> (
+ | Ok sv -> cf (Ok { v with V.value = V.Primitive (PV.Scalar sv) }))
+ | E.Cast (src_ty, tgt_ty), V.Primitive (PV.Scalar sv) -> (
assert (src_ty == sv.int_ty);
- let i = sv.V.value in
+ let i = sv.PV.value in
match mk_scalar tgt_ty i with
| Error _ -> cf (Error EPanic)
| Ok sv ->
let ty = T.Integer tgt_ty in
- let value = V.Concrete (V.Scalar sv) in
+ let value = V.Primitive (PV.Scalar sv) in
cf (Ok { V.ty; value }))
| _ -> raise (Failure "Invalid input for unop")
in
@@ -367,11 +368,11 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
(* Equality/inequality check is primitive only for a subset of types *)
assert (ty_is_primitively_copyable v1.ty);
let b = v1 = v2 in
- Ok { V.value = V.Concrete (Bool b); ty = T.Bool })
+ Ok { V.value = V.Primitive (Bool b); ty = T.Bool })
else
(* For the non-equality operations, the input values are necessarily scalars *)
match (v1.V.value, v2.V.value) with
- | V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> (
+ | V.Primitive (PV.Scalar sv1), V.Primitive (PV.Scalar sv2) -> (
(* There are binops which require the two operands to have the same
type, and binops for which it is not the case.
There are also binops which return booleans, and binops which
@@ -383,15 +384,15 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
assert (sv1.int_ty = sv2.int_ty);
let b =
match binop with
- | E.Lt -> Z.lt sv1.V.value sv2.V.value
- | E.Le -> Z.leq sv1.V.value sv2.V.value
- | E.Ge -> Z.geq sv1.V.value sv2.V.value
- | E.Gt -> Z.gt sv1.V.value sv2.V.value
+ | E.Lt -> Z.lt sv1.PV.value sv2.PV.value
+ | E.Le -> Z.leq sv1.PV.value sv2.PV.value
+ | E.Ge -> Z.geq sv1.PV.value sv2.PV.value
+ | E.Gt -> Z.gt sv1.PV.value sv2.PV.value
| E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
| E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
raise (Failure "Unreachable")
in
- Ok ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
+ Ok ({ V.value = V.Primitive (Bool b); ty = T.Bool } : V.typed_value)
| E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr
-> (
(* The two operands must have the same type and the result is an integer *)
@@ -399,15 +400,15 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
let res =
match binop with
| E.Div ->
- if sv2.V.value = Z.zero then Error ()
- else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value)
+ if sv2.PV.value = Z.zero then Error ()
+ else mk_scalar sv1.int_ty (Z.div sv1.PV.value sv2.PV.value)
| E.Rem ->
(* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
- if sv2.V.value = Z.zero then Error ()
- else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value)
- | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value)
- | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value)
- | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value)
+ if sv2.PV.value = Z.zero then Error ()
+ else mk_scalar sv1.int_ty (Z.rem sv1.PV.value sv2.PV.value)
+ | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.PV.value sv2.PV.value)
+ | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.PV.value sv2.PV.value)
+ | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.PV.value sv2.PV.value)
| E.BitXor -> raise Unimplemented
| E.BitAnd -> raise Unimplemented
| E.BitOr -> raise Unimplemented
@@ -419,7 +420,7 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
| Ok sv ->
Ok
{
- V.value = V.Concrete (V.Scalar sv);
+ V.value = V.Primitive (PV.Scalar sv);
ty = Integer sv1.int_ty;
})
| E.Shl | E.Shr -> raise Unimplemented
@@ -521,7 +522,7 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
| Error _ -> raise (Failure "Disciminant id out of range")
(* Should really never happen *)
| Ok sv ->
- cf { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
+ cf { V.value = V.Primitive (PV.Scalar sv); ty = Integer Isize }))
| _ ->
raise
(Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v))
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index d54a046e..28e81dc6 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -248,7 +248,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
in
Ok (ctx, { res with updated = nv })
else Error (FailSharedLoan bids))
- | (_, (V.Concrete _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
+ | (_, (V.Primitive _ | V.Adt _ | V.Bottom | V.Borrow _), _) as r ->
let pe, v, ty = r in
let pe = "- pe: " ^ E.show_projection_elem pe in
let v = "- v:\n" ^ V.show_value v in
@@ -711,7 +711,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
* the fact that we have exhaustive matches below makes very obvious the cases
* in which we need to fail *)
match v.V.value with
- | V.Concrete _ -> (ctx, v)
+ | V.Primitive _ -> (ctx, v)
| V.Adt av ->
(* Sanity check *)
(match v.V.ty with
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 064b8969..1d95c4b9 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -26,7 +26,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
if not (ty_has_regions_in_set regions ty) then []
else
match (v.V.value, ty) with
- | V.Concrete _, (T.Bool | T.Char | T.Integer _ | T.Str) -> []
+ | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> []
| V.Adt adt, T.Adt (id, region_params, tys) ->
(* Retrieve the types of the fields *)
let field_types =
@@ -136,7 +136,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
else
let value : V.avalue =
match (v.V.value, ty) with
- | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AConcrete cv
+ | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.APrimitive cv
| V.Adt adt, T.Adt (id, region_params, tys) ->
(* Retrieve the types of the fields *)
let field_types =
@@ -252,7 +252,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
let ty = Subst.erase_regions sv.V.sv_ty in
let value =
match see with
- | SeConcrete cv -> V.Concrete cv
+ | SePrimitive cv -> V.Primitive cv
| SeAdt (variant_id, field_values) ->
let field_values =
List.map mk_typed_value_from_symbolic_value field_values
@@ -293,7 +293,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
(* Match *)
let (value, ty) : V.avalue * T.rty =
match (see, original_sv_ty) with
- | SeConcrete _, (T.Bool | T.Char | T.Integer _ | T.Str) ->
+ | SePrimitive _, (T.Bool | T.Char | T.Integer _ | T.Str) ->
(V.AIgnored, original_sv_ty)
| SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) ->
(* Project over the field values *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4e61e683..45d2aab2 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1,4 +1,5 @@
module T = Types
+module PV = PrimitiveValues
module V = Values
module E = Expressions
module C = Contexts
@@ -144,7 +145,7 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
let eval_assert cf (v : V.typed_value) : m_fun =
fun ctx ->
match v.value with
- | Concrete (Bool b) ->
+ | Primitive (Bool b) ->
(* Branch *)
if b = assertion.expected then cf Unit ctx else cf Panic ctx
| _ ->
@@ -174,7 +175,7 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
* even if we are in symbolic mode. Note that this case should be
* extremely rare... *)
match v.value with
- | Concrete (Bool _) ->
+ | Primitive (Bool _) ->
(* Delegate to the concrete evaluation function *)
eval_assertion_concrete config assertion cf ctx
| Symbolic sv ->
@@ -279,7 +280,7 @@ let set_discriminant (config : C.config) (p : E.place)
* or reset an already initialized value, really. *)
raise (Failure "Unexpected value")
| _, (V.Adt _ | V.Bottom) -> raise (Failure "Inconsistent state")
- | _, (V.Concrete _ | V.Borrow _ | V.Loan _) ->
+ | _, (V.Primitive _ | V.Borrow _ | V.Loan _) ->
raise (Failure "Unexpected value")
in
(* Compose and apply *)
@@ -963,7 +964,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
match tgts with
| A.If (st1, st2) -> (
match op_v.value with
- | V.Concrete (V.Bool b) ->
+ | V.Primitive (PV.Bool b) ->
(* Evaluate the if and the branch body *)
let cf_branch cf : m_fun =
(* Branch *)
@@ -983,11 +984,11 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
| _ -> raise (Failure "Inconsistent state"))
| A.SwitchInt (int_ty, stgts, otherwise) -> (
match op_v.value with
- | V.Concrete (V.Scalar sv) ->
+ | V.Primitive (PV.Scalar sv) ->
(* Evaluate the branch *)
let cf_eval_branch cf =
(* Sanity check *)
- assert (sv.V.int_ty = int_ty);
+ assert (sv.PV.int_ty = int_ty);
(* Find the branch *)
match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
| None -> eval_statement config otherwise cf
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 4a3364a6..bd577d8d 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -2,6 +2,7 @@
* are always maintained by evaluation contexts *)
module T = Types
+module PV = PrimitiveValues
module V = Values
module E = Expressions
module C = Contexts
@@ -377,10 +378,10 @@ let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) :
let info = { outer_borrow = false; outer_shared = false } in
visitor#visit_eval_ctx info ctx
-let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit =
+let check_primitive_value_type (cv : V.primitive_value) (ty : T.ety) : unit =
match (cv, ty) with
- | V.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty)
- | V.Bool _, T.Bool | V.Char _, T.Char | V.String _, T.Str -> ()
+ | PV.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty)
+ | PV.Bool _, T.Bool | PV.Char _, T.Char | PV.String _, T.Str -> ()
| _ -> failwith "Erroneous typing"
let check_typing_invariant (ctx : C.eval_ctx) : unit =
@@ -404,7 +405,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
method! visit_typed_value info tv =
(* Check the current pair (value, type) *)
(match (tv.V.value, tv.V.ty) with
- | V.Concrete cv, ty -> check_constant_value_type cv ty
+ | V.Primitive cv, ty -> check_primitive_value_type cv ty
(* ADT case *)
| V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
(* Retrieve the definition to check the variant id, the number of
@@ -502,8 +503,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
method! visit_typed_avalue info atv =
(* Check the current pair (value, type) *)
(match (atv.V.value, atv.V.ty) with
- | V.AConcrete cv, ty ->
- check_constant_value_type cv (Subst.erase_regions ty)
+ | V.APrimitive cv, ty ->
+ check_primitive_value_type cv (Subst.erase_regions ty)
(* ADT case *)
| V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
(* Retrieve the definition to check the variant id, the number of
diff --git a/compiler/LlbcOfJson.ml b/compiler/LlbcOfJson.ml
index 79c9b756..ad4cd5e4 100644
--- a/compiler/LlbcOfJson.ml
+++ b/compiler/LlbcOfJson.ml
@@ -14,6 +14,7 @@ open OfJsonBasic
open Identifiers
open Meta
module T = Types
+module PV = PrimitiveValues
module V = Values
module S = Scalars
module E = Expressions
@@ -361,48 +362,49 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
(match js with
| `Assoc [ ("Isize", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = Isize }
+ Ok { PV.value = bi; int_ty = Isize }
| `Assoc [ ("I8", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = I8 }
+ Ok { PV.value = bi; int_ty = I8 }
| `Assoc [ ("I16", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = I16 }
+ Ok { PV.value = bi; int_ty = I16 }
| `Assoc [ ("I32", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = I32 }
+ Ok { PV.value = bi; int_ty = I32 }
| `Assoc [ ("I64", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = I64 }
+ Ok { PV.value = bi; int_ty = I64 }
| `Assoc [ ("I128", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = I128 }
+ Ok { PV.value = bi; int_ty = I128 }
| `Assoc [ ("Usize", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = Usize }
+ Ok { PV.value = bi; int_ty = Usize }
| `Assoc [ ("U8", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = U8 }
+ Ok { PV.value = bi; int_ty = U8 }
| `Assoc [ ("U16", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = U16 }
+ Ok { PV.value = bi; int_ty = U16 }
| `Assoc [ ("U32", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = U32 }
+ Ok { PV.value = bi; int_ty = U32 }
| `Assoc [ ("U64", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = U64 }
+ Ok { PV.value = bi; int_ty = U64 }
| `Assoc [ ("U128", `List [ bi ]) ] ->
let* bi = big_int_of_json bi in
- Ok { V.value = bi; int_ty = U128 }
+ Ok { PV.value = bi; int_ty = U128 }
| _ -> Error "")
in
match res with
| Error _ -> res
| Ok sv ->
if not (S.check_scalar_value_in_range sv) then (
- log#serror ("Scalar value not in range: " ^ V.show_scalar_value sv);
- raise (Failure ("Scalar value not in range: " ^ V.show_scalar_value sv)));
+ log#serror ("Scalar value not in range: " ^ PV.show_scalar_value sv);
+ raise
+ (Failure ("Scalar value not in range: " ^ PV.show_scalar_value sv)));
res
let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
@@ -482,21 +484,21 @@ let binop_of_json (js : json) : (E.binop, string) result =
| `String "Shr" -> Ok E.Shr
| _ -> Error ("binop_of_json failed on:" ^ show js)
-let constant_value_of_json (js : json) : (V.constant_value, string) result =
+let primitive_value_of_json (js : json) : (V.primitive_value, string) result =
combine_error_msgs js __FUNCTION__
(match js with
| `Assoc [ ("Scalar", scalar_value) ] ->
let* scalar_value = scalar_value_of_json scalar_value in
- Ok (V.Scalar scalar_value)
+ Ok (PV.Scalar scalar_value)
| `Assoc [ ("Bool", v) ] ->
let* v = bool_of_json v in
- Ok (V.Bool v)
+ Ok (PV.Bool v)
| `Assoc [ ("Char", v) ] ->
let* v = char_of_json v in
- Ok (V.Char v)
+ Ok (PV.Char v)
| `Assoc [ ("String", v) ] ->
let* v = string_of_json v in
- Ok (V.String v)
+ Ok (PV.String v)
| _ -> Error "")
let operand_of_json (js : json) : (E.operand, string) result =
@@ -510,7 +512,7 @@ let operand_of_json (js : json) : (E.operand, string) result =
Ok (E.Move place)
| `Assoc [ ("Const", `List [ ty; cv ]) ] ->
let* ty = ety_of_json ty in
- let* cv = constant_value_of_json cv in
+ let* cv = primitive_value_of_json cv in
Ok (E.Constant (ty, cv))
| _ -> Error "")
diff --git a/compiler/PrimitiveValues.ml b/compiler/PrimitiveValues.ml
new file mode 100644
index 00000000..0bf37256
--- /dev/null
+++ b/compiler/PrimitiveValues.ml
@@ -0,0 +1,41 @@
+(** The primitive values. *)
+
+open Types
+
+(** We use big integers to store the integer values (this way we don't have
+ to think about the bounds, nor architecture issues - Rust allows to
+ manipulate 128-bit integers for instance).
+ *)
+type big_int = Z.t
+
+let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
+ match json with
+ | `Int i -> Ok (Z.of_int i)
+ | `Intlit is -> Ok (Z.of_string is)
+ | _ -> Error "not an integer or an integer literal"
+
+let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
+
+let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
+ Format.pp_print_string fmt (Z.to_string bi)
+
+let show_big_int (bi : big_int) : string = Z.to_string bi
+
+(** A scalar value
+
+ Note that we use unbounded integers everywhere.
+ We then harcode the boundaries for the different types.
+ *)
+type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
+
+(** A primitive value.
+
+ Can be used by operands (in which case it represents a constant) or by
+ the interpreter to represent a concrete, primitive value.
+ *)
+type primitive_value =
+ | Scalar of scalar_value
+ | Bool of bool
+ | Char of char
+ | String of string
+[@@deriving show]
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 8f52b291..52a93a4d 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -210,7 +210,7 @@ module Values = struct
let scalar_value_to_string (sv : V.scalar_value) : string =
big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty
- let constant_value_to_string (cv : V.constant_value) : string =
+ let primitive_value_to_string (cv : V.primitive_value) : string =
match cv with
| Scalar sv -> scalar_value_to_string sv
| Bool b -> Bool.to_string b
@@ -240,7 +240,7 @@ module Values = struct
string =
let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in
match v.value with
- | Concrete cv -> constant_value_to_string cv
+ | Primitive cv -> primitive_value_to_string cv
| Adt av -> (
let field_values =
List.map (typed_value_to_string fmt) av.field_values
@@ -352,7 +352,7 @@ module Values = struct
string =
let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in
match v.value with
- | AConcrete cv -> constant_value_to_string cv
+ | APrimitive cv -> primitive_value_to_string cv
| AAdt av -> (
let field_values =
List.map (typed_avalue_to_string fmt) av.field_values
@@ -877,7 +877,7 @@ module LlbcAst = struct
| E.Move p -> "move " ^ place_to_string fmt p
| E.Constant (ty, cv) ->
"("
- ^ PV.constant_value_to_string cv
+ ^ PV.primitive_value_to_string cv
^ " : "
^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
^ ")"
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index a9e42f6c..6fafa0a3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -357,7 +357,7 @@ let adt_g_value_to_string (fmt : value_formatter)
let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
string =
match v.value with
- | PatConcrete cv -> Print.Values.constant_value_to_string cv
+ | PatConstant cv -> Print.Values.primitive_value_to_string cv
| PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v
| PatVar (v, Some mp) ->
let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
@@ -436,7 +436,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
| Var var_id ->
let s = fmt.var_id_to_string var_id in
if inside then "(" ^ s ^ ")" else s
- | Const cv -> Print.Values.constant_value_to_string cv
+ | Const cv -> Print.Values.primitive_value_to_string cv
| App _ ->
(* Recursively destruct the app, to have a pair (app, arguments list) *)
let app, args = destruct_apps e in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 77265f75..ae4cba22 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1,6 +1,7 @@
open Identifiers
open Names
module T = Types
+module PV = PrimitiveValues
module V = Values
module E = Expressions
module A = LlbcAst
@@ -122,7 +123,7 @@ type type_decl = {
[@@deriving show]
type scalar_value = V.scalar_value [@@deriving show]
-type constant_value = V.constant_value [@@deriving show]
+type primitive_value = V.primitive_value [@@deriving show]
(** Because we introduce a lot of temporary variables, the list of variables
is not fixed: we thus must carry all its information with the variable
@@ -167,7 +168,10 @@ type variant_id = VariantId.id [@@deriving show]
class ['self] iter_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
- method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
+
+ method visit_primitive_value : 'env -> primitive_value -> unit =
+ fun _ _ -> ()
+
method visit_var : 'env -> var -> unit = fun _ _ -> ()
method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
@@ -179,7 +183,7 @@ class ['self] map_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
- method visit_constant_value : 'env -> constant_value -> constant_value =
+ method visit_primitive_value : 'env -> primitive_value -> primitive_value =
fun _ x -> x
method visit_var : 'env -> var -> var = fun _ x -> x
@@ -193,7 +197,7 @@ class virtual ['self] reduce_value_base =
object (self : 'self)
inherit [_] VisitorsRuntime.reduce
- method visit_constant_value : 'env -> constant_value -> 'a =
+ method visit_primitive_value : 'env -> primitive_value -> 'a =
fun _ _ -> self#zero
method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
@@ -207,8 +211,8 @@ class virtual ['self] mapreduce_value_base =
object (self : 'self)
inherit [_] VisitorsRuntime.mapreduce
- method visit_constant_value : 'env -> constant_value -> constant_value * 'a
- =
+ method visit_primitive_value
+ : 'env -> primitive_value -> primitive_value * 'a =
fun _ x -> (x, self#zero)
method visit_var : 'env -> var -> var * 'a = fun _ x -> (x, self#zero)
@@ -224,8 +228,8 @@ class virtual ['self] mapreduce_value_base =
(** A pattern (which appears on the left of assignments, in matches, etc.). *)
type pattern =
- | PatConcrete of constant_value
- (** {!PatConcrete} is necessary because we merge the switches over integer
+ | PatConstant of primitive_value
+ (** {!PatConstant} is necessary because we merge the switches over integer
values and the matches over enumerations *)
| PatVar of var * mplace option
| PatDummy (** Ignored value: [_]. *)
@@ -373,7 +377,7 @@ class virtual ['self] mapreduce_expression_base =
*)
type expression =
| Var of var_id (** a variable *)
- | Const of constant_value
+ | Const of primitive_value
| App of texpression * texpression
(** Application of a function to an argument.
diff --git a/compiler/PureToExtract.ml b/compiler/PureToExtract.ml
index 77c3afd4..7f79aa88 100644
--- a/compiler/PureToExtract.ml
+++ b/compiler/PureToExtract.ml
@@ -137,7 +137,7 @@ type formatter = {
indices to names, the responsability of finding a proper index is
delegated to helper functions.
*)
- extract_constant_value : F.formatter -> bool -> constant_value -> unit;
+ extract_primitive_value : F.formatter -> bool -> primitive_value -> unit;
(** Format a constant value.
Inputs:
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index caad8a58..8c19a53b 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -45,17 +45,17 @@ type tc_ctx = {
env : ty VarId.Map.t; (** Environment from variables to types *)
}
-let check_constant_value (v : constant_value) (ty : ty) : unit =
+let check_primitive_value (v : primitive_value) (ty : ty) : unit =
match (ty, v) with
- | Integer int_ty, V.Scalar sv -> assert (int_ty = sv.V.int_ty)
+ | Integer int_ty, PV.Scalar sv -> assert (int_ty = sv.PV.int_ty)
| Bool, Bool _ | Char, Char _ | Str, String _ -> ()
| _ -> raise (Failure "Inconsistent type")
let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx =
log#ldebug (lazy ("check_typed_pattern: " ^ show_typed_pattern v));
match v.value with
- | PatConcrete cv ->
- check_constant_value cv v.ty;
+ | PatConstant cv ->
+ check_primitive_value cv v.ty;
ctx
| PatDummy -> ctx
| PatVar (var, _) ->
@@ -97,7 +97,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
match VarId.Map.find_opt var_id ctx.env with
| None -> ()
| Some ty -> assert (ty = e.ty))
- | Const cv -> check_constant_value cv e.ty
+ | Const cv -> check_primitive_value cv e.ty
| App (app, arg) ->
let input_ty, output_ty = destruct_arrow app.ty in
assert (input_ty = arg.ty);
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 39f3d76a..f5756046 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -35,16 +35,16 @@ let dest_arrow_ty (ty : ty) : ty * ty =
| Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
| _ -> raise (Failure "Unreachable")
-let compute_constant_value_ty (cv : constant_value) : ty =
+let compute_primitive_value_ty (cv : primitive_value) : ty =
match cv with
- | V.Scalar sv -> Integer sv.V.int_ty
+ | PV.Scalar sv -> Integer sv.PV.int_ty
| Bool _ -> Bool
| Char _ -> Char
| String _ -> Str
-let mk_typed_pattern_from_constant_value (cv : constant_value) : typed_pattern =
- let ty = compute_constant_value_ty cv in
- { value = PatConcrete cv; ty }
+let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern =
+ let ty = compute_primitive_value_ty cv in
+ { value = PatConstant cv; ty }
let mk_let (monadic : bool) (lv : typed_pattern) (re : texpression)
(next_e : texpression) : texpression =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 24af578f..749eae1d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -728,7 +728,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
(* Translate the value *)
let value =
match v.value with
- | V.Concrete cv -> { e = Const cv; ty }
+ | V.Primitive cv -> { e = Const cv; ty }
| Adt av -> (
let variant_id = av.variant_id in
let field_values = List.map translate av.field_values in
@@ -810,7 +810,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
let translate = typed_avalue_to_consumed ctx in
let value =
match av.value with
- | AConcrete _ -> raise (Failure "Unreachable")
+ | APrimitive _ -> raise (Failure "Unreachable")
| AAdt adt_v -> (
(* Translate the field values *)
let field_values = List.filter_map translate adt_v.field_values in
@@ -944,7 +944,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
(ctx : bs_ctx) : bs_ctx * typed_pattern option =
let ctx, value =
match av.value with
- | AConcrete _ -> raise (Failure "Unreachable")
+ | APrimitive _ -> raise (Failure "Unreachable")
| AAdt adt_v -> (
(* Translate the field values *)
(* For now we forget the meta-place information so that it doesn't get used
@@ -1485,7 +1485,7 @@ and translate_expansion (config : config) (p : S.mplace option)
match exp with
| ExpandNoBranch (sexp, e) -> (
match sexp with
- | V.SeConcrete _ ->
+ | V.SePrimitive _ ->
(* Actually, we don't *register* symbolic expansions to constant
* values in the symbolic ADT *)
raise (Failure "Unreachable")
@@ -1638,7 +1638,7 @@ and translate_expansion (config : config) (p : S.mplace option)
(* We don't need to update the context: we don't introduce any
* new values/variables *)
let branch = translate_expression config branch_e ctx in
- let pat = mk_typed_pattern_from_constant_value (V.Scalar v) in
+ let pat = mk_typed_pattern_from_primitive_value (PV.Scalar v) in
{ pat; branch }
in
let branches = List.map translate_branch branches in
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index a2256bdd..b4d2ae25 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -1,5 +1,6 @@
module C = Collections
module T = Types
+module PV = PrimitiveValues
module V = Values
module E = Expressions
module A = LlbcAst
@@ -33,8 +34,8 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
(* Boolean expansion: there should be two branches *)
match ls with
| [
- (Some (V.SeConcrete (V.Bool true)), true_exp);
- (Some (V.SeConcrete (V.Bool false)), false_exp);
+ (Some (V.SePrimitive (PV.Bool true)), true_exp);
+ (Some (V.SePrimitive (PV.Bool false)), false_exp);
] ->
ExpandBool (true_exp, false_exp)
| _ -> failwith "Ill-formed boolean expansion")
@@ -47,8 +48,8 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
let get_scalar (see : V.symbolic_expansion option) : V.scalar_value
=
match see with
- | Some (V.SeConcrete (V.Scalar cv)) ->
- assert (cv.V.int_ty = int_ty);
+ | Some (V.SePrimitive (PV.Scalar cv)) ->
+ assert (cv.PV.int_ty = int_ty);
cv
| _ -> failwith "Unreachable"
in
diff --git a/compiler/Values.ml b/compiler/Values.ml
index e404f40d..7d6623aa 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -1,7 +1,7 @@
open Identifiers
open Types
-(* TODO: I often write "abstract" (value, borrow content, etc.) while I should
+(* TODO(SH): I often write "abstract" (value, borrow content, etc.) while I should
* write "abstraction" (because those values are not abstract, they simply are
* inside abstractions) *)
@@ -11,37 +11,9 @@ module SymbolicValueId = IdGen ()
module AbstractionId = IdGen ()
module FunCallId = IdGen ()
-(** A variable *)
-
-type big_int = Z.t
-
-let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
- match json with
- | `Int i -> Ok (Z.of_int i)
- | `Intlit is -> Ok (Z.of_string is)
- | _ -> Error "not an integer or an integer literal"
-
-let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
-
-let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
- Format.pp_print_string fmt (Z.to_string bi)
-
-let show_big_int (bi : big_int) : string = Z.to_string bi
-
-(** A scalar value
-
- Note that we use unbounded integers everywhere.
- We then harcode the boundaries for the different types.
- *)
-type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
-
-(** A constant value *)
-type constant_value =
- | Scalar of scalar_value
- | Bool of bool
- | Char of char
- | String of string
-[@@deriving show]
+type big_int = PrimitiveValues.big_int [@@deriving show]
+type scalar_value = PrimitiveValues.scalar_value [@@deriving show]
+type primitive_value = PrimitiveValues.primitive_value [@@deriving show]
(** The kind of a symbolic value, which precises how the value was generated *)
type sv_kind =
@@ -80,7 +52,10 @@ type symbolic_value = {
class ['self] iter_typed_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
- method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
+
+ method visit_primitive_value : 'env -> primitive_value -> unit =
+ fun _ _ -> ()
+
method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
@@ -91,7 +66,7 @@ class ['self] map_typed_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
- method visit_constant_value : 'env -> constant_value -> constant_value =
+ method visit_primitive_value : 'env -> primitive_value -> primitive_value =
fun _ cv -> cv
method visit_erased_region : 'env -> erased_region -> erased_region =
@@ -105,7 +80,7 @@ class ['self] map_typed_value_base =
(** An untyped value, used in the environments *)
type value =
- | Concrete of constant_value (** Concrete (non-symbolic) value *)
+ | Primitive of primitive_value (** Non-symbolic primitive value *)
| Adt of adt_value (** Enumerations and structures *)
| Bottom (** No value (uninitialized or moved value) *)
| Borrow of borrow_content (** A borrowed value *)
@@ -392,7 +367,7 @@ class ['self] map_typed_avalue_base =
part of it is thus "abstracted" away.
*)
type avalue =
- | AConcrete of constant_value
+ | APrimitive of primitive_value
(** TODO: remove. We actually don't use that for the synthesis, but the
meta-values.
@@ -838,7 +813,7 @@ type abs = {
TODO: this should rather be name "expanded_symbolic"
*)
type symbolic_expansion =
- | SeConcrete of constant_value
+ | SePrimitive of primitive_value
| SeAdt of (VariantId.id option * symbolic_value list)
| SeMutRef of BorrowId.id * symbolic_value
| SeSharedRef of BorrowId.Set.t * symbolic_value
diff --git a/compiler/dune b/compiler/dune
index 0968b2be..08b0d30f 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -24,7 +24,7 @@
PureMicroPasses Pure PureToExtract PureTypeCheck PureUtils Scalars
StringUtils Substitute SymbolicAst SymbolicToPure SynthesizeSymbolic
TranslateCore Translate TypesAnalysis Types TypesUtils Utils Values
- ValuesUtils))
+ ValuesUtils PrimitiveValues))
(documentation
(package aeneas))
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 01:30:36 +0000