From 3dd30794611fa1e4344b0f7f3068211533b48f4f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Feb 2022 12:13:54 -0600 Subject: [PATCH] Fixes and additions for LFSC signatures (#8120) Fixes a critical issue in the re intersection rule, where a null terminator was missed. Also adds a sketch of the theory signature for floating points. --- proofs/lfsc/signatures/strings_rules.plf | 2 +- proofs/lfsc/signatures/theory_def.plf | 92 ++++++++++++++++++++++-- 2 files changed, 88 insertions(+), 6 deletions(-) diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf index 301d6f77b..5d4f5ad3d 100644 --- a/proofs/lfsc/signatures/strings_rules.plf +++ b/proofs/lfsc/signatures/strings_rules.plf @@ -107,7 +107,7 @@ (holds (or (and (= (str.len t) (int 0)) (and (= t emptystr) true)) (or (a.> (str.len t) (int 0)) false))))) (declare re_inter (! x term (! s term (! t term (! p1 (holds (str.in_re x s)) (! p2 (holds (str.in_re x t)) - (holds (str.in_re x (re.inter s t))))))))) + (holds (str.in_re x (re.inter s (re.inter t (re.* re.allchar))))))))))) (declare string_reduction (! r term (! t term (! s sort (! u (^ (sc_string_reduction t s) r) (holds r)))))))) diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index e797bcf41..da9689ab9 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -126,7 +126,7 @@ (declare f_store term) (define store (# x term (# y term (# z term (apply (apply (apply f_store x) y) z))))) (declare f_array_const (! s sort term)) -(define array_const (# x sort (# y term (apply (f_array_const x) y))) +(define array_const (# x sort (# y term (apply (f_array_const x) y)))) (declare f_eqrange term) (define eqrange (# x term (# y term (# z term (# w term (apply (apply (apply (apply f_eqrange x) y) z) w)))))) @@ -342,6 +342,85 @@ ; The empty bitvector, which is used as the null terminator of bvconcat chains (declare emptybv term) + +;; ---- Floating points + +; a floating point constant is indexed by 3 bitvector constants +(declare fp (! s bitvec (! e bitvec (! i bitvec term)))) +(declare f_fp.add term) +(define fp.add (# x term (# y term (# z term (apply (apply (apply f_fp.add x) y) z))))) +(declare f_fp.sub term) +(define fp.sub (# x term (# y term (# z term (apply (apply (apply f_fp.sub x) y) z))))) +(declare f_fp.mul term) +(define fp.mul (# x term (# y term (# z term (apply (apply (apply f_fp.mul x) y) z))))) +(declare f_fp.div term) +(define fp.div (# x term (# y term (# z term (apply (apply (apply f_fp.div x) y) z))))) +(declare f_fp.fma term) +(define fp.fma (# x term (# y term (# z term (# w term (apply (apply (apply (apply f_fp.fma x) y) z) w)))))) +(declare f_fp.sqrt term) +(define fp.sqrt (# x term (# y term (apply (apply f_fp.sqrt x) y)))) +(declare f_fp.rem term) +(define fp.rem (# x term (# y term (apply (apply f_fp.rem x) y)))) +(declare f_fp.roundToIntegral term) +(define fp.roundToIntegral (# x term (# y term (apply (apply f_fp.roundToIntegral x) y)))) +(declare f_fp.min term) +(define fp.min (# x term (# y term (apply (apply f_fp.min x) y)))) +(declare f_fp.max term) +(define fp.max (# x term (# y term (apply (apply f_fp.max x) y)))) +(declare f_fp.leq term) +(define fp.leq (# x term (# y term (apply (apply f_fp.leq x) y)))) +(declare f_fp.lt term) +(define fp.lt (# x term (# y term (apply (apply f_fp.lt x) y)))) +(declare f_fp.geq term) +(define fp.geq (# x term (# y term (apply (apply f_fp.geq x) y)))) +(declare f_fp.gt term) +(define fp.gt (# x term (# y term (apply (apply f_fp.gt x) y)))) +(declare f_fp.eq term) +(define fp.eq (# x term (# y term (apply (apply f_fp.eq x) y)))) +(declare f_to_fp_unsigned (! i mpz (! j mpz term))) +(define to_fp_unsigned (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_unsigned x y) z) w)))))) +(declare f_fp.to_ubv (! i mpz term)) +(define fp.to_ubv (# x mpz (# z term (# w term (apply (apply (f_fp.to_ubv x) z) w))))) +(declare f_fp.to_sbv (! i mpz term)) +(define fp.to_sbv (# x mpz (# z term (# w term (apply (apply (f_fp.to_sbv x) z) w))))) +(declare f_fp.abs term) +(define fp.abs (# x term (apply f_fp.abs x))) +(declare f_fp.neg term) +(define fp.neg (# x term (apply f_fp.neg x))) +(declare f_fp.isNormal term) +(define fp.isNormal (# x term (apply f_fp.isNormal x))) +(declare f_fp.isSubnormal term) +(define fp.isSubnormal (# x term (apply f_fp.isSubnormal x))) +(declare f_fp.isZero term) +(define fp.isZero (# x term (apply f_fp.isZero x))) +(declare f_fp.isInfinite term) +(define fp.isInfinite (# x term (apply f_fp.isInfinite x))) +(declare f_fp.isNaN term) +(define fp.isNaN (# x term (apply f_fp.isNaN x))) +(declare f_fp.isNegative term) +(define fp.isNegative (# x term (apply f_fp.isNegative x))) +(declare f_fp.isPositive term) +(define fp.isPositive (# x term (apply f_fp.isPositive x))) +(declare f_fp.to_real term) +(define fp.to_real (# x term (apply f_fp.to_real x))) +; to avoid overloading, must distinguish types +(declare f_to_fp_fp (! i mpz (! j mpz term))) +(define to_fp_fp (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_fp x y) z) w)))))) +(declare f_to_fp_real (! i mpz (! j mpz term))) +(define to_fp_real (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_real x y) z) w)))))) +(declare f_to_fp_sbv (! i mpz (! j mpz term))) +(define to_fp_sbv (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_sbv x y) z) w)))))) +(declare f_to_fp_generic (! i mpz (! j mpz term))) +(define to_fp_generic (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_generic x y) z) w)))))) +(declare f_to_fp_bv (! i mpz (! j mpz term))) +(define to_fp_bv (# x mpz (# y mpz (# z term (apply (f_to_fp_bv x y) z))))) +; rounding modes +(declare roundNearestTiesToEven term) +(declare roundNearestTiesToAway term) +(declare roundTowardPositive term) +(declare roundTowardNegative term) +(declare roundTowardZero term) + ;; ---- Sets (declare set.empty (! s sort term)) (declare set.universe (! s sort term)) @@ -410,12 +489,16 @@ (define bag.from_set (# x term (apply f_bag.from_set x))) (declare f_bag.to_set term) (define bag.to_set (# x term (apply f_bag.to_set x))) +(declare f_bag.member term) +(define bag.member (# x term (# y term (apply (apply f_bag.member x) y)))) (declare f_bag.map term) (define bag.map (# x term (# y term (apply (apply f_bag.map x) y)))) (declare f_bag.filter term) (define bag.filter (# x term (# y term (apply (apply f_bag.filter x) y)))) (declare f_bag.fold term) -(define bag.fold (# x term (# y term (apply (apply f_bag.fold x) y)))) +(define bag.fold (# x term (# y term (# z term (apply (apply (apply f_bag.fold x) y) z))))) +(declare f_table.product term) +(define table.product (# x term (# y term (apply (apply f_table.product x) y)))) ;; ---- Separation Logic (declare sep.nil (! s sort term)) @@ -434,6 +517,5 @@ (define SEP_LABEL (# x term (# y term (apply (apply f_SEP_LABEL x) y)))) ;; ---- UF with cardinality -; internally generated for finite model finding -(declare f_fmf.card term) -(define fmf.card (# x term (# y term (apply (apply f_fmf.card x) y)))) +; internally generated for finite model finding. Note this is an indexed constant. +(declare fmf.card (! s sort (! i mpz term))) -- 2.30.2