summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2024-06-05 11:30:42 +0200
committerGitHub2024-06-05 11:30:42 +0200
commitbaa0771885546816461e063131162b94c6954d86 (patch)
tree2f8b8bd9d6ddef3e56d3c840690e94d9322a963a
parentc708fc2556806abc95cd2ca173a94a5fb49d034d (diff)
parent967c1aa8bd47e76905baeda5b9d41167af664942 (diff)
Merge pull request #227 from AeneasVerif/son/clean-synthesis
Remove the use of `Option` from the functions synthesizing the symbolic AST
Diffstat (limited to '')
-rw-r--r--compiler/Cps.ml51
-rw-r--r--compiler/Interpreter.ml188
-rw-r--r--compiler/InterpreterExpansion.ml26
-rw-r--r--compiler/InterpreterExpansion.mli8
-rw-r--r--compiler/InterpreterExpressions.ml103
-rw-r--r--compiler/InterpreterExpressions.mli12
-rw-r--r--compiler/InterpreterLoops.ml40
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml20
-rw-r--r--compiler/InterpreterPaths.ml7
-rw-r--r--compiler/InterpreterPaths.mli2
-rw-r--r--compiler/InterpreterStatements.ml52
-rw-r--r--compiler/InterpreterStatements.mli4
-rw-r--r--compiler/SynthesizeSymbolic.ml238
-rw-r--r--compiler/Translate.ml5
-rw-r--r--tests/src/mutually-recursive-traits.lean.out12
15 files changed, 345 insertions, 423 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index f7694ba2..917989ff 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -35,23 +35,24 @@ type statement_eval_res =
*)
[@@deriving show]
-type eval_result = SymbolicAst.expression option
-
(** Function which takes a context as input, and evaluates to:
- a new context
- a continuation with which to build the execution trace, provided the
trace for the end of the execution.
*)
-type cm_fun = eval_ctx -> eval_ctx * (eval_result -> eval_result)
+type cm_fun =
+ eval_ctx -> eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
type st_cm_fun =
- eval_ctx -> (eval_ctx * statement_eval_res) * (eval_result -> eval_result)
+ eval_ctx ->
+ (eval_ctx * statement_eval_res)
+ * (SymbolicAst.expression -> SymbolicAst.expression)
(** Type of a function used when evaluating a statement *)
type stl_cm_fun =
eval_ctx ->
(eval_ctx * statement_eval_res) list
- * (SymbolicAst.expression list option -> eval_result)
+ * (SymbolicAst.expression list -> SymbolicAst.expression)
(** Compose continuations that we use to compute execution traces *)
let cc_comp (f : 'b -> 'c) (g : 'a -> 'b) : 'a -> 'c = fun e -> f (g e)
@@ -90,27 +91,11 @@ let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e))
in
eval_list inputs ctx
-let opt_list_to_list_opt (len : int) (el : 'a option list) : 'a list option =
- let expr_list =
- List.rev
- (List.fold_left
- (fun acc a -> match a with Some b -> b :: acc | None -> [])
- [] el)
- in
- let _ = assert (List.length expr_list = len) in
- if Option.is_none (List.hd expr_list) then None else Some expr_list
-
let cc_singleton file line span cf el =
- match el with
- | Some [ e ] -> cf (Some e)
- | Some _ -> internal_error file line span
- | _ -> None
+ match el with [ e ] -> cf e | _ -> internal_error file line span
let cf_singleton file line span el =
- match el with
- | Some [ e ] -> Some e
- | Some _ -> internal_error file line span
- | _ -> None
+ match el with [ e ] -> e | _ -> internal_error file line span
(** It happens that we need to concatenate lists of results, for
instance when evaluating the branches of a match. When applying
@@ -120,15 +105,11 @@ let cf_singleton file line span el =
*)
let comp_seqs (file : string) (line : int) (span : Meta.span)
(ls :
- ('a list
- * (SymbolicAst.expression list option -> SymbolicAst.expression option))
- list) :
- 'a list
- * (SymbolicAst.expression list option -> SymbolicAst.expression list option)
- =
+ ('a list * (SymbolicAst.expression list -> SymbolicAst.expression)) list)
+ : 'a list * (SymbolicAst.expression list -> SymbolicAst.expression list) =
(* Auxiliary function: given a list of expressions el, build the expressions
corresponding to the different branches *)
- let rec cc_aux ls el =
+ let rec cc ls el =
match ls with
| [] ->
(* End of the list of branches: there shouldn't be any expression remaining *)
@@ -140,14 +121,10 @@ let comp_seqs (file : string) (line : int) (span : Meta.span)
- the expressions for the remaining branches *)
let el0, el = Collections.List.split_at el (List.length resl) in
(* Compute the expression for the current branch *)
- let e0 = cf (Some el0) in
- let e0 =
- match e0 with None -> internal_error file line span | Some e -> e
- in
+ let e0 = cf el0 in
(* Compute the expressions for the remaining branches *)
- let e = cc_aux ls el in
+ let e = cc ls el in
(* Concatenate *)
e0 :: e
in
- let cc el = match el with None -> None | Some el -> Some (cc_aux ls el) in
- (List.flatten (fst (List.split ls)), cc)
+ (List.flatten (fst (List.split ls)), cc ls)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 94158979..fb3701f3 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -277,7 +277,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
(fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id)
(loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool)
- (ctx : eval_ctx) : SA.expression option =
+ (ctx : eval_ctx) : SA.expression =
log#ldebug
(lazy
("evaluate_function_symbolic_synthesize_backward_from_return:"
@@ -477,8 +477,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
(* Generate the Return node *)
let return_expr =
match loop_id with
- | None -> Some (SA.Return (ctx, None))
- | Some loop_id -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
+ | None -> SA.Return (ctx, None)
+ | Some loop_id -> SA.ReturnWithLoop (loop_id, inside_loop)
in
(* Apply *)
cc return_expr
@@ -486,12 +486,12 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
(** Evaluate a function with the symbolic interpreter.
We return:
- - the list of symbolic values introduced for the input values (this is useful
- for the synthesis)
+ - the list of symbolic values introduced for the input values (this is
+ useful for the synthesis)
- the symbolic AST generated by the symbolic execution
*)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
- (fdef : fun_decl) : symbolic_value list * SA.expression option =
+let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
+ symbolic_value list * SA.expression =
(* Debug *)
let name_to_string () =
Print.Types.name_to_string
@@ -518,101 +518,92 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
match res with
| Return | LoopReturn _ ->
- if synthesize then
- (* We have to "play different endings":
- * - one execution for the forward function
- * - one execution per backward function
- * We then group everything together.
- *)
- (* There are two cases:
- * - if this is a forward translation, we retrieve the returned value.
- * - if this is a backward translation, we introduce "return"
- * abstractions to consume the return value, then end all the
- * abstractions up to the one in which we are interested.
- *)
- (* Forward translation: retrieve the returned value *)
- let fwd_e =
- (* Pop the frame and retrieve the returned value at the same time *)
- let pop_return_value = true in
- let ret_value, ctx, cc_pop =
- pop_frame config fdef.item_meta.span pop_return_value ctx
- in
- (* Generate the Return node *)
- cc_pop (Some (SA.Return (ctx, ret_value)))
- in
- let fwd_e = Option.get fwd_e in
- (* Backward translation: introduce "return"
- abstractions to consume the return value, then end all the
- abstractions up to the one in which we are interested.
- *)
- let loop_id =
- match res with
- | Return -> None
- | LoopReturn loop_id -> Some loop_id
- | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
- in
- let is_regular_return = true in
- let inside_loop = Option.is_some loop_id in
- let finish_back_eval back_id =
- Option.get
- (evaluate_function_symbolic_synthesize_backward_from_return config
- fdef inst_sg back_id loop_id is_regular_return inside_loop ctx)
- in
- let back_el =
- RegionGroupId.mapi
- (fun gid _ -> (gid, finish_back_eval gid))
- regions_hierarchy
+ (* We have to "play different endings":
+ * - one execution for the forward function
+ * - one execution per backward function
+ * We then group everything together.
+ *)
+ (* There are two cases:
+ * - if this is a forward translation, we retrieve the returned value.
+ * - if this is a backward translation, we introduce "return"
+ * abstractions to consume the return value, then end all the
+ * abstractions up to the one in which we are interested.
+ *)
+ (* Forward translation: retrieve the returned value *)
+ let fwd_e =
+ (* Pop the frame and retrieve the returned value at the same time *)
+ let pop_return_value = true in
+ let ret_value, ctx, cc_pop =
+ pop_frame config fdef.item_meta.span pop_return_value ctx
in
- let back_el = RegionGroupId.Map.of_list back_el in
- (* Put everything together *)
- synthesize_forward_end ctx0 None fwd_e back_el
- else None
+ (* Generate the Return node *)
+ cc_pop (SA.Return (ctx, ret_value))
+ in
+ (* Backward translation: introduce "return"
+ abstractions to consume the return value, then end all the
+ abstractions up to the one in which we are interested.
+ *)
+ let loop_id =
+ match res with
+ | Return -> None
+ | LoopReturn loop_id -> Some loop_id
+ | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+ in
+ let is_regular_return = true in
+ let inside_loop = Option.is_some loop_id in
+ let finish_back_eval back_id =
+ evaluate_function_symbolic_synthesize_backward_from_return config fdef
+ inst_sg back_id loop_id is_regular_return inside_loop ctx
+ in
+ let back_el =
+ RegionGroupId.mapi
+ (fun gid _ -> (gid, finish_back_eval gid))
+ regions_hierarchy
+ in
+ let back_el = RegionGroupId.Map.of_list back_el in
+ (* Put everything together *)
+ synthesize_forward_end ctx0 None fwd_e back_el
| EndEnterLoop (loop_id, loop_input_values)
| EndContinue (loop_id, loop_input_values) ->
(* Similar to [Return]: we have to play different endings *)
- if synthesize then
- let inside_loop =
- match res with
- | EndEnterLoop _ -> false
- | EndContinue _ -> true
- | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
- in
- (* Forward translation *)
- let fwd_e =
- (* Pop the frame - there is no returned value to pop: in the
- translation we will simply call the loop function *)
- let pop_return_value = false in
- let _ret_value, _ctx, cc_pop =
- pop_frame config fdef.item_meta.span pop_return_value ctx
- in
- (* Generate the Return node *)
- cc_pop (Some (SA.ReturnWithLoop (loop_id, inside_loop)))
- in
- let fwd_e = Option.get fwd_e in
- (* Backward translation: introduce "return"
- abstractions to consume the return value, then end all the
- abstractions up to the one in which we are interested.
- *)
- let is_regular_return = false in
- let finish_back_eval back_id =
- Option.get
- (evaluate_function_symbolic_synthesize_backward_from_return config
- fdef inst_sg back_id (Some loop_id) is_regular_return
- inside_loop ctx)
- in
- let back_el =
- RegionGroupId.mapi
- (fun gid _ -> (gid, finish_back_eval gid))
- regions_hierarchy
+ let inside_loop =
+ match res with
+ | EndEnterLoop _ -> false
+ | EndContinue _ -> true
+ | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+ in
+ (* Forward translation *)
+ let fwd_e =
+ (* Pop the frame - there is no returned value to pop: in the
+ translation we will simply call the loop function *)
+ let pop_return_value = false in
+ let _ret_value, _ctx, cc_pop =
+ pop_frame config fdef.item_meta.span pop_return_value ctx
in
- let back_el = RegionGroupId.Map.of_list back_el in
- (* Put everything together *)
- synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
- else None
+ (* Generate the Return node *)
+ cc_pop (SA.ReturnWithLoop (loop_id, inside_loop))
+ in
+ (* Backward translation: introduce "return"
+ abstractions to consume the return value, then end all the
+ abstractions up to the one in which we are interested.
+ *)
+ let is_regular_return = false in
+ let finish_back_eval back_id =
+ evaluate_function_symbolic_synthesize_backward_from_return config fdef
+ inst_sg back_id (Some loop_id) is_regular_return inside_loop ctx
+ in
+ let back_el =
+ RegionGroupId.mapi
+ (fun gid _ -> (gid, finish_back_eval gid))
+ regions_hierarchy
+ in
+ let back_el = RegionGroupId.Map.of_list back_el in
+ (* Put everything together *)
+ synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
| Panic ->
(* Note that as we explore all the execution branches, one of
* the executions can lead to a panic *)
- if synthesize then Some SA.Panic else None
+ SA.Panic
| Unit | Break _ | Continue _ ->
craise __FILE__ __LINE__ fdef.item_meta.span
("evaluate_function_symbolic failed on: " ^ name_to_string ())
@@ -624,12 +615,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
let ctx_resl, cc =
eval_function_body config (Option.get fdef.body).body ctx
in
- let el =
- List.map Option.get
- (List.map (fun (ctx, res) -> finish res ctx) ctx_resl)
- in
- cc (Some el)
- with CFailure (span, msg) -> Some (Error (span, msg))
+ let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+ cc el
+ with CFailure (span, msg) -> Error (span, msg)
in
(* Return *)
(input_svs, symbolic)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 4393e89f..41190618 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -446,9 +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) option -> eval_result)
- =
+ (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression) =
fun ctx ->
(* Compute the expanded value *)
let original_sv = sv in
@@ -465,9 +463,8 @@ let expand_symbolic_bool (config : config) (span : Meta.span)
let ctx_true = apply_expansion see_true in
let ctx_false = apply_expansion see_false in
(* Compute the continuation to build the expression *)
- let cf e =
- let el = match e with Some (a, b) -> Some [ a; b ] | None -> None in
- S.synthesize_symbolic_expansion span sv sv_place seel el
+ let cf (e0, e1) =
+ S.synthesize_symbolic_expansion span sv sv_place seel [ e0; e1 ]
in
(* Return *)
((ctx_true, ctx_false), cf)
@@ -535,8 +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 option -> 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));
@@ -571,8 +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) option ->
- 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;
@@ -589,13 +584,10 @@ let expand_symbolic_int (config : config) (span : Meta.span)
in
let ctx_otherwise = ctx in
(* Update the symbolic ast *)
- let cf e =
- match e with
- | None -> None
- | Some (el, e) ->
- let seel = List.map (fun x -> Some x) seel in
- S.synthesize_symbolic_expansion span sv sv_place (seel @ [ None ])
- (Some (el @ [ e ]))
+ let cf (el, e) =
+ let seel = List.map (fun x -> Some x) seel in
+ S.synthesize_symbolic_expansion span sv sv_place (seel @ [ None ])
+ (el @ [ e ])
in
((ctx_branches, ctx_otherwise), cf)
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 7f8c3a0a..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 option -> 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) option -> eval_result)
+ (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression)
(** Symbolic integers are expanded upon evaluating a [SwitchInt].
@@ -76,8 +75,7 @@ val expand_symbolic_int :
scalar_value list ->
eval_ctx ->
(eval_ctx list * eval_ctx)
- * ((SymbolicAst.expression list * SymbolicAst.expression) option ->
- 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 56c0ab5f..5088d29a 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
@@ -287,16 +290,12 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
let v = mk_fresh_symbolic_typed_value span ty in
(* Wrap the generated expression *)
let cf e =
- match e with
- | None -> None
- | Some e ->
- Some
- (SymbolicAst.IntroSymbolic
- ( ctx0,
- None,
- value_as_symbolic span v.value,
- SymbolicAst.VaTraitConstValue (trait_ref, const_name),
- e ))
+ SymbolicAst.IntroSymbolic
+ ( ctx0,
+ None,
+ value_as_symbolic span v.value,
+ SymbolicAst.VaTraitConstValue (trait_ref, const_name),
+ e )
in
(v, ctx, cf)
| CVar vid ->
@@ -321,20 +320,16 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
in
(* We have to wrap the generated expression *)
let cf e =
- match e with
- | None -> None
- | Some e ->
- (* If we are synthesizing a symbolic AST, it means that we are in symbolic
- mode: the value of the const generic is necessarily symbolic. *)
- sanity_check __FILE__ __LINE__ (is_symbolic cv.value) span;
- (* *)
- Some
- (SymbolicAst.IntroSymbolic
- ( ctx0,
- None,
- value_as_symbolic span cv.value,
- SymbolicAst.VaCgValue vid,
- e ))
+ (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+ mode: the value of the const generic is necessarily symbolic. *)
+ sanity_check __FILE__ __LINE__ (is_symbolic cv.value) span;
+ (* *)
+ SymbolicAst.IntroSymbolic
+ ( ctx0,
+ None,
+ value_as_symbolic span cv.value,
+ SymbolicAst.VaCgValue vid,
+ e )
in
(cv, ctx, cf)
| CFnPtr _ ->
@@ -371,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
@@ -393,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 *)
@@ -402,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
@@ -413,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 *)
@@ -463,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 *)
@@ -489,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
@@ -573,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 *)
@@ -583,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 *)
@@ -631,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
@@ -640,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.
@@ -723,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 *)
@@ -783,13 +798,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
let saggregated = mk_fresh_symbolic_typed_value span ty in
(* Update the symbolic ast *)
let cf e =
- match e with
- | None -> None
- | Some e ->
- (* Introduce the symbolic value in the AST *)
- let sv = ValuesUtils.value_as_symbolic span saggregated.value in
- Some
- (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))
+ (* Introduce the symbolic value in the AST *)
+ let sv = ValuesUtils.value_as_symbolic span saggregated.value in
+ SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)
in
(saggregated, cf)
| AggregatedClosure _ ->
@@ -799,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 90161196..c33c34a6 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -64,10 +64,7 @@ let eval_loop_concrete (span : Meta.span) (eval_loop_body : stl_cm_fun) :
the loop body at least once *)
let ctx_resl = rec_eval_loop_body ctx (Continue 0) in
(* If we evaluate in concrete mode, we shouldn't have to generate any symbolic expression *)
- let cf el =
- sanity_check __FILE__ __LINE__ (el = None) span;
- None
- in
+ let cf _ = internal_error __FILE__ __LINE__ span in
(ctx_resl, cf)
(** Auxiliary function for {!eval_loop_symbolic}.
@@ -92,7 +89,8 @@ let eval_loop_symbolic_synthesize_fun_end (config : config) (span : span)
(loop_id : LoopId.id) (init_ctx : eval_ctx) (fixed_ids : ids_sets)
(fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list)
(rg_to_abs : AbstractionId.id RegionGroupId.Map.t) :
- ((eval_ctx * statement_eval_res) * (eval_result -> eval_result))
+ ((eval_ctx * statement_eval_res)
+ * (SymbolicAst.expression -> SymbolicAst.expression))
* borrow_loan_corresp =
(* First, preemptively end borrows/move values by matching the current
context with the target context *)
@@ -212,7 +210,7 @@ let eval_loop_symbolic_synthesize_loop_body (config : config) (span : span)
(fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list)
(fp_bl_corresp : borrow_loan_corresp) :
(eval_ctx * statement_eval_res) list
- * (SymbolicAst.expression list option -> 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
@@ -252,16 +250,9 @@ let eval_loop_symbolic_synthesize_loop_body (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 option) : eval_result =
- match el with
- | None -> None
- | Some el ->
- let el =
- List.map
- (fun (cf, e) -> Option.get (cf (Some e)))
- (List.combine cfl el)
- in
- cf_loop (Some el)
+ 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
(ctx_resl, cc)
@@ -380,17 +371,14 @@ let eval_loop_symbolic (config : config) (span : span)
in
(* Put everything together *)
- let cc (el : SymbolicAst.expression list option) =
+ let cc (el : SymbolicAst.expression list) =
match el with
- | None -> None
- | Some el -> (
- match el with
- | [] -> internal_error __FILE__ __LINE__ span
- | e :: el ->
- let fun_end_expr = cf_fun_end (Some e) in
- let loop_expr = cf_loop_body (Some el) in
- S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
- fun_end_expr loop_expr span)
+ | [] -> internal_error __FILE__ __LINE__ span
+ | e :: el ->
+ let fun_end_expr = cf_fun_end e in
+ let loop_expr = cf_loop_body el in
+ S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
+ fun_end_expr loop_expr span
in
(res_fun_end :: resl_loop_body, cc)
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index b68f2a4d..735f3743 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -371,19 +371,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
(* Synthesize *)
let cf e =
- match e with
- | None -> None
- | Some e ->
- (* Add the let-bindings which introduce the fresh symbolic values *)
- Some
- (List.fold_left
- (fun e (sid, v) ->
- let v = mk_typed_value_from_symbolic_value v in
- let sv =
- SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values
- in
- SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
- e !sid_subst)
+ (* Add the let-bindings which introduce the fresh symbolic values *)
+ List.fold_left
+ (fun e (sid, v) ->
+ let v = mk_typed_value_from_symbolic_value v in
+ let sv = SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values in
+ SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
+ e !sid_subst
in
(ctx, cf)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index b2de3b22..8a924a0a 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -525,7 +525,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 =
@@ -631,7 +632,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 283a711d..27f503bc 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));
@@ -1033,7 +1037,7 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
let func = { func = FunId (FRegular global.body); generics } in
let call = { func = FnOpRegular func; args = []; dest } in
eval_transparent_function_call_concrete config span global.body call ctx
- | SymbolicMode -> (
+ | SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
* defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
@@ -1056,12 +1060,8 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
dest ctx
in
( [ (ctx, Unit) ],
- fun el ->
- match el with
- | Some [ e ] ->
- (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e)
- | Some _ -> internal_error __FILE__ __LINE__ span
- | _ -> None ))
+ cc_singleton __FILE__ __LINE__ span
+ (cc_comp (S.synthesize_global_eval gid generics sval) cc) )
(** Evaluate a switch *)
and eval_switch (config : config) (span : Meta.span) (switch : switch) :
@@ -1102,8 +1102,7 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
in
let cc el =
match cf_branches el with
- | None -> None
- | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false))
+ | [ e_true; e_false ] -> cf_bool (e_true, e_false)
| _ -> internal_error __FILE__ __LINE__ span
in
(ctx_resl, cc)
@@ -1158,11 +1157,8 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
(resl_branches @ [ resl_otherwise ])
in
let cc el =
- match el with
- | None -> None
- | Some el ->
- let el, e_otherwise = Collections.List.pop_last el in
- cf_int (Some (el, e_otherwise))
+ let el, e_otherwise = Collections.List.pop_last el in
+ cf_int (el, e_otherwise)
in
(resl, cc_comp cc cf)
| _ -> craise __FILE__ __LINE__ span "Inconsistent state"
@@ -1235,7 +1231,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
match func.func with
| FunId (FRegular fid) ->
eval_transparent_function_call_concrete config span fid call ctx
- | FunId (FAssumed fid) -> (
+ | FunId (FAssumed fid) ->
(* Continue - note that we do as if the function call has been successful,
* by giving {!Unit} to the continuation, because we place us in the case
* where we haven't panicked. Of course, the translation needs to take the
@@ -1243,12 +1239,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
let ctx, cc =
eval_assumed_function_call_concrete config span fid call ctx
in
- ( [ (ctx, Unit) ],
- fun el ->
- match el with
- | Some [ e ] -> cc (Some e)
- | Some _ -> internal_error __FILE__ __LINE__ span
- | _ -> None ))
+ ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc)
| TraitMethod _ -> craise __FILE__ __LINE__ span "Unimplemented")
and eval_function_call_symbolic (config : config) (span : Meta.span)
@@ -1351,13 +1342,7 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span)
ctx_resl
in
let ctx_resl, cfl = List.split ctx_resl_cfl in
- let cf_pop el =
- match el with
- | None -> None
- | Some el ->
- Some
- (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
- in
+ let cf_pop el = List.map2 (fun cf e -> cf e) cfl el in
(* Continue *)
(ctx_resl, cc_comp cc cf_pop)
@@ -1620,11 +1605,6 @@ and eval_function_body (config : config) (body : statement) : stl_cm_fun =
ctx_resl
in
let ctx_resl, cfl = List.split ctx_res_cfl in
- let cf_end el =
- match el with
- | None -> None
- | Some el ->
- Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
- in
+ let cf_end el = List.map2 (fun cf e -> cf e) cfl el in
(* Compose and continue *)
(ctx_resl, cc_comp cf_body cf_end)
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.
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index ae701c33..b15ab38a 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -25,110 +25,101 @@ let mk_espan (m : espan) (e : expression) : expression = Meta (m, e)
let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
(place : mplace option) (seel : symbolic_expansion option list)
- (el : expression list option) : expression option =
- match el with
- | None -> None
- | Some el ->
- let ls = List.combine seel el in
- (* Match on the symbolic value type to know which can of expansion happened *)
- let expansion =
- match sv.sv_ty with
- | TLiteral TBool -> (
- (* Boolean expansion: there should be two branches *)
- match ls with
- | [
- (Some (SeLiteral (VBool true)), true_exp);
- (Some (SeLiteral (VBool false)), false_exp);
- ] ->
- ExpandBool (true_exp, false_exp)
- | _ -> craise __FILE__ __LINE__ span "Ill-formed boolean expansion")
- | TLiteral (TInteger int_ty) ->
- (* Switch over an integer: split between the "regular" branches
- and the "otherwise" branch (which should be the last branch) *)
- let branches, otherwise = Collections.List.pop_last ls in
- (* For all the regular branches, the symbolic value should have
- * been expanded to a constant *)
- let get_scalar (see : symbolic_expansion option) : scalar_value =
- match see with
- | Some (SeLiteral (VScalar cv)) ->
- sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) span;
- cv
- | _ -> craise __FILE__ __LINE__ span "Unreachable"
- in
- let branches =
- List.map (fun (see, exp) -> (get_scalar see, exp)) branches
- in
- (* For the otherwise branch, the symbolic value should have been left
- * unchanged *)
- let otherwise_see, otherwise = otherwise in
- sanity_check __FILE__ __LINE__ (otherwise_see = None) span;
- (* Return *)
- ExpandInt (int_ty, branches, otherwise)
- | TAdt (_, _) ->
- (* Branching: it is necessarily an enumeration expansion *)
- let get_variant (see : symbolic_expansion option) :
- VariantId.id option * symbolic_value list =
- match see with
- | Some (SeAdt (vid, fields)) -> (vid, fields)
- | _ ->
- craise __FILE__ __LINE__ span
- "Ill-formed branching ADT expansion"
- in
- let exp =
- List.map
- (fun (see, exp) ->
- let vid, fields = get_variant see in
- (vid, fields, exp))
- ls
- in
- ExpandAdt exp
- | TRef (_, _, _) -> (
- (* Reference expansion: there should be one branch *)
- match ls with
- | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
- | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
- | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _
- ->
- craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
- in
- Some (Expansion (place, sv, expansion))
+ (el : expression list) : expression =
+ let ls = List.combine seel el in
+ (* Match on the symbolic value type to know which can of expansion happened *)
+ let expansion =
+ match sv.sv_ty with
+ | TLiteral TBool -> (
+ (* Boolean expansion: there should be two branches *)
+ match ls with
+ | [
+ (Some (SeLiteral (VBool true)), true_exp);
+ (Some (SeLiteral (VBool false)), false_exp);
+ ] ->
+ ExpandBool (true_exp, false_exp)
+ | _ -> craise __FILE__ __LINE__ span "Ill-formed boolean expansion")
+ | TLiteral (TInteger int_ty) ->
+ (* Switch over an integer: split between the "regular" branches
+ and the "otherwise" branch (which should be the last branch) *)
+ let branches, otherwise = Collections.List.pop_last ls in
+ (* For all the regular branches, the symbolic value should have
+ * been expanded to a constant *)
+ let get_scalar (see : symbolic_expansion option) : scalar_value =
+ match see with
+ | Some (SeLiteral (VScalar cv)) ->
+ sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) span;
+ cv
+ | _ -> craise __FILE__ __LINE__ span "Unreachable"
+ in
+ let branches =
+ List.map (fun (see, exp) -> (get_scalar see, exp)) branches
+ in
+ (* For the otherwise branch, the symbolic value should have been left
+ * unchanged *)
+ let otherwise_see, otherwise = otherwise in
+ sanity_check __FILE__ __LINE__ (otherwise_see = None) span;
+ (* Return *)
+ ExpandInt (int_ty, branches, otherwise)
+ | TAdt (_, _) ->
+ (* Branching: it is necessarily an enumeration expansion *)
+ let get_variant (see : symbolic_expansion option) :
+ VariantId.id option * symbolic_value list =
+ match see with
+ | Some (SeAdt (vid, fields)) -> (vid, fields)
+ | _ ->
+ craise __FILE__ __LINE__ span "Ill-formed branching ADT expansion"
+ in
+ let exp =
+ List.map
+ (fun (see, exp) ->
+ let vid, fields = get_variant see in
+ (vid, fields, exp))
+ ls
+ in
+ ExpandAdt exp
+ | TRef (_, _, _) -> (
+ (* Reference expansion: there should be one branch *)
+ match ls with
+ | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
+ | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
+ | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
+ craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
+ in
+ Expansion (place, sv, expansion)
let synthesize_symbolic_expansion_no_branching (span : Meta.span)
(sv : symbolic_value) (place : mplace option) (see : symbolic_expansion)
- (e : expression option) : expression option =
- let el = Option.map (fun e -> [ e ]) e in
- synthesize_symbolic_expansion span sv place [ Some see ] el
+ (e : expression) : expression =
+ synthesize_symbolic_expansion span sv place [ Some see ] [ e ]
let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
(sg : fun_sig option) (regions_hierarchy : region_var_groups)
(abstractions : AbstractionId.id list) (generics : generic_args)
(trait_method_generics : (generic_args * trait_instance_id) option)
(args : typed_value list) (args_places : mplace option list)
- (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
- : expression option =
- Option.map
- (fun e ->
- let call =
- {
- call_id;
- ctx;
- sg;
- regions_hierarchy;
- abstractions;
- generics;
- trait_method_generics;
- args;
- dest;
- args_places;
- dest_place;
- }
- in
- FunCall (call, e))
- e
+ (dest : symbolic_value) (dest_place : mplace option) (e : expression) :
+ expression =
+ let call =
+ {
+ call_id;
+ ctx;
+ sg;
+ regions_hierarchy;
+ abstractions;
+ generics;
+ trait_method_generics;
+ args;
+ dest;
+ args_places;
+ dest_place;
+ }
+ in
+ FunCall (call, e)
let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args)
- (dest : symbolic_value) (e : expression option) : expression option =
- Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e
+ (dest : symbolic_value) (e : expression) : expression =
+ EvalGlobal (gid, generics, dest, e)
let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
(call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig)
@@ -136,8 +127,8 @@ let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
(abstractions : AbstractionId.id list) (generics : generic_args)
(trait_method_generics : (generic_args * trait_instance_id) option)
(args : typed_value list) (args_places : mplace option list)
- (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
- : expression option =
+ (dest : symbolic_value) (dest_place : mplace option) (e : expression) :
+ expression =
synthesize_function_call
(Fun (fun_id, call_id))
ctx (Some sg) regions_hierarchy abstractions generics trait_method_generics
@@ -145,7 +136,7 @@ let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop)
(arg : typed_value) (arg_place : mplace option) (dest : symbolic_value)
- (dest_place : mplace option) (e : expression option) : expression option =
+ (dest_place : mplace option) (e : expression) : expression =
let generics = empty_generic_args in
synthesize_function_call (Unop unop) ctx None [] [] generics None [ arg ]
[ arg_place ] dest dest_place e
@@ -153,50 +144,43 @@ let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop)
let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : binop)
(arg0 : typed_value) (arg0_place : mplace option) (arg1 : typed_value)
(arg1_place : mplace option) (dest : symbolic_value)
- (dest_place : mplace option) (e : expression option) : expression option =
+ (dest_place : mplace option) (e : expression) : expression =
let generics = empty_generic_args in
synthesize_function_call (Binop binop) ctx None [] [] generics None
[ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e
let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : abs)
- (e : expression option) : expression option =
- Option.map (fun e -> EndAbstraction (ctx, abs, e)) e
+ (e : expression) : expression =
+ EndAbstraction (ctx, abs, e)
let synthesize_assignment (ctx : Contexts.eval_ctx) (lplace : mplace)
- (rvalue : typed_value) (rplace : mplace option) (e : expression option) :
- expression option =
- Option.map (fun e -> Meta (Assignment (ctx, lplace, rvalue, rplace), e)) e
+ (rvalue : typed_value) (rplace : mplace option) (e : expression) :
+ expression =
+ Meta (Assignment (ctx, lplace, rvalue, rplace), e)
let synthesize_assertion (ctx : Contexts.eval_ctx) (v : typed_value)
- (e : expression option) =
- Option.map (fun e -> Assertion (ctx, v, e)) e
+ (e : expression) =
+ Assertion (ctx, v, e)
let synthesize_forward_end (ctx : Contexts.eval_ctx)
(loop_input_values : typed_value SymbolicValueId.Map.t option)
(e : expression) (el : expression RegionGroupId.Map.t) =
- Some (ForwardEnd (ctx, loop_input_values, e, el))
+ ForwardEnd (ctx, loop_input_values, e, el)
let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
(fresh_svalues : SymbolicValueId.Set.t)
- (rg_to_given_back_tys : ty list RegionGroupId.Map.t)
- (end_expr : expression option) (loop_expr : expression option)
- (span : Meta.span) : expression option =
- match (end_expr, loop_expr) with
- | None, None -> None
- | Some end_expr, Some loop_expr ->
- Some
- (Loop
- {
- loop_id;
- input_svalues;
- fresh_svalues;
- rg_to_given_back_tys;
- end_expr;
- loop_expr;
- span;
- })
- | _ -> craise __FILE__ __LINE__ span "Unreachable"
-
-let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
- expression option =
- match e with None -> None | Some e -> Some (Meta (Snapshot ctx, e))
+ (rg_to_given_back_tys : ty list RegionGroupId.Map.t) (end_expr : expression)
+ (loop_expr : expression) (span : Meta.span) : expression =
+ Loop
+ {
+ loop_id;
+ input_svalues;
+ fresh_svalues;
+ rg_to_given_back_tys;
+ end_expr;
+ loop_expr;
+ span;
+ }
+
+let save_snapshot (ctx : Contexts.eval_ctx) (e : expression) : expression =
+ Meta (Snapshot ctx, e)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 02d495c0..0f887ec8 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,9 +31,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
| None -> None
| Some _ ->
(* Evaluate *)
- let synthesize = true in
- let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
- Some (inputs, Option.get symb)
+ let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
+ Some (inputs, symb)
(** Translate a function, by generating its forward and backward translations.
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index 33206fe5..6d638644 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
[Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 813:
+[Error] In file Translate.ml, line 812:
Mutually recursive trait declarations are not supported
Uncaught exception:
(Failure
- "In file Translate.ml, line 813:\
- \nIn file Translate.ml, line 813:\
+ "In file Translate.ml, line 812:\
+ \nIn file Translate.ml, line 812:\
\nMutually recursive trait declarations are not supported")
Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1502, characters 5-42
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42
Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61