[wp] factorize switch cases

src/plugins/wp/cfgCalculus.ml

@@ -114,6 +114,14 @@ let is_selected_props (props : props) ?pi pid =
       | Some q -> q
       | None -> WpPropId.property_of_id pid
 
+let rec factorize ~wdefault = function
+  | (_,w)::wcs when w==wdefault -> factorize ~wdefault wcs
+  | (e,w)::wcs -> collect ~wdefault [e] w wcs
+  | [] -> []
+and collect ~wdefault rs wr = function
+  | (e,w)::wcs when w==wr -> collect ~wdefault (e::rs) wr wcs
+  | wcs -> (List.rev rs,wr) :: factorize ~wdefault wcs
+
 (* -------------------------------------------------------------------------- *)
 (* --- WP Calculus Driver from Interpreted Automata                       --- *)
 (* -------------------------------------------------------------------------- *)
@@ -218,9 +226,9 @@ struct
         let welse = wp env velse in
         W.test env.we s cond wthen welse
     | Switch { value ; cases ; default } ->
-        let wcases = List.map (fun (e,v) -> [e], wp env v) cases in
+        let wcases = List.map (fun (e,v) -> e,wp env v) cases in
         let wdefault = wp env default in
-        W.switch env.we s value wcases wdefault
+        W.switch env.we s value (factorize ~wdefault wcases) wdefault
     | Loop _ ->
         let m = env.mode in
         let smoking =

src/plugins/wp/cfgDump.ml

@@ -163,14 +163,25 @@ let return _env _stmt r k =
 
 let test _env _stmt e k1 k2 =
   let u = node () in
-  Format.fprintf !out "  %a [ color=cyan , label=\"If %a\" ] ;@." pretty u Printer.pp_exp e ;
+  Format.fprintf !out "  %a [ color=cyan , label=\"If %a\" ] ;@."
+    pretty u Printer.pp_exp e ;
   link u k1 ; link u k2 ; u
 
 let switch _env _stmt e cases def =
   let u = node () in
-  Format.fprintf !out "  %a [ color=cyan , label=\"Switch %a\" ] ;@." pretty u Printer.pp_exp e ;
-  List.iter (fun (_,k) -> link u k) cases ;
-  link u def ; u
+  Format.fprintf !out "  %a [ color=cyan , label=\"Switch %a\" ] ;@."
+    pretty u Printer.pp_exp e ;
+  List.iter (fun (es,k) ->
+      let c = node () in
+      Format.fprintf !out "  %a [ color=orange , label=\"Case %a\" ] ;@."
+        pretty c (Pretty_utils.pp_list ~sep:"," Printer.pp_exp) es ;
+      link u c ;
+      link c k ;
+    ) cases ;
+  let d = node () in
+  Format.fprintf !out "  %a [ color=orange , label=\"Default\" ] ;@." pretty d ;
+  link u d ;
+  link d def ; u
 
 let const _ x k =
   let u = node () in