diff options
| -rw-r--r-- | src/CfimAst.ml | 19 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 38 | ||||
| -rw-r--r-- | src/Interpreter.ml | 151 | ||||
| -rw-r--r-- | src/Print.ml | 64 | ||||
| -rw-r--r-- | src/Substitute.ml | 28 |
5 files changed, 128 insertions, 172 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index d2bf9181..9acf40ff 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -50,22 +50,17 @@ type statement = (** Continue to (outer) loop. The loop identifier works the same way as for [Break] *) | Nop -[@@deriving show] - -type expression = - | Statement of statement - | Sequence of expression * expression + | Sequence of statement * statement | Switch of operand * switch_targets - | Loop of expression + | Loop of statement [@@deriving show] -(* TODO: merge with statement *) and switch_targets = - | If of expression * expression (** Gives the "if" and "else" blocks *) - | SwitchInt of integer_type * (scalar_value * expression) list * expression + | If of statement * statement (** Gives the "if" and "else" blocks *) + | SwitchInt of integer_type * (scalar_value * statement) list * statement (** The targets for a switch over an integer are: - - the list `(matched value, expression to execute)` - - the "otherwise" expression. + - the list `(matched value, statement to execute)` + - the "otherwise" statement. Also note that we precise the type of the integer (uint32, int64, etc.) which we switch on. *) [@@deriving show] @@ -77,6 +72,6 @@ type fun_def = { divergent : bool; arg_count : int; locals : var list; - body : expression; + body : statement; } [@@deriving show] diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 4f6c2e73..383b8410 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -475,7 +475,7 @@ let call_of_json (js : json) : (A.call, string) result = Ok { A.func; region_params; type_params; args; dest } | _ -> Error "") -let statement_of_json (js : json) : (A.statement, string) result = +let rec statement_of_json (js : json) : (A.statement, string) result = combine_error_msgs js "statement_of_json" (match js with | `Assoc [ ("Assign", `List [ place; rvalue ]) ] -> @@ -507,42 +507,34 @@ let statement_of_json (js : json) : (A.statement, string) result = let* i = int_of_json i in Ok (A.Continue i) | `String "Nop" -> Ok A.Nop - | _ -> Error "") - -let rec expression_of_json (js : json) : (A.expression, string) result = - combine_error_msgs js "expression_of_json" - (match js with - | `Assoc [ ("Statement", statement) ] -> - let* statement = statement_of_json statement in - Ok (A.Statement statement) - | `Assoc [ ("Sequence", `List [ e1; e2 ]) ] -> - let* e1 = expression_of_json e1 in - let* e2 = expression_of_json e2 in - Ok (A.Sequence (e1, e2)) + | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] -> + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 in + Ok (A.Sequence (st1, st2)) | `Assoc [ ("Switch", `List [ op; tgt ]) ] -> let* op = operand_of_json op in let* tgt = switch_targets_of_json tgt in Ok (A.Switch (op, tgt)) - | `Assoc [ ("Loop", e) ] -> - let* e = expression_of_json e in - Ok (A.Loop e) + | `Assoc [ ("Loop", st) ] -> + let* st = statement_of_json st in + Ok (A.Loop st) | _ -> Error "") and switch_targets_of_json (js : json) : (A.switch_targets, string) result = combine_error_msgs js "switch_targets_of_json" (match js with - | `Assoc [ ("If", `List [ e1; e2 ]) ] -> - let* e1 = expression_of_json e1 in - let* e2 = expression_of_json e2 in - Ok (A.If (e1, e2)) + | `Assoc [ ("If", `List [ st1; st2 ]) ] -> + let* st1 = statement_of_json st1 in + let* st2 = statement_of_json st2 in + Ok (A.If (st1, st2)) | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] -> let* int_ty = integer_type_of_json int_ty in let* tgts = list_of_json - (pair_of_json scalar_value_of_json expression_of_json) + (pair_of_json scalar_value_of_json statement_of_json) tgts in - let* otherwise = expression_of_json otherwise in + let* otherwise = statement_of_json otherwise in Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") @@ -565,7 +557,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result = let* divergent = bool_of_json divergent in let* arg_count = int_of_json arg_count in let* locals = list_of_json var_of_json locals in - let* body = expression_of_json body in + let* body = statement_of_json body in Ok { A.def_id; name; signature; divergent; arg_count; locals; body } | _ -> Error "") diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 5d6af03a..b936fa70 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -35,10 +35,8 @@ let place_to_string = Print.EvalCtxCfimAst.place_to_string let operand_to_string = Print.EvalCtxCfimAst.operand_to_string -let statement_to_string = Print.EvalCtxCfimAst.statement_to_string - -let expression_to_string ctx = - Print.EvalCtxCfimAst.expression_to_string ctx " " " " +let statement_to_string ctx = + Print.EvalCtxCfimAst.statement_to_string ctx "" " " (* TODO: move *) let mk_unit_ty : T.ety = T.Tuple [] @@ -2326,6 +2324,68 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) | A.Break i -> Ok (ctx, Break i) | A.Continue i -> Ok (ctx, Continue i) | A.Nop -> Ok (ctx, Unit) + | A.Sequence (st1, st2) -> ( + (* Evaluate the first statement *) + match eval_statement config ctx st1 with + | Error err -> Error err + | Ok (ctx, Unit) -> + (* Evaluate the second statement *) + eval_statement config ctx st2 + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Ok (ctx, Break i) -> Ok (ctx, Break i) + | Ok (ctx, Continue i) -> Ok (ctx, Continue i) + | Ok (ctx, Return) -> Ok (ctx, 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_statement config ctx loop_body with + | Error err -> Error err + | Ok (ctx, Unit) -> + (* We finished evaluating the statement in a "normal" manner *) + Ok (ctx, Unit) + (* Control-flow breaks *) + | Ok (ctx, Break i) -> + (* Decrease the break index *) + if i = 0 then Ok (ctx, Unit) else Ok (ctx, Break (i - 1)) + | Ok (ctx, 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 ctx + else (* We don't stop there: transmit *) + Ok (ctx, Continue (i - 1)) + | Ok (ctx, Return) -> Ok (ctx, Return) + in + (* Apply *) + eval_loop_body ctx + | A.Switch (op, tgts) -> ( + (* Evaluate the operand *) + let ctx, op_v = eval_operand config ctx op in + match tgts with + | A.If (st1, st2) -> ( + match op_v.value with + | V.Concrete (V.Bool b) -> + if b then eval_statement config ctx st1 + else eval_statement config ctx st2 + | _ -> 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_statement config ctx otherwise + | Some (_, tgt) -> eval_statement config ctx tgt) + | _ -> failwith "Inconsistent state")) (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : @@ -2404,94 +2464,17 @@ and eval_local_function_call (config : C.config) (ctx : C.eval_ctx) Ok ctx) | SymbolicMode -> raise Unimplemented -(** Evaluate an expression seen as a function body (auxiliary helper for +(** Evaluate a statement seen as a function body (auxiliary helper for [eval_statement]) *) and eval_function_body (config : C.config) (ctx : C.eval_ctx) - (body : A.expression) : (C.eval_ctx, eval_error) result = - match eval_expression config ctx body with + (body : A.statement) : (C.eval_ctx, eval_error) result = + match eval_statement config ctx body with | Error err -> Error err | Ok (ctx, res) -> ( match res with | Unit | Break _ | Continue _ -> failwith "Inconsistent state" | Return -> Ok ctx) -(** Evaluate an expression *) -and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : - (C.eval_ctx * statement_eval_res) eval_result = - (* Debugging *) - (match e with - | A.Statement _ | A.Sequence (_, _) -> () - | A.Loop _ | A.Switch (_, _) -> - L.log#ldebug - (lazy - ("\n" ^ eval_ctx_to_string ctx ^ "\nAbout to evaluate expression: \n" - ^ expression_to_string ctx e ^ "\n"))); - (* Evaluate *) - 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 (ctx, Unit) -> - (* Evaluate the second expression *) - eval_expression config ctx e2 - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Ok (ctx, Break i) -> Ok (ctx, Break i) - | Ok (ctx, Continue i) -> Ok (ctx, Continue i) - | Ok (ctx, Return) -> Ok (ctx, 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 (ctx, Unit) -> - (* We finished evaluating the expression in a "normal" manner *) - Ok (ctx, Unit) - (* Control-flow breaks *) - | Ok (ctx, Break i) -> - (* Decrease the break index *) - if i = 0 then Ok (ctx, Unit) else Ok (ctx, Break (i - 1)) - | Ok (ctx, 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 ctx - else (* We don't stop there: transmit *) - Ok (ctx, Continue (i - 1)) - | Ok (ctx, Return) -> Ok (ctx, Return) - in - (* Apply *) - eval_loop_body ctx - | A.Switch (op, tgts) -> ( - (* Evaluate the operand *) - let ctx, 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 ctx e1 - else eval_expression config ctx 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 ctx otherwise - | Some (_, tgt) -> eval_expression config ctx tgt) - | _ -> failwith "Inconsistent state")) - (** Test a unit function (taking no arguments) by evaluating it in an empty environment diff --git a/src/Print.ml b/src/Print.ml index 25434eeb..dc559dc3 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -677,21 +677,22 @@ module CfimAst = struct in variant_name ^ " " ^ fields) - let statement_to_string (fmt : ast_formatter) (st : A.statement) : string = + let rec statement_to_string (fmt : ast_formatter) (indent : string) + (indent_incr : string) (st : A.statement) : string = match st with | A.Assign (p, rv) -> - place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv + indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv | A.FakeRead p -> "fake_read " ^ place_to_string fmt p | A.SetDiscriminant (p, variant_id) -> (* TODO: improve this to lookup the variant name by using the def id *) - "set_discriminant(" ^ place_to_string fmt p ^ ", " + indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", " ^ T.VariantId.to_string variant_id ^ ")" | A.Drop p -> "drop(" ^ place_to_string fmt p ^ ")" | A.Assert a -> let cond = operand_to_string fmt a.A.cond in - if a.A.expected then "assert(" ^ cond ^ ")" - else "assert(¬" ^ cond ^ ")" + if a.A.expected then indent ^ "assert(" ^ cond ^ ")" + else indent ^ "assert(¬" ^ cond ^ ")" | A.Call call -> let ty_fmt = ast_to_etype_formatter fmt in let params = @@ -717,38 +718,33 @@ module CfimAst = struct | A.BoxFree -> "alloc::alloc::box_free" ^ params) in let dest = place_to_string fmt call.A.dest in - dest ^ " := move " ^ name_params ^ args - | A.Panic -> "panic" - | A.Return -> "return" - | A.Break i -> "break " ^ string_of_int i - | A.Continue i -> "continue " ^ string_of_int i - | A.Nop -> "nop" - - let rec expression_to_string (fmt : ast_formatter) (indent : string) - (indent_incr : string) (e : A.expression) : string = - match e with - | A.Statement st -> indent ^ statement_to_string fmt st ^ ";" - | A.Sequence (e1, e2) -> - expression_to_string fmt indent indent_incr e1 + indent ^ dest ^ " := move " ^ name_params ^ args + | A.Panic -> indent ^ "panic" + | A.Return -> indent ^ "return" + | A.Break i -> indent ^ "break " ^ string_of_int i + | A.Continue i -> indent ^ "continue " ^ string_of_int i + | A.Nop -> indent ^ "nop" + | A.Sequence (st1, st2) -> + statement_to_string fmt indent indent_incr st1 ^ "\n" - ^ expression_to_string fmt indent indent_incr e2 + ^ statement_to_string fmt indent indent_incr st2 | A.Switch (op, tgts) -> ( let op = operand_to_string fmt op in match tgts with - | A.If (true_e, false_e) -> + | A.If (true_st, false_st) -> let inner_indent = indent ^ indent_incr in let inner_to_string = - expression_to_string fmt inner_indent indent_incr + statement_to_string fmt inner_indent indent_incr in - let true_e = inner_to_string true_e in - let false_e = inner_to_string false_e in - indent ^ "if (" ^ op ^ ") {\n" ^ true_e ^ "\n" ^ indent ^ "}\n" - ^ indent ^ "else {\n" ^ false_e ^ "\n" ^ indent ^ "}" + let true_st = inner_to_string true_st in + let false_st = inner_to_string false_st in + indent ^ "if (" ^ op ^ ") {\n" ^ true_st ^ "\n" ^ indent ^ "}\n" + ^ indent ^ "else {\n" ^ false_st ^ "\n" ^ indent ^ "}" | A.SwitchInt (_ty, branches, otherwise) -> let indent1 = indent ^ indent_incr in let indent2 = indent1 ^ indent_incr in let inner_to_string2 = - expression_to_string fmt indent2 indent_incr + statement_to_string fmt indent2 indent_incr in let branches = List.map @@ -764,9 +760,9 @@ module CfimAst = struct ^ inner_to_string2 otherwise ^ "\n" ^ indent1 ^ "}" in indent ^ "switch (" ^ op ^ ") {\n" ^ branches ^ "\n" ^ indent ^ "}") - | A.Loop loop_e -> + | A.Loop loop_st -> indent ^ "loop {\n" - ^ expression_to_string fmt (indent ^ indent_incr) indent_incr loop_e + ^ statement_to_string fmt (indent ^ indent_incr) indent_incr loop_st ^ "\n" ^ indent ^ "}" let fun_def_to_string (fmt : ast_formatter) (indent : string) @@ -820,7 +816,7 @@ module CfimAst = struct (* Body *) let body = - expression_to_string fmt (indent ^ indent_incr) indent_incr def.body + statement_to_string fmt (indent ^ indent_incr) indent_incr def.body in (* Put everything together *) @@ -929,12 +925,8 @@ module EvalCtxCfimAst = struct let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.operand_to_string fmt op - let statement_to_string (ctx : C.eval_ctx) (s : A.statement) : string = + let statement_to_string (ctx : C.eval_ctx) (indent : string) + (indent_incr : string) (e : A.statement) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in - PA.statement_to_string fmt s - - let expression_to_string (ctx : C.eval_ctx) (indent : string) - (indent_incr : string) (e : A.expression) : string = - let fmt = PA.eval_ctx_to_ast_formatter ctx in - PA.expression_to_string fmt indent indent_incr e + PA.statement_to_string fmt indent indent_incr e end diff --git a/src/Substitute.ml b/src/Substitute.ml index b8c3edd9..9099155f 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -146,8 +146,8 @@ let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call } (** Apply a type substitution to a statement *) -let statement_substitute (tsubst : T.TypeVarId.id -> T.ety) (st : A.statement) : - A.statement = +let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety) + (st : A.statement) : A.statement = match st with | A.Assign (p, rvalue) -> let p = place_substitute tsubst p in @@ -169,42 +169,36 @@ let statement_substitute (tsubst : T.TypeVarId.id -> T.ety) (st : A.statement) : let call = call_substitute tsubst call in A.Call call | A.Panic | A.Return | A.Break _ | A.Continue _ | A.Nop -> st - -(** Apply a type substitution to an expression *) -let rec expression_substitute (tsubst : T.TypeVarId.id -> T.ety) - (e : A.expression) : A.expression = - match e with - | A.Statement st -> A.Statement (statement_substitute tsubst st) - | A.Sequence (e1, e2) -> + | A.Sequence (st1, st2) -> A.Sequence - (expression_substitute tsubst e1, expression_substitute tsubst e2) + (statement_substitute tsubst st1, statement_substitute tsubst st2) | A.Switch (op, tgts) -> A.Switch (operand_substitute tsubst op, switch_targets_substitute tsubst tgts) - | A.Loop le -> A.Loop (expression_substitute tsubst le) + | A.Loop le -> A.Loop (statement_substitute tsubst le) (** Apply a type substitution to switch targets *) and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety) (tgts : A.switch_targets) : A.switch_targets = match tgts with - | A.If (e1, e2) -> - A.If (expression_substitute tsubst e1, expression_substitute tsubst e2) + | A.If (st1, st2) -> + A.If (statement_substitute tsubst st1, statement_substitute tsubst st2) | A.SwitchInt (int_ty, tgts, otherwise) -> let tgts = - List.map (fun (sv, e) -> (sv, expression_substitute tsubst e)) tgts + List.map (fun (sv, st) -> (sv, statement_substitute tsubst st)) tgts in - let otherwise = expression_substitute tsubst otherwise in + let otherwise = statement_substitute tsubst otherwise in A.SwitchInt (int_ty, tgts, otherwise) (** Apply a type substitution to a function body. Return the local variables and the body. *) let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) - (def : A.fun_def) : V.var list * A.expression = + (def : A.fun_def) : V.var list * A.statement = let rsubst r = r in let locals = List.map (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty }) def.A.locals in - let body = expression_substitute tsubst def.body in + let body = statement_substitute tsubst def.body in (locals, body) |