From 4af8386de0db4bf09a3a55034f221b941b5963a7 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 2 Sep 2019 11:28:48 +0200
Subject: [PATCH] [WP] minor
---
src/plugins/wp/Cint.ml | 29 +++++++++++++++++++----------
src/plugins/wp/Cint.mli | 3 +--
2 files changed, 20 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 946d858aabe..572ea84ed4b 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -97,12 +97,15 @@ let f_lsr = Lang.extern_f ~library ~result "lsr"
let f_bitwised = [ f_lnot ; f_lor ; f_land ; f_lxor ; f_lsl ; f_lsr ]
-let f_bit_stdlib = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
-let f_bit = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
-let f_bit_export = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+(* [f_bit_stdlib] is related to the function [bit_test] of Frama-C StdLib *)
+let f_bit_stdlib = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+(* [f_bit_positive] is actually exported in forgoting the fact the position is positive *)
+let f_bit_positive = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+(* At export, some constructs such as [e & (1 << k)] are written into [f_bit_export] construct *)
+let f_bit_export = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
let () = let open LogicBuiltins in add_builtin "\\bit_test_stdlib" [Z;Z] f_bit_stdlib
-let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit
+let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit_positive
(* -------------------------------------------------------------------------- *)
(* --- Matching utilities for simplifications --- *)
@@ -475,10 +478,14 @@ let smp2 f zf = (* f(c1,c2) ~> zf(c1,c2), f(c1,c2,...) ~> f(zf(c1,c2),...) *)
end
| _ -> raise Not_found
-let bitk_positive k e = F.e_fun f_bit [e;k]
-let smp_intro_bitk_positive = function
- | [ a ; k ] when is_positive_or_null k -> bitk_positive k a
- | [ a ; k ] -> (* TODO: expand the current logic definition of the ACSL stdlib symbol *)
+let bitk_positive k e = F.e_fun f_bit_positive [e;k]
+let smp_mk_bit_stdlib = function
+ | [ a ; k ] when is_positive_or_null k ->
+ (* No need to expand the logic definition of the ACSL stdlib symbol when
+ [k] is positive (the definition must comply with that simplification). *)
+ bitk_positive k a
+ | [ a ; k ] ->
+ (* TODO: expand the current logic definition of the ACSL stdlib symbol *)
F.e_neq F.e_zero (F.e_fun f_land [a; (F.e_fun f_lsl [F.e_one;k])])
| _ -> raise Not_found
@@ -778,8 +785,10 @@ let () =
begin
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
- let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_intro_bitk_positive in
- let bi_lbit = mk_builtin "f_bit" f_bit smp_bitk_positive in
+ (* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
+ no creation of [e_fun f_bit_stdlib args] *)
+ let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
+ let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
(smp1 Integer.lognot) in
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index a78c5b91909..be94baad52b 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -71,9 +71,8 @@ val f_lxor : lfun
val f_lor : lfun
val f_lsl : lfun
val f_lsr : lfun
-val f_bit : lfun
-val f_bitwised : lfun list (** All except f_bit *)
+val f_bitwised : lfun list (** All except f_bit_positive *)
(** Simplifiers *)
--
GitLab