Commit f1c55bac authored by Clément Fumex's avatar Clément Fumex

Driver smt-libv2 factorisé (pour cvc4 et z3)

Module bitvec
parent 6d215c15
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for CVC4"
prelude "(set-logic AUFNIRA)"
prelude "(set-logic AUFNIRA)" (* how come bv is supported by cvc4 in this logic ?!? *)
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)" *)
printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; this is a prelude for CVC4 integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude ";;; this is a prelude for CVC4 real arithmetic"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
end
import "smt-libv2.drv"
(* CVC4 division seems to be neither the Euclidean one,
nor the Computer one *)
......@@ -164,93 +30,6 @@ theory int.ComputerDivision
end
*)
(*
theory real.Truncate
syntax function floor "(to_int %1)"
remove prop Floor_down
remove prop Floor_monotonic
end
*)
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding : lskept" function const
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
(* syntax function const "(const[%t0] %1)" *)
end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax function to_uint "(bv2nat %1)"
syntax function to_int "(ite (= ((_ extract 31 31) %1) #b0)
(bv2nat %1)
(- (bv2nat %1) 4294967296))"
syntax function of_int "((_ int2bv 32) %1)"
syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)"
syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_and
remove prop Nth_bw_or
remove prop Nth_bw_xor
remove prop Nth_bw_not
(* remove prop Add_is_add *)
(* remove prop Min_is_min *)
(* remove prop Neg_is_neg *)
(* remove prop Mul_is_mul *)
(* remove prop Udiv_is_udiv *)
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
end
(*
Local Variables:
mode: why
......
This diff is collapsed.
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for Z3"
prelude "(set-logic AUFNIRA)"
printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; this is a prelude for Z3 integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude ";;; this is a prelude for Z3 real arithmetic"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
end
import "smt-libv2.drv"
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
......@@ -157,26 +20,6 @@ theory real.FromInt
remove prop Neg
end
(*
theory real.Truncate
syntax function floor "(to_int %1)"
remove prop Floor_down
remove prop Floor_monotonic
end
*)
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding : lskept" function const
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
(* syntax function const "(const[%t0] %1)" *)
end
(*
Local Variables:
mode: why
......
This diff is collapsed.
(* module BitVectors *)
(* use import int.Int *)
(* use import int.Power *)
(* use import int.EuclideanDivision *)
(* use import bv.BitVector *)
(* type bitvec = t *)
(* (\* shifts and rotations *\) *)
(* val lsl (x : bitvec) (n : bitvec) : bitvec *)
(* requires{ 0 <= to_uint n < 32 } *)
(* ensures{ result = lsl_bv x n } *)
(* ensures{ to_uint result = mod ( to_uint x * ( power 2 ( to_uint n ) ) ) powSize } *)
(* val lsr (x : bitvec) (n : bitvec) : bitvec *)
(* requires{ 0 <= to_uint n < 32 } *)
(* ensures{ result = lsr_bv x n } *)
(* ensures{ to_uint result = div ( to_uint x ) ( power 2 ( to_uint n ) ) } *)
(* val asr (x : bitvec) (n : bitvec) : bitvec (\* Check that ! | find better *\) *)
(* requires{ 0 <= to_uint n < 32 } *)
(* ensures{ result = asr_bv x n } *)
(* ensures{ to_int result = div ( to_int x ) ( power 2 ( to_uint n ) ) } *)
(* val rotate_left (x : bitvec) : bitvec *)
(* ensures{ result = rotate_left x } *)
(* val rotate_right (x : bitvec) : bitvec *)
(* ensures{ result = rotate_right x } *)
(* (\* bitwise operations *\) *)
(* val bw_and (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = bw_and x y } *)
(* val bw_or (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = bw_or x y } *)
(* val bw_xor (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = bw_xor x y } *)
(* val bw_not (x : bitvec) : bitvec *)
(* ensures{ result = bw_not x } *)
(* (\* arithmetic operations *\) *)
(* val add (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = add x y } *)
(* ensures{ to_uint result = mod ( to_uint x + to_uint y ) powSize } *)
(* val sub (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = sub x y } *)
(* ensures{ to_uint result = mod ( to_uint x - to_uint y ) powSize } *)
(* val neg (x : bitvec) : bitvec *)
(* ensures{ result = neg x } *)
(* ensures{ to_uint result = mod ( - to_uint x ) powSize } *)
(* val mul (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = mul x y } *)
(* ensures{ to_uint result = mod ( to_uint x * to_uint y ) powSize } *)
(* val udiv (x : bitvec) (y : bitvec) : bitvec *)
(* ensures{ result = udiv x y } *)
(* ensures{ to_uint result = mod ( div ( to_uint x ) ( to_uint y ) ) powSize } *)
(* (\* comparison *\) *)
(* val eq (x : bitvec) (y : bitvec) : bool *)
(* ensures{ result = eq x y } *)
(* ensures{ result = (=) ( to_uint x ) ( to_uint y ) } *)
(* val ult (x : bitvec) (y : bitvec) : bool *)
(* ensures{ result = ult x y } *)
(* ensures{ result = (<) ( to_uint x ) ( to_uint y ) } *)
(* val ule (x : bitvec) (y : bitvec) : bool *)
(* ensures{ result = ule x y } *)
(* ensures{ result = (<=) ( to_uint x ) ( to_uint y ) } *)
(* val ugt (x : bitvec) (y : bitvec) : bool *)
(* ensures{ result = ugt x y } *)
(* ensures{ result = (>) ( to_uint x ) ( to_uint y ) } *)
(* val uge (x : bitvec) (y : bitvec) : bool *)
(* ensures{ result = uge x y } *)
(* ensures{ result = (>=) ( to_uint x ) ( to_uint y ) } *)
(* end *)
module BitVector_32
use import int.Int
use import int.Power
use import int.EuclideanDivision
use export bv.BV32
type bitvec32 = t
(* shifts and rotations *)
val lsl (x : bitvec32) (n : bitvec32) : bitvec32
requires{ 0 <= to_uint n < 32 }
ensures{ result = lsl_bv x n }
ensures{ to_uint result = mod ( to_uint x * ( power 2 ( to_uint n ) ) ) two_power_size }
val lsr (x : bitvec32) (n : bitvec32) : bitvec32
requires{ 0 <= to_uint n < 32 }
ensures{ result = lsr_bv x n }
ensures{ to_uint result = div ( to_uint x ) ( power 2 ( to_uint n ) ) }
val asr (x : bitvec32) (n : bitvec32) : bitvec32 (* Check that ! | find better *)
requires{ 0 <= to_uint n < 32 }
ensures{ result = asr_bv x n }
ensures{ to_int result = div ( to_int x ) ( power 2 ( to_uint n ) ) }
val rotate_left (x : bitvec32) : bitvec32
ensures{ result = rotate_left x }
val rotate_right (x : bitvec32) : bitvec32
ensures{ result = rotate_right x }
(* bitwise operations *)
val bw_and (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = bw_and x y }
val bw_or (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = bw_or x y }
val bw_xor (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = bw_xor x y }
val bw_not (x : bitvec32) : bitvec32
ensures{ result = bw_not x }
(* arithmetic operations *)
val add (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = add x y }
ensures{ to_uint result = mod ( to_uint x + to_uint y ) two_power_size }
val sub (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = sub x y }
ensures{ to_uint result = mod ( to_uint x - to_uint y ) two_power_size }
val neg (x : bitvec32) : bitvec32
ensures{ result = neg x }
ensures{ to_uint result = mod ( - to_uint x ) two_power_size }
val mul (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = mul x y }
ensures{ to_uint result = mod ( to_uint x * to_uint y ) two_power_size }
val udiv (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = udiv x y }
ensures{ to_uint result = mod ( div ( to_uint x ) ( to_uint y ) ) two_power_size }
val urem (x : bitvec32) (y : bitvec32) : bitvec32
ensures{ result = urem x y}
ensures{ to_uint result = mod (to_uint x) (to_uint y) }
(* comparison *)
val eq (x : bitvec32) (y : bitvec32) : bool
ensures{ result = eq x y }
ensures{ result = (=) ( to_uint x ) ( to_uint y ) }
val ult (x : bitvec32) (y : bitvec32) : bool
ensures{ result = ult x y }
ensures{ result = (<) ( to_uint x ) ( to_uint y ) }
val ule (x : bitvec32) (y : bitvec32) : bool
ensures{ result = ule x y }
ensures{ result = (<=) ( to_uint x ) ( to_uint y ) }
val ugt (x : bitvec32) (y : bitvec32) : bool
ensures{ result = ugt x y }
ensures{ result = (>) ( to_uint x ) ( to_uint y ) }
val uge (x : bitvec32) (y : bitvec32) : bool
ensures{ result = uge x y }
ensures{ result = (>=) ( to_uint x ) ( to_uint y ) }
end
......@@ -53,7 +53,7 @@ let ident_printer =
"concat"; "bvnot"; "bvand"; "bvor"; "bvneg"; "bvadd"; "bvmul"; "bvudiv";
"bvurem"; "bvshl"; "bvlshr"; "bvult"; "bvnand"; "bvnor"; "bvxor";
"bvcomp"; "bvsub"; "bvsdiv"; "bvsrem"; "bvsmod"; "bvashr"; "bvule";
"bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge";
"bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left"; "rotate_right";
(** Other stuff that Why3 seems to need *)
"DECIMAL"; "NUMERAL"; "par"; "STRING";
......
This diff is collapsed.
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