diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterStatements.ml | 186 | ||||
| -rw-r--r-- | src/Synthesis.ml | 4 |
2 files changed, 101 insertions, 89 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index f6223fa8..c889281b 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -963,10 +963,9 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id) cc cf ctx (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) -and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) - (fid : A.FunDefId.id) (region_params : T.erased_region list) - (type_params : T.ety list) (args : E.operand list) (dest : E.place) : - st_cm_fun = +and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDefId.id) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> (* Retrieve the (correctly instantiated) signature *) let def = C.ctx_lookup_fun_def ctx fid in @@ -977,7 +976,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) (* Sanity check *) assert (List.length args = def.A.arg_count); (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config ctx (A.Local fid) inst_sg + eval_function_call_symbolic_from_inst_sig config (A.Local fid) inst_sg region_params type_params args dest cf ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -986,7 +985,7 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) calls in symbolic mode: only their signatures matter. *) and eval_function_call_symbolic_from_inst_sig (config : C.config) - (ctx : C.eval_ctx) (fid : A.fun_id) (inst_sg : A.inst_fun_sig) + (fid : A.fun_id) (inst_sg : A.inst_fun_sig) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = fun cf ctx -> @@ -998,55 +997,74 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let ret_av regions = mk_aproj_loans_value_from_symbolic_value regions ret_spc in + (* Evaluate the input operands *) - let ctx, args = eval_operands config ctx args in - let args_with_rtypes = List.combine args inst_sg.A.inputs in - (* Check the type of the input arguments *) - assert ( - List.for_all - (fun ((arg, rty) : V.typed_value * T.rty) -> - arg.V.ty = Subst.erase_regions rty) - args_with_rtypes); - (* Check that the input arguments don't contain symbolic values that can't - * be fed to functions (i.e., symbolic values output from function return - * values and which contain borrows of borrows can't be used as function - * inputs *) - assert ( - List.for_all - (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args); - (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) - let empty_absl = - create_empty_abstractions_from_abs_region_groups V.FunCall - inst_sg.A.regions_hierarchy - in - (* Add the avalues to the abstractions and insert them in the context *) - let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = - (* Project over the input values *) - let ctx, args_projs = - List.fold_left_map - (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config ctx abs.regions - abs.ancestors_regions arg arg_rty) - ctx args_with_rtypes + let cc = eval_operands config args in + + (* Generate the abstractions and insert them in the context *) + let cf_call cf (args : V.typed_value list) : m_fun = + fun ctx -> + let args_with_rtypes = List.combine args inst_sg.A.inputs in + + (* Check the type of the input arguments *) + assert ( + List.for_all + (fun ((arg, rty) : V.typed_value * T.rty) -> + arg.V.ty = Subst.erase_regions rty) + args_with_rtypes); + (* Check that the input arguments don't contain symbolic values that can't + * be fed to functions (i.e., symbolic values output from function return + * values and which contain borrows of borrows can't be used as function + * inputs *) + assert ( + List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args); + + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let empty_absl = + create_empty_abstractions_from_abs_region_groups V.FunCall + inst_sg.A.regions_hierarchy + in + + (* Add the avalues to the abstractions and insert them in the context *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Project over the input values *) + let ctx, args_projs = + List.fold_left_map + (fun ctx (arg, arg_rty) -> + apply_proj_borrows_on_input_value config ctx abs.regions + abs.ancestors_regions arg arg_rty) + ctx args_with_rtypes + in + (* Group the input and output values *) + let avalues = List.append args_projs [ ret_av abs.regions ] in + (* Add the avalues to the abstraction *) + let abs = { abs with avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in + (* Return *) + ctx in - (* Group the input and output values *) - let avalues = List.append args_projs [ ret_av abs.regions ] in - (* Add the avalues to the abstraction *) - let abs = { abs with avalues } in - (* Insert the abstraction in the context *) - let ctx = { ctx with env = Abs abs :: ctx.env } in - (* Return *) - ctx + let ctx = List.fold_left insert_abs ctx empty_absl in + + (* Synthesis *) + S.synthesize_function_call fid region_params type_params args dest ret_spc; + + (* Continue *) + cf ctx in - let ctx = List.fold_left insert_abs ctx empty_absl in + let cc = comp cc cf_call in + (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in - (* Synthesis *) - S.synthesize_function_call fid region_params type_params args dest ret_spc; - (* Return *) - ctx + let cc = comp cc (assign_to_place config ret_value dest) in + + (* 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 + * panic case into account... *) + cc (cf Unit) ctx (** Evaluate a non-local function call in symbolic mode *) and eval_non_local_function_call_symbolic (config : C.config) @@ -1070,25 +1088,24 @@ and eval_non_local_function_call_symbolic (config : C.config) | A.BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config region_params type_params args dest ctx + eval_box_free config region_params type_params args dest (cf Unit) ctx | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined * by the signature of the function: we thus simply generate correctly * instantiated signatures, and delegate the work to an auxiliary function *) - let ctx, inst_sig = + let inst_sig = match fid with - | A.BoxNew -> (ctx, eval_box_new_inst_sig region_params type_params) - | A.BoxDeref -> eval_box_deref_inst_sig region_params type_params ctx - | A.BoxDerefMut -> - eval_box_deref_mut_inst_sig region_params type_params ctx + | A.BoxNew -> eval_box_new_inst_sig region_params type_params + | A.BoxDeref -> eval_box_deref_inst_sig region_params type_params + | A.BoxDerefMut -> eval_box_deref_mut_inst_sig region_params type_params | A.BoxFree -> failwith "Unreachable" (* should have been treated above *) in (* Evaluate the function call *) - eval_function_call_symbolic_from_inst_sig config ctx (A.Assumed fid) - inst_sig region_params type_params args dest + eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig + region_params type_params args dest cf ctx (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` (auxiliary helper for [eval_statement]) *) @@ -1114,46 +1131,45 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id) match config.mode with | C.ConcreteMode -> - eval_non_local_function_call_concrete config ctx fid region_params - type_params args dest + eval_non_local_function_call_concrete config fid region_params type_params + args dest (cf Unit) ctx | C.SymbolicMode -> - Ok - (eval_non_local_function_call_symbolic config ctx fid region_params - type_params args dest) + eval_non_local_function_call_symbolic config fid region_params type_params + args dest cf ctx (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for [eval_statement]) *) and eval_local_function_call (config : C.config) (fid : A.FunDefId.id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : st_cm_fun = - fun cf ctx -> match config.mode with | ConcreteMode -> - eval_local_function_call_concrete config ctx fid region_params type_params + eval_local_function_call_concrete config fid region_params type_params args dest | SymbolicMode -> - [ - Ok - (eval_local_function_call_symbolic config ctx fid region_params - type_params args dest); - ] + eval_local_function_call_symbolic config fid region_params type_params + args dest (** Evaluate a statement seen as a function body (auxiliary helper for [eval_statement]) *) and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = fun cf ctx -> - let res = eval_statement config ctx body in - let finish res = - match res with - | Error err -> Error err - | Ok (ctx, res) -> ( - (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let ctx = greedy_expand_symbolic_values config ctx in - (* Sanity check *) - if config.C.check_invariants then Inv.check_invariants config ctx; - match res with - | Unit | Break _ | Continue _ -> failwith "Inconsistent state" - | Return -> Ok ctx) + let cc = eval_statement config body in + let cf_finish cf res = + (* Note that we *don't* check the result ([Panic], [Return], etc.): we + * delegate the check to the caller. *) + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let cc = greedy_expand_symbolic_values config in + (* Sanity check *) + let cc = + if config.C.check_invariants then + comp_check_ctx cc (Inv.check_invariants config) + else cc + in + + (* Continue *) + cc (cf res) in - List.map finish res + (* Compose and continue *) + comp cc cf_finish cf ctx diff --git a/src/Synthesis.ml b/src/Synthesis.ml index b45c2810..d28a7971 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -75,7 +75,6 @@ let synthesize_eval_rvalue_aggregate (_aggregate_kind : E.aggregate_kind) (_ops : E.operand list) : unit = () -(* let synthesize_function_call (_fid : A.fun_id) (_region_params : T.erased_region list) (_type_params : T.ety list) (_args : V.typed_value list) (_dest : E.place) (_res : V.symbolic_value) : @@ -83,6 +82,3 @@ let synthesize_function_call (_fid : A.fun_id) () (*let synthesize_panic () : unit = ()*) - -let synthesize_assert (_v : V.typed_value) : unit = () - *) |