summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Cps.ml3
-rw-r--r--compiler/InterpreterExpansion.ml7
-rw-r--r--compiler/InterpreterExpansion.mli7
-rw-r--r--compiler/InterpreterExpressions.ml53
-rw-r--r--compiler/InterpreterExpressions.mli12
-rw-r--r--compiler/InterpreterLoops.ml8
-rw-r--r--compiler/InterpreterPaths.ml7
-rw-r--r--compiler/InterpreterPaths.mli2
-rw-r--r--compiler/InterpreterStatements.ml8
-rw-r--r--compiler/InterpreterStatements.mli4
10 files changed, 73 insertions, 38 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index c414652d..7138477b 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -35,9 +35,6 @@ type statement_eval_res =
*)
[@@deriving show]
-(* TODO: remove *)
-type eval_result = SymbolicAst.expression
-
(** Function which takes a context as input, and evaluates to:
- a new context
- a continuation with which to build the execution trace, provided the
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 3c264c6e..5a3d6f10 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -446,8 +446,7 @@ let expand_symbolic_value_borrow (config : config) (span : Meta.span)
let expand_symbolic_bool (config : config) (span : Meta.span)
(sv : symbolic_value) (sv_place : SA.mplace option) :
eval_ctx ->
- (eval_ctx * eval_ctx)
- * (SymbolicAst.expression * SymbolicAst.expression -> eval_result) =
+ (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression) =
fun ctx ->
(* Compute the expanded value *)
let original_sv = sv in
@@ -533,7 +532,7 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span)
let expand_symbolic_adt (config : config) (span : Meta.span)
(sv : symbolic_value) (sv_place : SA.mplace option) :
- eval_ctx -> eval_ctx list * (SymbolicAst.expression list -> eval_result) =
+ eval_ctx -> eval_ctx list * (SA.expression list -> SA.expression) =
fun ctx ->
(* Debug *)
log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
@@ -568,7 +567,7 @@ let expand_symbolic_int (config : config) (span : Meta.span)
(int_type : integer_type) (tgts : scalar_value list) :
eval_ctx ->
(eval_ctx list * eval_ctx)
- * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result) =
+ * (SA.expression list * SA.expression -> SA.expression) =
fun ctx ->
(* Sanity check *)
sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) span;
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 9b5ebed3..50554490 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -38,7 +38,7 @@ val expand_symbolic_adt :
symbolic_value ->
SA.mplace option ->
eval_ctx ->
- eval_ctx list * (SymbolicAst.expression list -> eval_result)
+ eval_ctx list * (SA.expression list -> SA.expression)
(** Expand a symbolic boolean.
@@ -50,8 +50,7 @@ val expand_symbolic_bool :
symbolic_value ->
SA.mplace option ->
eval_ctx ->
- (eval_ctx * eval_ctx)
- * (SymbolicAst.expression * SymbolicAst.expression -> eval_result)
+ (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression)
(** Symbolic integers are expanded upon evaluating a [SwitchInt].
@@ -76,7 +75,7 @@ val expand_symbolic_int :
scalar_value list ->
eval_ctx ->
(eval_ctx list * eval_ctx)
- * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result)
+ * (SA.expression list * SA.expression -> SA.expression)
(** If this mode is activated through the [config], greedily expand the symbolic
values which need to be expanded. See {!type:Contexts.config} for more information.
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 51c8108e..32c1cda5 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -67,7 +67,9 @@ let read_place_check (span : Meta.span) (access : access_kind) (p : place)
let access_rplace_reorganize_and_read (config : config) (span : Meta.span)
(expand_prim_copy : bool) (access : access_kind) (p : place)
- (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+ (ctx : eval_ctx) :
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
(* Make sure we can evaluate the path *)
let ctx, cc = update_ctx_along_read_place config span access p ctx in
(* End the proper loans at the place itself *)
@@ -264,7 +266,8 @@ let prepare_eval_operand_reorganize (config : config) (span : Meta.span)
(** Evaluate an operand, without reorganizing the context before *)
let eval_operand_no_reorganize (config : config) (span : Meta.span)
(op : operand) (ctx : eval_ctx) :
- typed_value * eval_ctx * (eval_result -> eval_result) =
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
(* Debug *)
log#ldebug
(lazy
@@ -363,7 +366,9 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
(v, ctx, fun e -> e)
let eval_operand (config : config) (span : Meta.span) (op : operand)
- (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+ (ctx : eval_ctx) :
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
(* Debug *)
log#ldebug
(lazy
@@ -385,7 +390,9 @@ let prepare_eval_operands_reorganize (config : config) (span : Meta.span)
(** Evaluate several operands. *)
let eval_operands (config : config) (span : Meta.span) (ops : operand list)
(ctx : eval_ctx) :
- typed_value list * eval_ctx * (eval_result -> eval_result) =
+ typed_value list
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Prepare the operands *)
let ctx, cc = prepare_eval_operands_reorganize config span ops ctx in
(* Evaluate the operands *)
@@ -394,7 +401,9 @@ let eval_operands (config : config) (span : Meta.span) (ops : operand list)
let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
(op2 : operand) (ctx : eval_ctx) :
- (typed_value * typed_value) * eval_ctx * (eval_result -> eval_result) =
+ (typed_value * typed_value)
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
let res, ctx, cc = eval_operands config span [ op1; op2 ] ctx in
let res =
match res with
@@ -405,7 +414,9 @@ let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
(op : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Evaluate the operand *)
let v, ctx, cc = eval_operand config span op ctx in
(* Apply the unop *)
@@ -455,7 +466,9 @@ let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
(op : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Evaluate the operand *)
let v, ctx, cc = eval_operand config span op ctx in
(* Generate a fresh symbolic value to store the result *)
@@ -481,7 +494,9 @@ let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
let eval_unary_op (config : config) (span : Meta.span) (unop : unop)
(op : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
match config.mode with
| ConcreteMode -> eval_unary_op_concrete config span unop op ctx
| SymbolicMode -> eval_unary_op_symbolic config span unop op ctx
@@ -565,7 +580,9 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop)
let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
(op1 : operand) (op2 : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Evaluate the operands *)
let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
(* Compute the result of the binop *)
@@ -575,7 +592,9 @@ let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
(op1 : operand) (op2 : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Evaluate the operands *)
let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
(* Generate a fresh symbolic value to store the result *)
@@ -623,7 +642,9 @@ let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
(op1 : operand) (op2 : operand) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
match config.mode with
| ConcreteMode -> eval_binary_op_concrete config span binop op1 op2 ctx
| SymbolicMode -> eval_binary_op_symbolic config span binop op1 op2 ctx
@@ -632,7 +653,8 @@ let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
`&p` or `&mut p` or `&two-phase p`) *)
let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
(bkind : borrow_kind) (ctx : eval_ctx) :
- typed_value * eval_ctx * (eval_result -> eval_result) =
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
match bkind with
| BShared | BTwoPhaseMut | BShallow ->
(* **REMARK**: we initially treated shallow borrows like shared borrows.
@@ -715,7 +737,8 @@ let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
let eval_rvalue_aggregate (config : config) (span : Meta.span)
(aggregate_kind : aggregate_kind) (ops : operand list) (ctx : eval_ctx) :
- typed_value * eval_ctx * (eval_result -> eval_result) =
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
(* Evaluate the operands *)
let values, ctx, cc = eval_operands config span ops ctx in
(* Compute the value *)
@@ -787,7 +810,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
let eval_rvalue_not_global (config : config) (span : Meta.span)
(rvalue : rvalue) (ctx : eval_ctx) :
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
log#ldebug (lazy "eval_rvalue");
(* Small helper *)
let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index feb641d1..29234ea9 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -25,7 +25,7 @@ val access_rplace_reorganize_and_read :
access_kind ->
place ->
eval_ctx ->
- typed_value * eval_ctx * (eval_result -> eval_result)
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate an operand.
@@ -41,7 +41,7 @@ val eval_operand :
Meta.span ->
operand ->
eval_ctx ->
- typed_value * eval_ctx * (eval_result -> eval_result)
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate several operands at once. *)
val eval_operands :
@@ -49,7 +49,9 @@ val eval_operands :
Meta.span ->
operand list ->
eval_ctx ->
- typed_value list * eval_ctx * (eval_result -> eval_result)
+ typed_value list
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate an rvalue which is not a global (globals are handled elsewhere).
@@ -63,7 +65,9 @@ val eval_rvalue_not_global :
Meta.span ->
rvalue ->
eval_ctx ->
- (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result)
+ (typed_value, eval_error) result
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression)
(** Evaluate a fake read (update the context so that we can read a place) *)
val eval_fake_read : config -> Meta.span -> place -> cm_fun
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 4755f0e9..90a3afe8 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -105,7 +105,9 @@ let eval_loop_symbolic (config : config) (span : span)
will end with a call to the loop translation
*)
let ((res_fun_end, cf_fun_end), fp_bl_corresp) :
- ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ =
+ ((eval_ctx * statement_eval_res)
+ * (SymbolicAst.expression -> SymbolicAst.expression))
+ * _ =
(* First, preemptively end borrows/move values by matching the current
context with the target context *)
let ctx, cf_prepare =
@@ -158,7 +160,7 @@ let eval_loop_symbolic (config : config) (span : span)
(* Synthesize the loop body *)
let (resl_loop_body, cf_loop_body) :
(eval_ctx * statement_eval_res) list
- * (SymbolicAst.expression list -> eval_result) =
+ * (SymbolicAst.expression list -> SymbolicAst.expression) =
(* First, evaluate the loop body starting from the **fixed-point** context *)
let ctx_resl, cf_loop = eval_loop_body fp_ctx in
@@ -198,7 +200,7 @@ let eval_loop_symbolic (config : config) (span : span)
(* Apply and compose *)
let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in
- let cc (el : SymbolicAst.expression list) : eval_result =
+ let cc (el : SymbolicAst.expression list) : SymbolicAst.expression =
let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in
cf_loop el
in
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index faba1088..f201b84d 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -523,7 +523,8 @@ let rec update_ctx_along_write_place (config : config) (span : Meta.span)
comp cc (update_ctx_along_write_place config span access p ctx)
(** Small utility used to break control-flow *)
-exception UpdateCtx of (eval_ctx * (eval_result -> eval_result))
+exception
+ UpdateCtx of (eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression))
let rec end_loans_at_place (config : config) (span : Meta.span)
(access : access_kind) (p : place) : cm_fun =
@@ -629,7 +630,9 @@ let drop_outer_loans_at_lplace (config : config) (span : Meta.span) (p : place)
(ctx, cc)
let prepare_lplace (config : config) (span : Meta.span) (p : place)
- (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+ (ctx : eval_ctx) :
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+ =
log#ldebug
(lazy
("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 86f0dcc0..3377f612 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -104,4 +104,4 @@ val prepare_lplace :
Meta.span ->
place ->
eval_ctx ->
- typed_value * eval_ctx * (eval_result -> eval_result)
+ typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4b4bac62..c74a1218 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -306,7 +306,9 @@ let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx)
let move_return_value (config : config) (span : Meta.span)
(pop_return_value : bool) (ctx : eval_ctx) :
- typed_value option * eval_ctx * (eval_result -> eval_result) =
+ typed_value option
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
if pop_return_value then
let ret_vid = VarId.zero in
let v, ctx, cc =
@@ -317,7 +319,9 @@ let move_return_value (config : config) (span : Meta.span)
let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool)
(ctx : eval_ctx) :
- typed_value option * eval_ctx * (eval_result -> eval_result) =
+ typed_value option
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression) =
(* Debug *)
log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx));
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index c70396d6..443f559e 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -21,7 +21,9 @@ val pop_frame :
Meta.span ->
bool ->
eval_ctx ->
- typed_value option * eval_ctx * (eval_result -> eval_result)
+ typed_value option
+ * eval_ctx
+ * (SymbolicAst.expression -> SymbolicAst.expression)
(** Helper.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:13:14 +0000