diff --git a/headers/header_spec.txt b/headers/header_spec.txt index bfb81802ef8ea8ae06508e9c51c5504ccc8ee483..f2b7746849a3a64caa2dc813c843b392d3a6c0cb 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1754,6 +1754,8 @@ src/plugins/wp/TacInstance.ml: CEA_WP src/plugins/wp/TacInstance.mli: CEA_WP src/plugins/wp/TacLemma.ml: CEA_WP src/plugins/wp/TacLemma.mli: CEA_WP +src/plugins/wp/TacModMask.ml: CEA_WP +src/plugins/wp/TacModMask.mli: CEA_WP src/plugins/wp/TacNormalForm.ml: CEA_WP src/plugins/wp/TacNormalForm.mli: CEA_WP src/plugins/wp/TacOverflow.ml: CEA_WP diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli index b4868c855f417c28f2984ccc3c879795ef2540d1..e889cc7d28636556e4bd95d472db3dbdd01da4f6 100644 --- a/src/plugins/wp/Cint.mli +++ b/src/plugins/wp/Cint.mli @@ -77,6 +77,11 @@ val f_bits : lfun list (** All bit-test functions *) val bit_test : term -> int -> term +(** Matchers *) + +val match_power2 : term -> term +val match_power2_minus1 : term -> term + (** Simplifiers *) val is_cint_simplifier: simplifier diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in index 72ad09daf3b043ff114ba3ab2f89fdfc1681c145..d9c8c5f2903af5bc661e3015e2dcbba5f025a0bd 100644 --- a/src/plugins/wp/Makefile.in +++ b/src/plugins/wp/Makefile.in @@ -90,7 +90,7 @@ PLUGIN_CMO:= \ TacArray TacCompound TacUnfold \ TacHavoc TacInstance TacLemma \ TacFilter TacCut WpTac TacNormalForm \ - TacRewrite TacBitwised TacBitrange TacBittest TacShift \ + TacRewrite TacBitwised TacBitrange TacBittest TacModMask TacShift \ TacSequence \ TacCongruence TacOverflow Auto \ ProofSession ProofScript ProofEngine \ diff --git a/src/plugins/wp/TacModMask.ml b/src/plugins/wp/TacModMask.ml new file mode 100644 index 0000000000000000000000000000000000000000..ac36c191eb812f8cee19bef219f23bfd4eaaa55c --- /dev/null +++ b/src/plugins/wp/TacModMask.ml @@ -0,0 +1,123 @@ +(**************************************************************************) +(* *) +(* This file is part of WP plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2021 *) +(* CEA (Commissariat a l'energie atomique et aux energies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +open Tactical + +let title_no_revert = "Revert (current: a & m -> a % m+1)" +let title_revert = "Revert (current: m & a -> a % m+1)" + +let v_revert,p_revert = + Tactical.checkbox ~id:"Wp.modmask.revert" + ~title:title_no_revert + ~descr:"Changes operands for modulo" + ~default:false () + +class modmask = + object(self) + inherit Tactical.make + ~id:"Wp.modmask" + ~title:"Mod-Mask" + ~descr:"Converts modulo from/to bitmask" + ~params:[p_revert] + + method select feedback selection = + let open Lang.N in + let open Lang.F in + let open Qed.Logic in + + let e = Tactical.selected selection in + let at = Tactical.at selection in + + let on_cond = Tactical.condition in + let replace_with d v = Tactical.rewrite ?at [ d, Lang.F.p_true, e, v ] in + + let update_title ~hard = + feedback#set_title "Mod-Mask%s" (if hard then " (hard)" else "") + in + let update_field ~enabled = + let revert = self#get_field v_revert in + let title = if revert then title_revert else title_no_revert in + feedback#update_field ~enabled v_revert ; + feedback#update_field ~title v_revert + in + let update_display ~hard ~active_field = + update_title ~hard ; + update_field ~enabled:active_field + in + match Lang.F.repr e with + | Mod(a, m) -> + begin + try + let m = Cint.l_lsl e_one @@ Cint.match_power2 m in + let n = Cint.l_and a (m - e_one) in + let cond = a >= e_zero in + + update_display ~hard:false ~active_field:false ; + Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n) + + with Not_found -> + let power_of_2 = + let v = Lang.freshvar ~basename:"n" Lang.t_int in + let tv = e_var v in + p_exists [v] (e_zero <= tv && m = Cint.l_lsl e_one tv) + in + let cond = (a >= e_zero && e_zero < m && power_of_2) in + let n = Cint.l_and a (m - e_one) in + + update_display ~hard:true ~active_field:false ; + Applicable (on_cond "Mask Guard" cond @@ replace_with "Mask" n) + end + + | Fun( f , [ a ; b ] ) when Lang.Fun.equal f Cint.f_land -> + begin + try + let a, m = + try b, Cint.match_power2_minus1 a + with Not_found -> a, Cint.match_power2_minus1 b + in + + let cond = a >= e_zero in + let n = a mod (Cint.l_lsl e_one m) in + + update_display ~hard:false ~active_field:false ; + Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n) + + with Not_found -> + let a, m = if self#get_field v_revert then b, a else a, b in + let plus_1_power_of_2 = + let v = Lang.freshvar ~basename:"n" Lang.t_int in + let tv = e_var v in + p_exists [v] (e_zero <= tv && m + e_one = Cint.l_lsl e_one tv) + in + let cond = (a >= e_zero && e_zero <= m && plus_1_power_of_2) in + let n = a mod (m + e_one) in + + update_display ~hard:true ~active_field:true ; + Applicable (on_cond "Mod Guard" cond @@ replace_with "Mod" n) + end + + | _ -> + update_display ~hard:false ~active_field:false ; + Not_applicable + end + +let modmask = Tactical.export (new modmask) diff --git a/src/plugins/wp/TacModMask.mli b/src/plugins/wp/TacModMask.mli new file mode 100644 index 0000000000000000000000000000000000000000..fb0f0f4daf14c2bea477c92e0e0dad1ffa8895ec --- /dev/null +++ b/src/plugins/wp/TacModMask.mli @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* This file is part of WP plug-in of Frama-C. *) +(* *) +(* Copyright (C) 2007-2021 *) +(* CEA (Commissariat a l'energie atomique et aux energies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +val modmask : Tactical.tactical