Add support for "fused" match branches

4 files changed, 26 insertions, 9 deletions

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