From 5929eba6894e246538d1fc193d6c5773631e1f10 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 1 Dec 2023 16:53:03 +0100
Subject: [PATCH] [wp] no more axioms in Cint Why3 theory
---
src/plugins/wp/share/why3/frama_c_wp/cint.mlw | 295 +++++++++++++-----
1 file changed, 212 insertions(+), 83 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
index 471483d7973..9fd52dd660a 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cint.mlw
@@ -24,7 +24,7 @@
(* --- C-Integer Arithmetics for Why-3 --- *)
(* -------------------------------------------------------------------------- *)
-theory Cint
+module Cint
use int.Int
use bool.Bool
@@ -33,71 +33,97 @@ theory Cint
(** ** bounds are inlined into prover files ** **)
- function max_uint8: int = 256
- function max_sint8: int = 128
- function max_uint16: int = 65536
- function max_sint16: int = 32768
- function max_uint32: int = 4294967296
- function max_sint32: int = 2147483648
- function max_uint64: int = 18446744073709551616
- function max_sint64: int = 9223372036854775808
+ let constant max_uint8: int = 0x100
+ let constant max_sint8: int = 0x80
+ let constant max_uint16: int = 0x10000
+ let constant max_sint16: int = 0x8000
+ let constant max_uint32: int = 0x100000000
+ let constant max_sint32: int = 0x80000000
+ let constant max_uint64: int = 0x10000000000000000
+ let constant max_sint64: int = 0x8000000000000000
(** * C-Integer Ranges * **)
- predicate is_bool (x:int) = x = 0 \/ x = 1
+ predicate is_bool(x:int) = x = 0 \/ x = 1
+ predicate is_uint8(x:int) = 0 <= x < max_uint8
+ predicate is_sint8(x:int) = -max_sint8 <= x < max_sint8
+ predicate is_uint16(x:int) = 0 <= x < max_uint16
+ predicate is_sint16(x:int) = -max_sint16 <= x < max_sint16
+ predicate is_uint32(x:int) = 0 <= x < max_uint32
+ predicate is_sint32(x:int) = -max_sint32 <= x < max_sint32
+ predicate is_uint64(x:int) = 0 <= x < max_uint64
+ predicate is_sint64(x:int) = -max_sint64 <= x < max_sint64
- predicate is_uint8 int
-
- axiom is_uint8_def :
- forall x:int [is_uint8 x]. is_uint8 x <-> 0 <= x /\ x < max_uint8
-
- predicate is_sint8 int
-
- axiom is_sint8_def :
- forall x:int [is_sint8 x]. is_sint8 x <-> (- max_sint8) <= x /\ x < max_sint8
-
- predicate is_uint16 int
-
- axiom is_uint16_def :
- forall x:int [is_uint16 x]. is_uint16 x <-> 0 <= x /\ x < max_uint16
-
- predicate is_sint16 (x:int) = (- max_sint16) <= x /\ x < max_sint16
-
- predicate is_uint32 int
-
- axiom is_uint32_def :
- forall x:int [is_uint32 x]. is_uint32 x <-> 0 <= x /\ x < max_uint32
-
- predicate is_sint32 int
-
- axiom is_sint32_def :
- forall x:int [is_sint32 x]. is_sint32 x <-> (- max_sint32) <= x /\ x < max_sint32
-
- predicate is_uint64 int
-
- axiom is_uint64_def :
- forall x:int [is_uint64 x]. is_uint64 x <-> 0 <= x /\ x < max_uint64
-
- predicate is_sint64 int
-
- axiom is_sint64_def :
- forall x:int [is_sint64 x]. is_sint64 x <-> (- max_sint64) <= x /\ x < max_sint64
-
- lemma is_bool0 : is_bool 0
-
- lemma is_bool1 : is_bool 1
+ lemma is_bool0: is_bool(0)
+ lemma is_bool1: is_bool(1)
(** * C-Integer Conversion * **)
function to_bool ( x : int ) : int = if x = 0 then 0 else 1
- function to_uint8 int : int
- function to_sint8 int : int
- function to_uint16 int : int
- function to_sint16 int : int
- function to_uint32 int : int
- function to_sint32 int : int
- function to_uint64 int : int
- function to_sint64 int : int
+
+ let rec function to_uint8 (x: int) : int
+ variant { if x < 0 then max_uint8 - x else x }
+ = if x < 0
+ then to_uint8 (x + max_uint8)
+ else if x >= max_uint8
+ then to_uint8 (x - max_uint8)
+ else x
+
+ let rec function to_sint8 (x: int) : int
+ variant { if x < - max_sint8 then max_sint8 - x else x - max_sint8 }
+ = if x < -max_sint8
+ then to_sint8 (x + max_uint8)
+ else if x >= max_sint8
+ then to_sint8 (x - max_uint8)
+ else x
+
+ let rec function to_uint16 (x: int) : int
+ variant { if x < 0 then max_uint16 - x else x }
+ = if x < 0
+ then to_uint16 (x + max_uint16)
+ else if x >= max_uint16
+ then to_uint16 (x - max_uint16)
+ else x
+
+ let rec function to_sint16 (x: int) : int
+ variant { if x < - max_sint16 then max_sint16 - x else x - max_sint16 }
+ = if x < -max_sint16
+ then to_sint16 (x + max_uint16)
+ else if x >= max_sint16
+ then to_sint16 (x - max_uint16)
+ else x
+
+ let rec function to_uint32 (x: int) : int
+ variant { if x < 0 then max_uint32 - x else x }
+ = if x < 0
+ then to_uint32 (x + max_uint32)
+ else if x >= max_uint32
+ then to_uint32 (x - max_uint32)
+ else x
+
+ let rec function to_sint32 (x: int) : int
+ variant { if x < - max_sint32 then max_sint32 - x else x - max_sint32 }
+ = if x < -max_sint32
+ then to_sint32 (x + max_uint32)
+ else if x >= max_sint32
+ then to_sint32 (x - max_uint32)
+ else x
+
+ let rec function to_uint64 (x: int) : int
+ variant { if x < 0 then max_uint64 - x else x }
+ = if x < 0
+ then to_uint64 (x + max_uint64)
+ else if x >= max_uint64
+ then to_uint64 (x - max_uint64)
+ else x
+
+ let rec function to_sint64 (x: int) : int
+ variant { if x < - max_sint64 then max_sint64 - x else x - max_sint64 }
+ = if x < -max_sint64
+ then to_sint64 (x + max_uint64)
+ else if x >= max_sint64
+ then to_sint64 (x - max_uint64)
+ else x
function two_power_abs int : int
@@ -109,33 +135,136 @@ theory Cint
function to_uint int int : int
function to_sint int int : int
- (** * C-Integer Conversions are in-range * **)
-
- axiom is_to_uint8 : forall x:int. is_uint8 (to_uint8 x)
- axiom is_to_sint8 : forall x:int. is_sint8 (to_sint8 x)
- axiom is_to_uint16 : forall x:int. is_uint16 (to_uint16 x)
- axiom is_to_sint16 : forall x:int. is_sint16 (to_sint16 x)
- axiom is_to_uint32 : forall x:int. is_uint32 (to_uint32 x)
- axiom is_to_sint32 : forall x:int. is_sint32 (to_sint32 x)
- axiom is_to_uint64 : forall x:int. is_uint64 (to_uint64 x)
- axiom is_to_sint64 : forall x:int. is_sint64 (to_sint64 x)
+ (** * C-Integer Conversions are in-range * **)
+
+ let rec lemma is_to_uint8 (x: int)
+ ensures { is_uint8 (to_uint8 x) }
+ variant { if x < 0 then max_uint8 - x else x }
+ = if x < 0
+ then is_to_uint8 (x + max_uint8)
+ else if x >= max_uint8
+ then is_to_uint8 (x - max_uint8)
+ else ()
+
+ let rec lemma is_to_sint8 (x: int)
+ ensures { is_sint8 (to_sint8 x) }
+ variant { if x < - max_sint8 then max_sint8 - x else x - max_sint8 }
+ = if x < -max_sint8
+ then is_to_sint8 (x + max_uint8)
+ else if x >= max_sint8
+ then is_to_sint8 (x - max_uint8)
+ else ()
+
+ let rec lemma is_to_uint16 (x: int)
+ ensures { is_uint16 (to_uint16 x) }
+ variant { if x < 0 then max_uint16 - x else x }
+ = if x < 0
+ then is_to_uint16 (x + max_uint16)
+ else if x >= max_uint16
+ then is_to_uint16 (x - max_uint16)
+ else ()
+
+ let rec lemma is_to_sint16 (x: int)
+ ensures { is_sint16 (to_sint16 x) }
+ variant { if x < - max_sint16 then max_sint16 - x else x - max_sint16 }
+ = if x < -max_sint16
+ then is_to_sint16 (x + max_uint16)
+ else if x >= max_sint16
+ then is_to_sint16 (x - max_uint16)
+ else ()
+
+ let rec lemma is_to_uint32 (x: int)
+ ensures { is_uint32 (to_uint32 x) }
+ variant { if x < 0 then max_uint32 - x else x }
+ = if x < 0
+ then is_to_uint32 (x + max_uint32)
+ else if x >= max_uint32
+ then is_to_uint32 (x - max_uint32)
+ else ()
+
+ let rec lemma is_to_sint32 (x: int)
+ ensures { is_sint32 (to_sint32 x) }
+ variant { if x < - max_sint32 then max_sint32 - x else x - max_sint32 }
+ = if x < -max_sint32
+ then is_to_sint32 (x + max_uint32)
+ else if x >= max_sint32
+ then is_to_sint32 (x - max_uint32)
+ else ()
+
+ let rec lemma is_to_uint64 (x: int)
+ ensures { is_uint64 (to_uint64 x) }
+ variant { if x < 0 then max_uint64 - x else x }
+ = if x < 0
+ then is_to_uint64 (x + max_uint64)
+ else if x >= max_uint64
+ then is_to_uint64 (x - max_uint64)
+ else ()
+
+ let rec lemma is_to_sint64 (x: int)
+ ensures { is_sint64 (to_sint64 x) }
+ variant { if x < - max_sint64 then max_sint64 - x else x - max_sint64 }
+ = if x < -max_sint64
+ then is_to_sint64 (x + max_uint64)
+ else if x >= max_sint64
+ then is_to_sint64 (x - max_uint64)
+ else ()
(** * C-Integer Conversions are identity when in-range * **)
- axiom id_uint8 : forall x:int [ to_uint8 x ]. 0 <= x < max_uint8 -> (to_uint8 x) = x
- axiom id_sint8 : forall x:int [ to_sint8 x ]. -max_sint8 <= x < max_sint8 -> (to_sint8 x) = x
- axiom id_uint16 : forall x:int [ to_uint16 x ]. 0 <= x < max_uint16 -> (to_uint16 x) = x
- axiom id_sint16 : forall x:int [ to_sint16 x ]. -max_sint16 <= x < max_sint16 -> (to_sint16 x) = x
- axiom id_uint32 : forall x:int [ to_uint32 x ]. 0 <= x < max_uint32 -> (to_uint32 x) = x
- axiom id_sint32 : forall x:int [ to_sint32 x ]. -max_sint32 <= x < max_sint32 -> (to_sint32 x) = x
- axiom id_uint64 : forall x:int [ to_uint64 x ]. 0 <= x < max_uint64 -> (to_uint64 x) = x
- axiom id_sint64 : forall x:int [ to_sint64 x ]. -max_sint64 <= x < max_sint64 -> (to_sint64 x) = x
-
- (** * Generalization for [to_sint _ (to_uint _ x)] * **)
-
- axiom proj_int8 : forall x:int [ to_sint8(to_uint8 x) ]. to_sint8(to_uint8 x) =to_sint8 x
- axiom proj_int16 : forall x:int [ to_sint16(to_uint16 x) ]. to_sint16(to_uint16 x)=to_sint16 x
- axiom proj_int32 : forall x:int [ to_sint32(to_uint32 x) ]. to_sint32(to_uint32 x)=to_sint32 x
- axiom proj_int64 : forall x:int [ to_sint64(to_uint64 x) ]. to_sint64(to_uint64 x)=to_sint64 x
+ lemma id_uint8 : forall x:int [ to_uint8 x ]. is_uint8 x -> (to_uint8 x) = x
+ lemma id_sint8 : forall x:int [ to_sint8 x ]. is_sint8 x -> (to_sint8 x) = x
+ lemma id_uint16 : forall x:int [ to_uint16 x ]. is_uint16 x -> (to_uint16 x) = x
+ lemma id_sint16 : forall x:int [ to_sint16 x ]. is_sint16 x -> (to_sint16 x) = x
+ lemma id_uint32 : forall x:int [ to_uint32 x ]. is_uint32 x -> (to_uint32 x) = x
+ lemma id_sint32 : forall x:int [ to_sint32 x ]. is_sint32 x -> (to_sint32 x) = x
+ lemma id_uint64 : forall x:int [ to_uint64 x ]. is_uint64 x -> (to_uint64 x) = x
+ lemma id_sint64 : forall x:int [ to_sint64 x ]. is_sint64 x -> (to_sint64 x) = x
+
+ lemma id_uint8_inl : forall x: int [ to_uint8 x ].
+ 0 <= x < max_uint8 -> (to_uint8 x) = x
+ lemma id_sint8_inl : forall x: int [ to_sint8 x ].
+ - max_sint8 <= x < max_sint8 -> (to_sint8 x) = x
+ lemma id_uint16_inl : forall x: int [ to_uint16 x ].
+ 0 <= x < max_uint16 -> (to_uint16 x) = x
+ lemma id_sint16_inl : forall x: int [ to_sint16 x ].
+ - max_sint16 <= x < max_sint16 -> (to_sint16 x) = x
+ lemma id_uint32_inl : forall x: int [ to_uint32 x ].
+ 0 <= x < max_uint32 -> (to_uint32 x) = x
+ lemma id_sint32_inl : forall x: int [ to_sint32 x ].
+ - max_sint32 <= x < max_sint32 -> (to_sint32 x) = x
+ lemma id_uint64_inl : forall x: int [ to_uint64 x ].
+ 0 <= x < max_uint64 -> (to_uint64 x) = x
+ lemma id_sint64_inl : forall x: int [ to_sint64 x ].
+ - max_sint64 <= x < max_sint64 -> (to_sint64 x) = x
+
+ (** * C-Integer Conversions are projections * **)
+
+ let rec lemma proj_int8 (x: int)
+ ensures { to_sint8(to_uint8 x) = to_sint8 x }
+ variant { if x < - max_sint8 then max_sint8 - x else x }
+ = if x < - max_sint8 then proj_int8 (x + max_uint8) else
+ if max_uint8 <= x then proj_int8 (x - max_uint8)
+ else ()
+
+ let rec lemma proj_int16 (x: int)
+ ensures { to_sint16(to_uint16 x) = to_sint16 x }
+ variant { if x < - max_sint16 then max_sint16 - x else x }
+ = if x < - max_sint16 then proj_int16 (x + max_uint16) else
+ if max_uint16 <= x then proj_int16 (x - max_uint16)
+ else ()
+
+ let rec lemma proj_int32 (x: int)
+ ensures { to_sint32(to_uint32 x) = to_sint32 x }
+ variant { if x < - max_sint32 then max_sint32 - x else x }
+ = if x < - max_sint32 then proj_int32 (x + max_uint32) else
+ if max_uint32 <= x then proj_int32 (x - max_uint32)
+ else ()
+
+ let rec lemma proj_int64 (x: int)
+ ensures { to_sint64(to_uint64 x) = to_sint64 x }
+ variant { if x < - max_sint64 then max_sint64 - x else x }
+ = if x < - max_sint64 then proj_int64 (x + max_uint64) else
+ if max_uint64 <= x then proj_int64 (x - max_uint64)
+ else ()
end
--
GitLab