Commit 484e6603 authored by MARCHE Claude's avatar MARCHE Claude

provers with BV specific support

parent d9a3aab4
......@@ -9,7 +9,6 @@ model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
......
(** Why3 driver for Z3 >= 4.3.2 *)
(* Do not set any logic, let z3 choose by itself
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
......@@ -30,7 +30,7 @@ editor = "altgr-ergo"
# CVC4 version 1.5-prerelease
[ATP cvc4]
name = "CVC4"
name = "CVC4 (BV)"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
exec = "cvc4-1.5"
......@@ -41,9 +41,26 @@ version_ok = "1.5"
driver = "drivers/cvc4_15.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --lang=smt2 %f"
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%l/why3-cpulimit %U %m -s %e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version 1.4, using SMTLIB fixed-size bitvectors
[ATP cvc4]
name = "CVC4 (BV)"
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.4"
driver = "drivers/cvc4_15.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
# CVC4 version 1.4
[ATP cvc4]
name = "CVC4"
......@@ -52,7 +69,7 @@ exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.4"
driver = "drivers/cvc4_14.drv"
driver = "drivers/cvc4.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
......@@ -300,12 +317,23 @@ command = "%l/why3-cpulimit %t %m -s %e --disable-print-success --enable-simp \
driver = "drivers/verit.drv"
version_old = "201310"
# Z3 with BV support
[ATP z3]
name = "Z3 (BV)"
exec = "z3"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.4.0"
driver = "drivers/z3_440.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s %e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
# Z3 4.3.2 does not support option global option -rs anymore.
# use settings given by "z3 -p" instead
# Z3 4.3.2 supports Datatypes
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.4.0"
exec = "z3-4.3.2"
version_switch = "-version"
......
......@@ -158,6 +158,8 @@ theory BV_Gen
forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
nth (lsr b s) n = False
lemma lsr_zero: forall x. lsr x 0 = x
function asr t int : t
axiom Asr_nth_low:
......@@ -168,6 +170,8 @@ theory BV_Gen
forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
nth (asr b s) n = nth b (size-1)
lemma asr_zero: forall x. asr x 0 = x
function lsl t int : t
axiom Lsl_nth_high:
......@@ -178,6 +182,8 @@ theory BV_Gen
forall b:t,n s:int. 0 <= n < s ->
nth (lsl b s) n = False
lemma lsl_zero: forall x. lsr x 0 = x
use import Pow2int
use import int.EuclideanDivision
......@@ -197,13 +203,18 @@ theory BV_Gen
axiom to_int_extensionality:
forall v,v':t. to_int v = to_int v' -> v = v'
(*
predicate uint_in_range (i : int) = (Int.(<=) 0 i) /\ (Int.(<=) i max_int)
*)
axiom to_uint_bounds :
(*
forall v:t. uint_in_range (to_uint v)
*)
forall v:t. 0 <= to_uint v < two_power_size
axiom to_uint_of_int :
forall i. uint_in_range i -> to_uint (of_int i) = i
forall i. 0 <= i < two_power_size -> to_uint (of_int i) = i
constant size_bv : t = of_int size
......@@ -244,10 +255,18 @@ theory BV_Gen
function add (v1 v2 : t) : t
axiom to_uint_add:
forall v1 v2. to_uint (add v1 v2) = mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
lemma to_uint_add_bounded:
forall v1 v2.
to_uint v1 + to_uint v2 < two_power_size ->
to_uint (add v1 v2) = to_uint v1 + to_uint v2
function sub (v1 v2 : t) : t
axiom to_uint_sub:
forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
lemma to_uint_sub_bounded:
forall v1 v2.
0 <= to_uint v1 - to_uint v2 < two_power_size ->
to_uint (sub v1 v2) = to_uint v1 - to_uint v2
function neg (v1 : t) : t
axiom to_uint_neg:
......@@ -256,6 +275,10 @@ theory BV_Gen
function mul (v1 v2 : t) : t
axiom to_uint_mul:
forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
lemma to_uint_mul_bounded:
forall v1 v2.
to_uint v1 * to_uint v2 < two_power_size ->
to_uint (mul v1 v2) = to_uint v1 * to_uint v2
function udiv (v1 v2 : t) : t
axiom to_uint_udiv:
......@@ -273,7 +296,7 @@ theory BV_Gen
nth x (to_uint i) = nth_bv x i
axiom Nth_bv_is_nth2:
forall x i. uint_in_range i ->
forall x i. 0 <= i < two_power_size ->
nth_bv x (of_int i) = nth x i
(** logical shift right *)
......@@ -348,6 +371,13 @@ theory BV64
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
meta "remove_prop" prop to_uint_add
meta "remove_prop" prop to_uint_sub
meta "remove_prop" prop to_uint_mul
end
theory BV32
......@@ -359,6 +389,13 @@ theory BV32
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
meta "remove_prop" prop to_uint_add
meta "remove_prop" prop to_uint_sub
meta "remove_prop" prop to_uint_mul
end
theory BV16
......@@ -370,6 +407,13 @@ theory BV16
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
meta "remove_prop" prop to_uint_add
meta "remove_prop" prop to_uint_sub
meta "remove_prop" prop to_uint_mul
end
theory BV8
......@@ -381,6 +425,13 @@ theory BV8
constant size = size,
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
meta "remove_prop" prop to_uint_add
meta "remove_prop" prop to_uint_sub
meta "remove_prop" prop to_uint_mul
end
(** {2 Generic Converter} *)
......@@ -390,8 +441,6 @@ theory BVConverter_Gen
type bigBV
type smallBV
constant pow2_smallSize_Bv : int
predicate in_small_range bigBV
function to_uint_small smallBV : int
......@@ -422,7 +471,6 @@ theory BVConverter_32_64
type bigBV = BV64.t,
type smallBV = BV32.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV32.two_power_size,
function to_uint_small = BV32.to_uint,
function to_uint_big = BV64.to_uint
end
......@@ -437,7 +485,6 @@ theory BVConverter_16_64
type bigBV = BV64.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV16.two_power_size,
function to_uint_small = BV16.to_uint,
function to_uint_big = BV64.to_uint
end
......@@ -452,7 +499,6 @@ theory BVConverter_8_64
type bigBV = BV64.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV8.two_power_size,
function to_uint_small = BV8.to_uint,
function to_uint_big = BV64.to_uint
end
......@@ -467,7 +513,6 @@ theory BVConverter_16_32
type bigBV = BV32.t,
type smallBV = BV16.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV16.two_power_size,
function to_uint_small = BV16.to_uint,
function to_uint_big = BV32.to_uint
end
......@@ -482,7 +527,6 @@ theory BVConverter_8_32
type bigBV = BV32.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV8.two_power_size,
function to_uint_small = BV8.to_uint,
function to_uint_big = BV32.to_uint
end
......@@ -497,7 +541,6 @@ theory BVConverter_8_16
type bigBV = BV16.t,
type smallBV = BV8.t,
predicate in_small_range = in_range,
constant pow2_smallSize_Bv = BV8.two_power_size,
function to_uint_small = BV8.to_uint,
function to_uint_big = BV16.to_uint
end
Markdown is supported
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