Commit a04e9bdc authored by Clément Fumex's avatar Clément Fumex
Browse files

add current ieee_float theory & drivers for z3 + a first test example

parent 22408364
theory ieee_float.RoundingMode
syntax type mode "RoundingMode"
syntax function RNE "RNE"
syntax function RNA "RNA"
syntax function RTP "RTP"
syntax function RTN "RTN"
syntax function RTZ "RTZ"
end
theory ieee_float.GenericFloat
(* Part I *)
syntax function abs "(fp.abs %1)"
syntax function neg "(fp.neg %1)"
syntax function add "(fp.add %1 %2 %3)"
syntax function sub "(fp.sub %1 %2 %3)"
syntax function mul "(fp.mul %1 %2 %3)"
syntax function div "(fp.div %1 %2 %3)"
syntax function fma "(fp.fma %1 %2 %3 %4)"
syntax function sqrt "(fp.sqrt %1 %2)"
syntax function rem "(fp.rem %1 %2)"
syntax function roundToIntegral "(fp.roundToIntegral %1 %2)"
syntax function min "(fp.min %1 %2)"
syntax function max "(fp.max %1 %2)"
syntax predicate le "(fp.leq %1 %2)"
syntax predicate lt "(fp.lt %1 %2)"
syntax predicate ge "(fp.geq %1 %2)"
syntax predicate gt "(fp.gt %1 %2)"
syntax predicate eq "(fp.eq %1 %2)"
syntax predicate is_normal "(fp.isNormal %1)"
syntax predicate is_subnormal "(fp.isSubnormal %1)"
syntax predicate is_zero "(fp.isZero %1)"
syntax predicate is_infinite "(fp.isInfinite %1)"
syntax predicate is_nan "(fp.isNaN %1)"
syntax predicate is_positive "(fp.isPositive %1)"
syntax predicate is_negative "(fp.isNegative %1)"
syntax predicate is_finite "(not (or (fp.isInfinite %1) (fp.isNaN %1)))"
syntax function to_real "(fp.to_real %1)"
syntax predicate overflow_value "true"
syntax predicate sign_zero_result "true"
(* Part II *)
remove allprops
end
theory ieee_float.Float32
(* Part I *)
syntax type t "Float32"
syntax converter from_binary "((_ to_fp 8 24) ((_ int2bv 32) %1))"
syntax converter (!_) "((_ to_fp 8 24) %1 %2)"
syntax function zeroF "((_ to_fp 8 24) #x00000000)"
syntax function half "((_ to_fp 8 24) #x3F000000)"
remove allprops
end
theory ieee_float.Float64
(* Part I *)
syntax type t "Float64"
syntax converter from_binary "((_ to_fp 11 53) ((_ int2bv 64) %1))"
syntax converter (!_) "((_ to_fp 11 53) %1 %2)"
syntax function zeroF "((_ to_fp 11 53) #x0000000000000000)"
syntax function half "((_ to_fp 11 53) #x3FE0000000000000)"
remove allprops
end
theory ieee_float.FloatConverter
(* Part I *)
syntax function to_float32 "((_ to_fp 8 24) %1 %2)"
syntax function to_float64 "((_ to_fp 11 53) %1 %2)"
remove allprops
end
theory ieee_float.Float_BV_Converter
(* Part I *)
syntax function to_ubv8 "((_ fp.to_ubv 8) %1 %2)"
syntax function to_ubv16 "((_ fp.to_ubv 16) %1 %2)"
syntax function to_ubv32 "((_ fp.to_ubv 32) %1 %2)"
syntax function to_ubv64 "((_ fp.to_ubv 64) %1 %2)"
remove allprops
end
theory ieee_float.Float32_BV_Converter
(* Part I *)
syntax function of_ubv8 "((_ to_fp_unsigned 8 24) %1 %2)"
syntax function of_ubv16 "((_ to_fp_unsigned 8 24) %1 %2)"
syntax function of_ubv32 "((_ to_fp_unsigned 8 24) %1 %2)"
syntax function of_ubv64 "((_ to_fp_unsigned 8 24) %1 %2)"
remove allprops
end
theory ieee_float.Float64_BV_Converter
(* Part I *)
syntax function of_ubv8 "((_ to_fp_unsigned 11 53) %1 %2)"
syntax function of_ubv16 "((_ to_fp_unsigned 11 53) %1 %2)"
syntax function of_ubv32 "((_ to_fp_unsigned 11 53) %1 %2)"
syntax function of_ubv64 "((_ to_fp_unsigned 11 53) %1 %2)"
remove allprops
end
......@@ -7,9 +7,9 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "smt-libv2-floats.gen"
import "discrimination.gen"
transformation "inline_trivial"
......@@ -110,3 +110,23 @@ theory bv.BV8
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory ieee_float.Float64
(* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
syntax function to_int
"(ite (= ((_ extract 1024 1024) ((_ fp.to_sbv 1025) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 1025) %1 %2)) (- (bv2int ((_ fp.to_sbv 1025) %1 %2)) (bv2int (bvshl (_ bv1 1026) (_ bv1025 1026)))))"
syntax function of_int
"((_ to_fp 11 53) %1 (ite (< %2 0) ((_ int2bv 1025) (+ (bv2int (bvshl (_ bv1 1026) (_ bv1025 1026))) %2)) ((_ int2bv 1025) %2)))"
end
theory ieee_float.Float32
(* check the sign bit; if pos |%1| else |%1| - 2^129 *)
syntax function to_int
"(ite (= ((_ extract 128 128) ((_ fp.to_sbv 129) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 129) %1 %2)) (- (bv2int ((_ fp.to_sbv 129) %1 %2)) (bv2int (bvshl (_ bv1 130) (_ bv129 130)))))"
syntax function of_int
"((_ to_fp 8 24) %1 (ite (< %2 0) ((_ int2bv 129) (+ (bv2int (bvshl (_ bv1 130) (_ bv129 130))) %2)) ((_ int2bv 129) %2)))"
end
theory real.Square
remove allprops
end
module TestIeeeFloat
use import ieee_float.Float32
use real.Abs
lemma Test00: forall x:t. abs x .<= (of_int RNE 2) -> .- (of_int RNE 3) .<= x
lemma Test01:
forall x:t.
.-(of_int RNE 2) .<= x .<= (of_int RNE 2) -> zeroF .<= x .* x .<= (of_int RNE 4)
end
module M603_018
use import ieee_float.Float32
constant x : t = zeroF
constant y : t = of_int RNE 1
constant z : t = half
constant t : t = (x .+ y) ./ (of_int RNE 2)
let triplet (x y z : t)
requires { x .<= z /\ z .<= y }
requires { .-(of_int RNE 1) .<= x /\ x .<= (of_int RNE 10) }
requires { y .= x .+ (of_int RNE 1) }
requires { roundToIntegral RTN z = x }
requires { roundToIntegral RTP z = y }
=
let t = (x .+ y) ./ (of_int RNE 2) in
assert { roundToIntegral RTN x .= x };
assert { roundToIntegral RTN y .= y };
assert { roundToIntegral RTN z .= x };
assert { roundToIntegral RTN t .= x };
assert { roundToIntegral RTP x .= x };
assert { roundToIntegral RTP y .= y };
assert { roundToIntegral RTP z .= y };
assert { roundToIntegral RTP t .= y };
assert { x .<= z /\ z .<= y };
assert { x .<= t /\ t .<= y };
()
goal G1: roundToIntegral RTN x .= x
goal G2: roundToIntegral RTN y .= y
goal G3: roundToIntegral RTN z .= x
goal G4: roundToIntegral RTN t .= x
goal G5: roundToIntegral RTP x .= x
goal G6: roundToIntegral RTP y .= y
goal G7: roundToIntegral RTP z .= y
goal G8: roundToIntegral RTP t .= y
goal G9: x .<= z /\ z .<= y
goal G10: x .<= t /\ t .<= y
end
module M121_039_nonlinear
use import ieee_float.Float32
constant max : t = of_int RNE 340282346638528859811704183484516925440
constant min : t = .- max
constant one : t = of_int RNE 1
constant zero : t = zeroF
predicate in_range (x :t) = min .<= x .<= max
(* predicate axiom_mult t t t *)
(* axiom axiom_mult : forall a b y. *)
(* axiom_mult a b y = if a .<= b /\ y .<= zero then a .* y .>= b .* y else false *)
predicate axiom_mult (a b y : t) =
if a .<= b /\ y .<= zero then a .* y .>= b .* y else false
let test (a x y:t)
requires { zero .<= a .<= one }
requires { .- one .<= x .<= one }
requires { .- one .<= y .<= one }
requires { x .> zero /\ y .< zero /\ x .+ y .>= zero }
ensures { result .>= zero /\ result .<= (of_int RNE 2) }
=
assert { axiom_mult a one y };
assert { a .>= zero };
assert { a .<= one };
assert { x .> zero };
assert { y .<= zero };
assert { y .* a .<= zero };
assert { y .* a .>= y .* one };
assert { x .+ y .* a .>= x .+ y };
assert { x .+ y .>= zero };
assert { x .+ y .* a .>= zero };
x .+ y .* a
end
module LB09_025_conversion
use import ieee_float.Float32
use import int.Int
let fti x
requires { x .>= of_int RNE (-2147483648) /\ x .+ (of_int RNE 1) .<= of_int RNE 2147483647 }
ensures { of_int RNE result .>= x .- (of_int RNE 1) }
ensures { of_int RNE result .<= x .+ (of_int RNE 1) }
ensures { result = to_int RNE x }
=
to_int RNE x
end
module Test
use import ieee_float.Float32
goal G1: forall x. is_finite x -> x .- half .<= roundToIntegral RNA x .<= x .+ half
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Z3" version="4.4.2" timelimit="11" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="11" steplimit="0" memlimit="4000"/>
<prover id="3" name="Alt-Ergo" version="1.01" timelimit="11" steplimit="0" memlimit="4000"/>
<file name="../ieee_float.mlw" expanded="true">
<theory name="TestIeeeFloat" sum="9626577688521ad42852a971b5d056ff" expanded="true">
<goal name="Test00" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Test01" expanded="true">
<proof prover="1"><result status="valid" time="12.50"/></proof>
</goal>
</theory>
<theory name="M603_018" sum="edea63e177c099c0def0aaed6f99c750" expanded="true">
<goal name="WP_parameter triplet" expl="VC for triplet" expanded="true">
<proof prover="1"><result status="timeout" time="10.56"/></proof>
<proof prover="2"><result status="unknown" time="5.39"/></proof>
<proof prover="3"><result status="highfailure" time="9.25"/></proof>
</goal>
<goal name="G1" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="G3" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G4" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G6" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="G7" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G8" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G9" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="3"><result status="valid" time="0.11" steps="140"/></proof>
</goal>
<goal name="G10" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="M121_039_nonlinear" sum="673222610c1bf6e6c9111b886ac4347f" expanded="true">
<goal name="WP_parameter test" expl="VC for test" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter test.1" expl="1. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="10.57"/></proof>
<proof prover="2"><result status="timeout" time="12.06"/></proof>
<proof prover="3"><result status="highfailure" time="4.29"/></proof>
</goal>
<goal name="WP_parameter test.2" expl="2. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter test.3" expl="3. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter test.4" expl="4. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter test.5" expl="5. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="WP_parameter test.6" expl="6. assertion" expanded="true">
<proof prover="1"><result status="valid" time="2.35"/></proof>
</goal>
<goal name="WP_parameter test.7" expl="7. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="10.94"/></proof>
<proof prover="2"><result status="timeout" time="11.94"/></proof>
<proof prover="3"><result status="highfailure" time="4.28"/></proof>
</goal>
<goal name="WP_parameter test.8" expl="8. assertion" expanded="true">
<proof prover="1"><result status="timeout" time="10.79"/></proof>
<proof prover="2"><result status="timeout" time="11.91"/></proof>
<proof prover="3"><result status="highfailure" time="4.46"/></proof>
</goal>
<goal name="WP_parameter test.9" expl="9. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter test.10" expl="10. assertion" expanded="true">
<proof prover="1"><result status="valid" time="0.18"/></proof>
<proof prover="2"><result status="valid" time="3.11"/></proof>
</goal>
<goal name="WP_parameter test.11" expl="11. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="7.39"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LB09_025_conversion" sum="1cce16b73b44bb26d7c42668659aa4ff" expanded="true">
<goal name="WP_parameter fti" expl="VC for fti" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fti.1" expl="1. postcondition" expanded="true">
<proof prover="1"><result status="timeout" time="10.83"/></proof>
<proof prover="2"><result status="timeout" time="11.82"/></proof>
<proof prover="3"><result status="highfailure" time="4.78"/></proof>
</goal>
<goal name="WP_parameter fti.2" expl="2. postcondition" expanded="true">
<proof prover="1"><result status="timeout" time="10.46"/></proof>
<proof prover="2"><result status="timeout" time="12.01"/></proof>
<proof prover="3"><result status="highfailure" time="5.88"/></proof>
</goal>
<goal name="WP_parameter fti.3" expl="3. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Test" sum="ee987103086bb1677a6382ca333aeb34" expanded="true">
<goal name="G1" expanded="true">
<proof prover="1"><result status="timeout" time="21.63"/></proof>
<proof prover="2"><result status="timeout" time="11.78"/></proof>
<proof prover="3"><result status="highfailure" time="5.56"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -72,7 +72,10 @@ let ident_printer () =
"BitVec"; "extract"; "bv2nat"; "nat2bv";
(* From Z3 *)
"map"; "bv"; "subset"; "union"; "default"
"map"; "bv"; "subset"; "union"; "default";
(* floats *)
"RNE"; "RNA"; "RTP"; "RTN"; "RTZ"
]
in
let san = sanitizer char_to_alpha char_to_alnumus in
......
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment