From de97108f14129ea0ca1e0442f819be1fd4bd830b Mon Sep 17 00:00:00 2001 From: Japheth Lim Date: Thu, 18 Jul 2019 19:16:29 +1000 Subject: [PATCH] autocorres: exhaustive testsuite for arithmetic op word abstraction --- tools/autocorres/tests/examples/WordAbs.thy | 81 ++++++++++++++++++++- tools/autocorres/tests/examples/word_abs.c | 15 ++++ 2 files changed, 95 insertions(+), 1 deletion(-) diff --git a/tools/autocorres/tests/examples/WordAbs.thy b/tools/autocorres/tests/examples/WordAbs.thy index a1146cd39..60afb1aa7 100644 --- a/tools/autocorres/tests/examples/WordAbs.thy +++ b/tools/autocorres/tests/examples/WordAbs.thy @@ -15,7 +15,9 @@ begin external_file "word_abs.c" install_C_file "word_abs.c" autocorres - [ (*signed_word_abs = + [ (* signed_word_abs is implicit; these are the functions that would be abstracted: *) + (*signed_word_abs = + S_add_S S_sub_S S_mul_S S_div_S S_mod_S neg_S S_and_S S_or_S S_xor_S not_S U_shiftl_U_abs_S U_shiftr_U_abs_S U_shiftl_S_abs_S U_shiftr_S_abs_S S_shiftl_U_abs_S S_shiftr_U_abs_S S_shiftl_S_abs_S S_shiftr_S_abs_S @@ -28,6 +30,7 @@ autocorres S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U , unsigned_word_abs = ver366 + U_add_U U_sub_U U_mul_U U_div_U U_mod_U neg_U U_and_U U_or_U U_xor_U not_U U_shiftl_U_abs_U U_shiftr_U_abs_U U_shiftl_S_abs_U U_shiftr_S_abs_U S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U @@ -43,10 +46,84 @@ lemma "\ P \ ver366' 0 \ \v s. v = 0 \ P s lemma "\ P \ ver366' UINT_MAX \ \v s. v = UINT_MAX-1 \ P s \" by (wpsimp simp: ver366'_def UINT_MAX_def) +section \Arithmetic ops\ +thm S_add_S'_def S_sub_S'_def S_mul_S'_def S_div_S'_def S_mod_S'_def neg_S'_def + U_add_U'_def U_sub_U'_def U_mul_U'_def U_div_U'_def U_mod_U'_def neg_U'_def + +lemma "x + y < INT_MIN \ x + y > INT_MAX \ \ no_fail \ (S_add_S' (x::int) (y::int))" + by (monad_eq simp: S_add_S'_def no_fail_def INT_MIN_def INT_MAX_def) +lemma "\\s. INT_MIN \ x + y \ x + y \ INT_MAX \ P s\ + S_add_S' (x::int) (y::int) + \\r s. r = x + y \ P s\!" + by (wpsimp simp: S_add_S'_def INT_MIN_def INT_MAX_def) +lemma "x - y < INT_MIN \ x - y > INT_MAX \ \ no_fail \ (S_sub_S' (x::int) (y::int))" + by (monad_eq simp: S_sub_S'_def no_fail_def INT_MIN_def INT_MAX_def) +lemma "\\s. INT_MIN \ x - y \ x - y \ INT_MAX \ P s\ + S_sub_S' (x::int) (y::int) + \\r s. r = x - y \ P s\!" + by (wpsimp simp: S_sub_S'_def INT_MIN_def INT_MAX_def) +lemma "x * y < INT_MIN \ x * y > INT_MAX \ \ no_fail \ (S_mul_S' (x::int) (y::int))" + by (monad_eq simp: S_mul_S'_def no_fail_def INT_MIN_def INT_MAX_def) +lemma "\\s. INT_MIN \ x * y \ x * y \ INT_MAX \ P s\ + S_mul_S' (x::int) (y::int) + \\r s. r = x * y \ P s\!" + by (wpsimp simp: S_mul_S'_def INT_MIN_def INT_MAX_def) +lemma "y = 0 \ x sdiv y < INT_MIN \ x sdiv y > INT_MAX \ \ no_fail \ (S_div_S' (x::int) (y::int))" + by (monad_eq simp: S_div_S'_def no_fail_def INT_MIN_def INT_MAX_def) +lemma "\\s. y \ 0 \ INT_MIN \ x sdiv y \ x sdiv y \ INT_MAX \ P s\ + S_div_S' (x::int) (y::int) + \\r s. r = x sdiv y \ P s\!" + by (wpsimp simp: S_div_S'_def INT_MIN_def INT_MAX_def) +lemma "y = 0 \ x smod y < INT_MIN \ x smod y > INT_MAX \ \ no_fail \ (S_mod_S' (x::int) (y::int))" + by (monad_eq simp: S_mod_S'_def no_fail_def INT_MIN_def INT_MAX_def) +lemma "\\s. y \ 0 \ INT_MIN \ x smod y \ x smod y \ INT_MAX \ P s\ + S_mod_S' (x::int) (y::int) + \\r s. r = x smod y \ P s\!" + by (wpsimp simp: S_mod_S'_def INT_MIN_def INT_MAX_def) +lemma "x \ INT_MIN \ x > -INT_MIN \ \ no_fail \ (neg_S' (x::int))" + by (monad_eq simp: neg_S'_def no_fail_def INT_MIN_def) +lemma "\\s. INT_MIN < x \ x \ -INT_MIN \ P s\ neg_S' (x::int) \\r s. r = -x \ P s\!" + by (wpsimp simp: neg_S'_def INT_MIN_def) + +lemma "x + y > UINT_MAX \ \ no_fail \ (U_add_U' (x::nat) (y::nat))" + by (monad_eq simp: U_add_U'_def no_fail_def) +lemma "\\s. x + y \ UINT_MAX \ P s\ + U_add_U' (x::nat) (y::nat) + \\r s. r = x + y \ P s\!" + by (wpsimp simp: U_add_U'_def UINT_MAX_def) +lemma "x < y \ \ no_fail \ (U_sub_U' (x::nat) (y::nat))" + by (monad_eq simp: U_sub_U'_def no_fail_def) +lemma "\\s. x \ y \ P s\ + U_sub_U' (x::nat) (y::nat) + \\r s. r = x - y \ P s\!" + by (wpsimp simp: U_sub_U'_def) +lemma "x * y > UINT_MAX \ \ no_fail \ (U_mul_U' (x::nat) (y::nat))" + by (monad_eq simp: U_mul_U'_def no_fail_def) +lemma "\\s. x * y \ UINT_MAX \ P s\ + U_mul_U' (x::nat) (y::nat) + \\r s. r = x * y \ P s\!" + by (wpsimp simp: U_mul_U'_def UINT_MAX_def) +lemma "y = 0 \ \ no_fail \ (U_div_U' (x::nat) (y::nat))" + by (monad_eq simp: U_div_U'_def no_fail_def) +lemma "\\s. y \ 0 \ P s\ + U_div_U' (x::nat) (y::nat) + \\r s. r = x div y \ P s\!" + by (wpsimp simp: U_div_U'_def UINT_MAX_def) +lemma "y = 0 \ \ no_fail \ (U_mod_U' (x::nat) (y::nat))" + by (monad_eq simp: U_mod_U'_def no_fail_def) +lemma "\\s. y \ 0 \ P s\ + U_mod_U' (x::nat) (y::nat) + \\r s. r = x mod y \ P s\!" + by (wpsimp simp: U_mod_U'_def UINT_MAX_def) +lemma "\P\ neg_U' (x::nat) \\r s. r = (if x = 0 then 0 else Suc UINT_MAX - x) \ P s\!" + unfolding neg_U'_def by (wp, simp) + + section \Bitwise ops\ thm S_and_S'_def S_or_S'_def S_xor_S'_def not_S'_def U_and_U'_def U_or_U'_def U_xor_U'_def not_U'_def + lemma "\P\ S_and_S' (x::int) (y::int) \\r s. r = x AND y \ P s\!" by (wpsimp simp: S_and_S'_def) lemma "\P\ S_or_S' (x::int) (y::int) \\r s. r = x OR y \ P s\!" @@ -55,6 +132,7 @@ lemma "\P\ S_xor_S' (x::int) (y::int) \\r s. r = by (wpsimp simp: S_xor_S'_def) lemma "\P\ not_S' (x::int) \\r s. r = NOT x \ P s\!" by (wpsimp simp: not_S'_def) + lemma "\P\ U_and_U' (x::nat) (y::nat) \\r s. r = x AND y \ P s\!" by (wpsimp simp: U_and_U'_def) lemma "\P\ U_or_U' (x::nat) (y::nat) \\r s. r = x OR y \ P s\!" @@ -64,6 +142,7 @@ lemma "\P\ U_xor_U' (x::nat) (y::nat) \\r s. r = lemma "\P\ not_U' (x::nat) \\r s. r = UINT_MAX - x \ P s\!" by (wpsimp simp: not_U'_def) + section \Left shifts\ thm U_shiftl_U_abs_US'_def U_shiftr_U_abs_US'_def U_shiftl_S_abs_US'_def U_shiftr_S_abs_US'_def diff --git a/tools/autocorres/tests/examples/word_abs.c b/tools/autocorres/tests/examples/word_abs.c index c8c2d6409..31c3ffc16 100644 --- a/tools/autocorres/tests/examples/word_abs.c +++ b/tools/autocorres/tests/examples/word_abs.c @@ -14,6 +14,21 @@ unsigned ver366(unsigned x) { else return x - 1; } +/* All arithmetic operators */ +unsigned U_add_U(unsigned a, unsigned b) { return a + b; } +unsigned U_sub_U(unsigned a, unsigned b) { return a - b; } +unsigned U_mul_U(unsigned a, unsigned b) { return a * b; } +unsigned U_div_U(unsigned a, unsigned b) { return a / b; } +unsigned U_mod_U(unsigned a, unsigned b) { return a % b; } +unsigned neg_U(unsigned a) { return -a; } + +int S_add_S(int a, int b) { return a + b; } +int S_sub_S(int a, int b) { return a - b; } +int S_mul_S(int a, int b) { return a * b; } +int S_div_S(int a, int b) { return a / b; } +int S_mod_S(int a, int b) { return a % b; } +int neg_S(int a) { return -a; } + /* All bitwise operators */ unsigned U_and_U(unsigned a, unsigned b) { return a & b; } unsigned U_or_U (unsigned a, unsigned b) { return a | b; }