diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | src/CfimAst.ml | 8 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 14 | ||||
| -rw-r--r-- | src/Print.ml | 11 |
5 files changed, 28 insertions, 10 deletions
@@ -3,6 +3,7 @@ all: build-test CHARON_HOME=../charon CHARON_EXEC=$(CHARON_HOME)/charon CHARON_TESTS_DIR=$(CHARON_HOME)/tests/cfim +CHARON_OPTIONS= --dest ../tests/cfim --no-code-duplication DEST_DIR=tests # Default translation options: @@ -33,7 +34,7 @@ translate-hashmap: SUBDIR:=hashmap # Generic rule to extract the CFIM from a rust file .PHONY: gen-cfim-% gen-cfim-%: build - cd $(CHARON_HOME)/charon && cargo run ../tests/src/$*.rs --dest ../tests/cfim + cd $(CHARON_HOME)/charon && cargo run ../tests/src/$*.rs $(CHARON_OPTIONS) # Generic rule to test the translation on a CFIM file .PHONY: translate-% diff --git a/src/CfimAst.ml b/src/CfimAst.ml index a06dfc90..6716c793 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -142,10 +142,12 @@ type statement = and switch_targets = | If of statement * statement (** Gives the "if" and "else" blocks *) - | SwitchInt of integer_type * (scalar_value * statement) list * statement + | SwitchInt of integer_type * (scalar_value list * statement) list * statement (** The targets for a switch over an integer are: - - the list `(matched value, statement to execute)` - - the "otherwise" statement. + - the list `(matched values, statement to execute)` + We need a list for the matched values in case we do something like this: + `switch n { 0 | 1 => ..., _ => ... } + - the "otherwise" statement Also note that we precise the type of the integer (uint32, int64, etc.) which we switch on. *) [@@deriving diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 9ac0a974..f91f7b05 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -586,7 +586,7 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result = let* int_ty = integer_type_of_json int_ty in let* tgts = list_of_json - (pair_of_json scalar_value_of_json statement_of_json) + (pair_of_json (list_of_json scalar_value_of_json) statement_of_json) tgts in let* otherwise = statement_of_json otherwise in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 517c239c..c3b60fa9 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -944,7 +944,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : assert (op_v' = op_v); assert (sv.V.int_ty = int_ty); (* Find the branch *) - match List.find_opt (fun (sv', _) -> sv = sv') stgts with + match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with | None -> eval_statement config otherwise cf | Some (_, tgt) -> eval_statement config tgt cf in @@ -961,7 +961,19 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st cf)) stgts in + (* Several branches may be grouped together: every branch is described + * by a pair (list of values, branch expression). + * In order to do a symbolic evaluation, we make this "flat" by + * de-grouping the branches. *) + let stgts = + List.concat + (List.map + (fun (vl, st) -> List.map (fun v -> (v, st)) vl) + stgts) + in + (* Translate the otherwise branch *) let otherwise = eval_statement config otherwise cf in + (* Expand and continue *) expand_symbolic_int config sv (S.mk_opt_place_from_op op ctx) int_ty stgts otherwise ctx diff --git a/src/Print.ml b/src/Print.ml index d19e03e5..a868963a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -943,10 +943,13 @@ module CfimAst = struct in let branches = List.map - (fun (sv, be) -> - indent1 - ^ PV.scalar_value_to_string sv - ^ " => {\n" ^ inner_to_string2 be ^ "\n" ^ indent1 ^ "}") + (fun (svl, be) -> + let svl = + List.map (fun sv -> "| " ^ PV.scalar_value_to_string sv) svl + in + let svl = String.concat " " svl in + indent1 ^ svl ^ " => {\n" ^ inner_to_string2 be ^ "\n" + ^ indent1 ^ "}") branches in let branches = String.concat "\n" branches in |