From 2fb08aa7da2e3e9d9ced6cfb3aa99ea7f95f1a48 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 18:23:06 +0100
Subject: [PATCH] [wp] factorize switch cases
---
src/plugins/wp/cfgCalculus.ml | 12 ++++++++++--
src/plugins/wp/cfgDump.ml | 19 +++++++++++++++----
2 files changed, 25 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 313ffb87e0a..bb1c39135e2 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/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 =
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 3d25437b758..0b14a6f2785 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/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
--
GitLab