diff options
| -rw-r--r-- | src/InterpreterExpansion.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 54 | ||||
| -rw-r--r-- | src/Synthesis.ml | 6 |
3 files changed, 56 insertions, 6 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 46398c84..7366a819 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -166,6 +166,8 @@ let replace_symbolic_values (at_most_once : bool) (** Apply a symbolic expansion to a context, by replacing the original symbolic value with its expanded value. Is valid only if the expansion is not a borrow (i.e., an adt...). + + This function does update the synthesis. *) let apply_symbolic_expansion_non_borrow (config : C.config) (original_sv : V.symbolic_value) (expansion : symbolic_expansion) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 83d531a0..15bfb6e7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -38,6 +38,51 @@ let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) let ctx = write_place_unwrap config Write p v ctx in ctx +(** Evaluates an assertion. + + In the case the boolean under scrutinee is symbolic, we synthesize + a call to `assert ...` then continue in the success branch (and thus + expand the boolean to `true`). + *) +let eval_assertion (config : C.config) (ctx : C.eval_ctx) + (assertion : A.assertion) : C.eval_ctx eval_result = + (* There may be a symbolic expansion, so don't fully evaluate the operand + * (if we moved the value, we can't expand it because it is hanging in + * thin air, outside of the environment... *) + let ctx, v = eval_operand_prepare config ctx assertion.cond in + assert (v.ty = T.Bool); + let symbolic_mode = config.mode = C.SymbolicMode in + (* We make a choice here: we could completely decouple the concrete and + * symbolic executions here but choose not to. In the case where we + * know the concrete value of the boolean we test, we use this value + * even if we are in symbolic mode. Note that this case should be + * extremely rare... *) + match v.value with + | Concrete (Bool b) -> + (* There won't be any symbolic expansions: fully evaluate the operand *) + let ctx, v' = eval_operand config ctx assertion.cond in + assert (v' = v); + (* Branch *) + if b = assertion.expected then Ok ctx + else ( + if symbolic_mode then S.synthesize_panic (); + Error Panic) + | Symbolic sv -> + (* We register the fact that we called an assertion (the synthesized + * code will then check that the assert succeeded) then continue + * with the succeeding branch: we thus expand the symbolic value with + * `true` *) + S.synthesize_assert v; + let see = SeConcrete (V.Bool true) in + let ctx = + apply_symbolic_expansion_non_borrow config sv.V.svalue see ctx + in + S.synthesize_symbolic_expansion_no_branching sv.V.svalue see; + (* We can finally fully evaluate the operand *) + let ctx, _ = eval_operand config ctx assertion.cond in + Ok ctx + | _ -> failwith ("Expected a boolean, got: " ^ V.show_value v.value) + (** Updates the discriminant of a value at a given place. There are two situations: @@ -500,12 +545,9 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) [ Ok (set_discriminant config ctx p variant_id) ] | A.Drop p -> [ Ok (drop_value config ctx p, Unit) ] | A.Assert assertion -> ( - let ctx, v = eval_operand config ctx assertion.cond in - assert (v.ty = T.Bool); - match v.value with - | Concrete (Bool b) -> - if b = assertion.expected then [ Ok (ctx, Unit) ] else [ Error Panic ] - | _ -> failwith ("Expected a boolean, got: " ^ V.show_value v.value)) + match eval_assertion config ctx assertion with + | Ok ctx -> [ Ok (ctx, Unit) ] + | Error e -> [ Error e ]) | A.Call call -> eval_function_call config ctx call | A.Panic -> [ Error Panic ] | A.Return -> [ Ok (ctx, Return) ] diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 85834e7a..79fa4065 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -23,6 +23,8 @@ open InterpreterProjectors * `s := op1 + op2` * *) +(* TODO: error Panic *) + (** Synthesize code for a symbolic expansion which doesn't lead to branching (i.e., applied on a value which is not an enumeration with several variants). *) @@ -66,3 +68,7 @@ let synthesize_function_call (_fid : A.fun_id) (_args : V.typed_value list) (_dest : E.place) (_res : V.symbolic_value) : unit = () + +let synthesize_panic () : unit = () + +let synthesize_assert (v : V.typed_value) : unit = () |