diff options
Diffstat (limited to 'src/lfsc/tests/signatures/th_bv.plf')
| -rw-r--r-- | src/lfsc/tests/signatures/th_bv.plf | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/src/lfsc/tests/signatures/th_bv.plf b/src/lfsc/tests/signatures/th_bv.plf new file mode 100644 index 0000000..0004b35 --- /dev/null +++ b/src/lfsc/tests/signatures/th_bv.plf @@ -0,0 +1,192 @@ +;;;; TEMPORARY: + +(declare trust-bad (th_holds false)) + +; helper stuff +(program mpz_sub ((x mpz) (y mpz)) mpz + (mp_add x (mp_mul (~1) y))) + +(program mp_ispos ((x mpz)) formula + (mp_ifneg x false true)) + +(program mpz_eq ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + +(program mpz_lt ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true false)) + +(program mpz_lte ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) + +(program mpz_ ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + + +; "bitvec" is a term of type "sort" +; (declare BitVec sort) +(declare BitVec (! n mpz sort)) + +; bit type +(declare bit type) +(declare b0 bit) +(declare b1 bit) + +; bit vector type used for constants +(declare bv type) +(declare bvn bv) +(declare bvc (! b bit (! v bv bv))) + +; calculate the length of a bitvector +;; (program bv_len ((v bv)) mpz +;; (match v +;; (bvn 0) +;; ((bvc b v') (mp_add (bv_len v') 1)))) + + +; a bv constant term +(declare a_bv + (! n mpz + (! v bv + (term (BitVec n))))) + +(program bv_constants_are_disequal ((x bv) (y bv)) formula + (match x + (bvn (fail formula)) + ((bvc bx x') + (match y + (bvn (fail formula)) + ((bvc by y') (match bx + (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true)))) + (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y')))) + )) + )) +)) + +(declare bv_disequal_constants + (! n mpz + (! x bv + (! y bv + (! c (^ (bv_constants_are_disequal x y) true) + (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y))))))))) + +; a bv variable +(declare var_bv type) +; a bv variable term +(declare a_var_bv + (! n mpz + (! v var_bv + (term (BitVec n))))) + +; bit vector binary operators +(define bvop2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (term (BitVec n)))))) + +(declare bvand bvop2) +(declare bvor bvop2) +(declare bvor bvop2) +(declare bvxor bvop2) +(declare bvnand bvop2) +(declare bvnor bvop2) +(declare bvxnor bvop2) +(declare bvmul bvop2) +(declare bvadd bvop2) +(declare bvsub bvop2) +(declare bvudiv bvop2) +(declare bvurem bvop2) +(declare bvsdiv bvop2) +(declare bvsrem bvop2) +(declare bvsmod bvop2) +(declare bvshl bvop2) +(declare bvlshr bvop2) +(declare bvashr bvop2) +(declare concat bvop2) + +; bit vector unary operators +(define bvop1 + (! n mpz + (! x (term (BitVec n)) + (term (BitVec n))))) + + +(declare bvneg bvop1) +(declare bvnot bvop1) +(declare rotate_left bvop1) +(declare rotate_right bvop1) + +(declare bvcomp + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (term (BitVec 1)))))) + + +(declare concat + (! n mpz + (! m mpz + (! m' mpz + (! t1 (term (BitVec m)) + (! t2 (term (BitVec m')) + (term (BitVec n)))))))) + +;; side-condition fails in signature only?? +;; (! s (^ (mp_add m m') n) + +;; (declare repeat bvopp) + +(declare extract + (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n)))))))) + +(declare zero_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare sign_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare repeat + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + + + +;; TODO: add checks for valid typing for these operators +;; (! c1 (^ (mpz_lte i j) +;; (! c2 (^ (mpz_lt i n) true) +;; (! c3 (^ (mp_ifneg i false true) true) +;; (! c4 (^ (mp_ifneg j false true) true) +;; (! s (^ (mp_add (mpz_sub i j) 1) m) + + +; bit vector predicates +(define bvpred + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + formula)))) + +(declare bvult bvpred) +(declare bvule bvpred) +(declare bvugt bvpred) +(declare bvuge bvpred) +(declare bvslt bvpred) +(declare bvsle bvpred) +(declare bvsgt bvpred) +(declare bvsge bvpred) |