diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Cps.ml | 47 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 188 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 25 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 7 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 50 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 37 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 20 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 44 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 238 | ||||
| -rw-r--r-- | compiler/Translate.ml | 5 |
10 files changed, 276 insertions, 385 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml index 142c2b08..c414652d 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -35,23 +35,27 @@ type statement_eval_res = *) [@@deriving show] -type eval_result = SymbolicAst.expression option +(* 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 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,21 +94,8 @@ 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 (** It happens that we need to concatenate lists of results, for instance when evaluating the branches of a match. When applying @@ -114,15 +105,11 @@ let cc_singleton file line span cf 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 *) @@ -134,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 388d7382..3c264c6e 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -447,8 +447,7 @@ 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) - = + * (SymbolicAst.expression * SymbolicAst.expression -> eval_result) = fun ctx -> (* Compute the expanded value *) let original_sv = sv in @@ -465,9 +464,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 +533,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 * (SymbolicAst.expression list -> eval_result) = fun ctx -> (* Debug *) log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv)); @@ -571,8 +568,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) = + * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result) = fun ctx -> (* Sanity check *) sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) span; @@ -589,13 +585,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..9b5ebed3 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 * (SymbolicAst.expression list -> eval_result) (** Expand a symbolic boolean. @@ -51,7 +51,7 @@ val expand_symbolic_bool : SA.mplace option -> eval_ctx -> (eval_ctx * eval_ctx) - * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result) + * (SymbolicAst.expression * SymbolicAst.expression -> eval_result) (** Symbolic integers are expanded upon evaluating a [SwitchInt]. @@ -76,8 +76,7 @@ val expand_symbolic_int : scalar_value list -> eval_ctx -> (eval_ctx list * eval_ctx) - * ((SymbolicAst.expression list * SymbolicAst.expression) option -> - eval_result) + * (SymbolicAst.expression list * SymbolicAst.expression -> eval_result) (** 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 2223897c..51c8108e 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -287,16 +287,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 +317,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 _ -> @@ -783,13 +775,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 _ -> diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 776cb6fa..4755f0e9 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) (** Evaluate a loop in symbolic mode *) @@ -161,7 +158,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 option -> eval_result) = + * (SymbolicAst.expression list -> eval_result) = (* First, evaluate the loop body starting from the **fixed-point** context *) let ctx_resl, cf_loop = eval_loop_body fp_ctx in @@ -201,16 +198,9 @@ 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 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) : eval_result = + let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in + cf_loop el in (ctx_resl, cc) @@ -296,17 +286,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 1a0bb090..603dc608 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -425,19 +425,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/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index c6a65757..4b4bac62 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1035,7 +1035,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 @@ -1058,12 +1058,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) : @@ -1104,8 +1100,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) @@ -1160,11 +1155,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" @@ -1237,7 +1229,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 @@ -1245,12 +1237,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) @@ -1353,13 +1340,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) @@ -1622,11 +1603,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/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. |