diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 76 |
1 files changed, 72 insertions, 4 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 496347ff..2636d6d2 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2040,7 +2040,12 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) and eval_function_body (config : C.config) (ctx : C.eval_ctx) (body : A.expression) : (C.eval_ctx, eval_error) result = - raise Unimplemented + match eval_expression config ctx body with + | Error err -> Error err + | Ok (ctx1, res) -> ( + match res with + | Unit | Break _ | Continue _ -> failwith "Inconsistent state" + | Return -> Ok ctx1) and eval_assumed_function_call (config : C.config) (ctx : C.eval_ctx) (fid : A.assumed_fun_id) (region_params : T.erased_region list) @@ -2048,6 +2053,69 @@ and eval_assumed_function_call (config : C.config) (ctx : C.eval_ctx) (C.eval_ctx * statement_eval_res) eval_result = raise Unimplemented -and eval_expression (config : C.config) (ctx : C.eval_ctx) (expr : A.expression) - : (C.eval_ctx * statement_eval_res) eval_result = - raise Unimplemented +and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : + (C.eval_ctx * statement_eval_res) eval_result = + match e with + | A.Statement st -> eval_statement config ctx st + | A.Sequence (e1, e2) -> ( + (* Evaluate the first expression *) + match eval_expression config ctx e1 with + | Error err -> Error err + | Ok (ctx1, Unit) -> + (* Evaluate the second expression *) + eval_expression config ctx1 e2 + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Ok (ctx1, Break i) -> Ok (ctx1, Break i) + | Ok (ctx1, Continue i) -> Ok (ctx1, Continue i) + | Ok (ctx1, Return) -> Ok (ctx1, Return)) + | A.Loop loop_body -> + (* Evaluate a loop body + + We need a specific function for the [Continue] case: in case we continue, + we might have to reevaluate the current loop body with the new context + (and repeat this an indefinite number of times). + *) + let rec eval_loop_body (ctx : C.eval_ctx) : + (C.eval_ctx * statement_eval_res) eval_result = + (* Evaluate the loop body *) + match eval_expression config ctx loop_body with + | Error err -> Error err + | Ok (ctx1, Unit) -> + (* We finished evaluating the expression in a "normal" manner *) + Ok (ctx1, Unit) + (* Control-flow breaks *) + | Ok (ctx1, Break i) -> + (* Decrease the break index *) + if i = 0 then Ok (ctx1, Unit) else Ok (ctx1, Break (i - 1)) + | Ok (ctx1, Continue i) -> + (* Decrease the continue index *) + if i = 0 then + (* We stop there. When we continue, we go back to the beginning + of the loop: we must thus reevaluate the loop body (and + recheck the result to know whether we must reevaluate again, + etc. *) + eval_loop_body ctx1 + else (* We don't stop there: transmit *) + Ok (ctx1, Continue (i - 1)) + | Ok (ctx1, Return) -> Ok (ctx1, Return) + in + (* Apply *) + eval_loop_body ctx + | A.Switch (op, tgts) -> ( + (* Evaluate the operand *) + let ctx1, op_v = eval_operand config ctx op in + match tgts with + | A.If (e1, e2) -> ( + match op_v.value with + | V.Concrete (V.Bool b) -> + if b then eval_expression config ctx1 e1 + else eval_expression config ctx1 e2 + | _ -> failwith "Inconsistent state") + | A.SwitchInt (int_ty, tgts, otherwise) -> ( + match op_v.value with + | V.Concrete (V.Scalar sv) -> ( + assert (sv.V.int_ty = int_ty); + match List.find_opt (fun (sv', _) -> sv = sv') tgts with + | None -> eval_expression config ctx1 otherwise + | Some (_, tgt) -> eval_expression config ctx1 tgt) + | _ -> failwith "Inconsistent state")) |