Commit 323642e8 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Add general case multiplication that uses Toom-Cook

parent 38bc296d
...@@ -553,8 +553,8 @@ end ...@@ -553,8 +553,8 @@ end
module mach.c.C module mach.c.C
prelude "#define IGNORE2(x,y) do {} while (0)" prelude "#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
interface "#define IGNORE2(x,y) do {} while (0)" interface "#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
syntax type ptr "%1 *" syntax type ptr "%1 *"
syntax type bool "int" (* ? *) syntax type bool "int" (* ? *)
...@@ -563,6 +563,9 @@ module mach.c.C ...@@ -563,6 +563,9 @@ module mach.c.C
syntax val free "free(%1)" syntax val free "free(%1)"
syntax val realloc "realloc(%1, (%2) * sizeof(%v0))" syntax val realloc "realloc(%1, (%2) * sizeof(%v0))"
syntax val salloc "alloca((%1) * sizeof(%v0))"
syntax val sfree "(void)(%1)"
(* syntax val is_null "(%1) == NULL" *) (* syntax val is_null "(%1) == NULL" *)
syntax val is_not_null "(%1) != NULL" syntax val is_not_null "(%1) != NULL"
syntax val null "NULL" syntax val null "NULL"
......
...@@ -35,7 +35,7 @@ tests: extract check-gmp ...@@ -35,7 +35,7 @@ tests: extract check-gmp
./build/minitests ./build/minitests
bench-tests: extract bench-tests: extract
gcc -O2 -Wall -g -std=c11 tests.c $(CFILES) -Ibench-include -Irandom -fomit-frame-pointer -fno-tree-vectorize -lgmp -o build/bench-tests gcc -O2 -Wall -Wno-unused-function -g -std=c11 tests.c $(CFILES) -Ibench-include -Irandom -fomit-frame-pointer -fno-tree-vectorize -lgmp -o build/bench-tests
build/why3%bench: extract check-gmp build/why3%bench: extract check-gmp
......
...@@ -55,12 +55,21 @@ module Lemmas ...@@ -55,12 +55,21 @@ module Lemmas
requires { 0 < c } requires { 0 < c }
ensures { c * a < c * b } ensures { c * a < c * b }
= () = ()
let lemma prod_compat_r (a b c:int) let lemma prod_compat_r (a b c:int)
requires { 0 <= a <= b } requires { 0 <= a <= b }
requires { 0 <= c } requires { 0 <= c }
ensures { c * a <= c * b } ensures { c * a <= c * b }
= () = ()
let lemma prod_compat_strict_lr (a b c d:int)
requires { 0 <= a < b }
requires { 0 <= c < d }
ensures { a * c < b * d }
= () (* assert { a * c < a * d = d * a < d * b = b * d } *)
meta remove_prop axiom prod_compat_strict_lr
(** {3 Integer value of a natural number} *) (** {3 Integer value of a natural number} *)
(** `value_sub x n m` denotes the integer represented by (** `value_sub x n m` denotes the integer represented by
...@@ -204,4 +213,14 @@ module Lemmas ...@@ -204,4 +213,14 @@ module Lemmas
= value_sub_concat (pelts x) x.offset (x.offset + p2i n) (x.offset + p2i m) = value_sub_concat (pelts x) x.offset (x.offset + p2i n) (x.offset + p2i m)
let lemma value_sub_eq (x1 x2: map int limb) (n1 n2 m1 m2: int)
requires { x1 = x2 }
requires { n1 = n2 }
requires { m1 = m2 }
ensures { value_sub x1 n1 m1 = value_sub x2 n2 m2 }
= ()
meta remove_prop axiom value_sub_eq
end end
...@@ -7,8 +7,8 @@ ...@@ -7,8 +7,8 @@
<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../lemmas.mlw" proved="true"> <file name="../lemmas.mlw">
<theory name="Lemmas" proved="true"> <theory name="Lemmas">
<goal name="VC map_eq_shift" expl="VC for map_eq_shift" proved="true"> <goal name="VC map_eq_shift" expl="VC for map_eq_shift" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC map_eq_shift.0" expl="postcondition" proved="true"> <goal name="VC map_eq_shift.0" expl="postcondition" proved="true">
...@@ -56,6 +56,9 @@ ...@@ -56,6 +56,9 @@
<goal name="VC prod_compat_r" expl="VC for prod_compat_r" proved="true"> <goal name="VC prod_compat_r" expl="VC for prod_compat_r" proved="true">
<proof prover="5" memlimit="2000"><result status="valid" time="0.02" steps="10"/></proof> <proof prover="5" memlimit="2000"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="VC prod_compat_strict_lr" expl="VC for prod_compat_strict_lr" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_sub" expl="VC for value_sub" proved="true"> <goal name="VC value_sub" expl="VC for value_sub" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC value_sub.0" expl="variant decrease" proved="true"> <goal name="VC value_sub.0" expl="variant decrease" proved="true">
...@@ -265,6 +268,8 @@ ...@@ -265,6 +268,8 @@
<goal name="VC value_concat" expl="VC for value_concat" proved="true"> <goal name="VC value_concat" expl="VC for value_concat" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="26"/></proof> <proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="26"/></proof>
</goal> </goal>
<goal name="VC value_sub_eq" expl="VC for value_sub_eq">
</goal>
</theory> </theory>
</file> </file>
</why3session> </why3session>
...@@ -312,10 +312,10 @@ module Mul ...@@ -312,10 +312,10 @@ module Mul
done; done;
!c !c
(** `wmpn_mul r x y sx sy` multiplies `(x, sx)` and `(y,sy)` and writes (** `wmpn_mul_basecase r x y sx sy` multiplies `(x, sx)` and `(y,sy)` and writes
the result in `(r, sx+sy)`. `sx` must be greater than or equal to the result in `(r, sx+sy)`. `sx` must be greater than or equal to
`sy`. Corresponds to `mpn_mul`. *) `sy`. Corresponds to `mpn_mul`. *)
let wmpn_mul (r x y:t) (sx sy:int32) : unit let wmpn_mul_basecase (r x y:t) (sx sy:int32) : unit
requires { 0 < sy <= sx } requires { 0 < sy <= sx }
requires { valid x sx } requires { valid x sx }
requires { valid y sy } requires { valid y sy }
......
This diff is collapsed.
...@@ -72,7 +72,7 @@ int main () { ...@@ -72,7 +72,7 @@ int main () {
/* Re-interpret reps argument as a size argument. */ /* Re-interpret reps argument as a size argument. */
init_genrand64((unsigned long long)time(NULL)); init_genrand64((unsigned long long)time(NULL));
max_n = 200; max_n = 1000;
max_add = 50; max_add = 50;
max_mul = 20; max_mul = 20;
max_toom = 95; max_toom = 95;
...@@ -215,8 +215,9 @@ int main () { ...@@ -215,8 +215,9 @@ int main () {
for (bn = 35; bn <= max_toom; bn += 2) for (bn = 35; bn <= max_toom; bn += 2)
{ {
mp_ptr ws = TMP_ALLOC_LIMBS(9 * bn / 2 + 32); //mp_ptr ws = TMP_ALLOC_LIMBS(9 * bn / 2 + 32);
an = (bn * 3) / 2; //an = (bn * 3) / 2;
an = bn * 6;
init_valid (ap, bp, an, bn); init_valid (ap, bp, an, bn);
#ifdef BENCH #ifdef BENCH
elapsed = 0; elapsed = 0;
...@@ -230,7 +231,7 @@ int main () { ...@@ -230,7 +231,7 @@ int main () {
mpn_mul (refp, ap, an, bp, bn); mpn_mul (refp, ap, an, bp, bn);
#endif #endif
#ifdef TEST_WHY3 #ifdef TEST_WHY3
toom32_mul (rp, ap, bp, ws, an, bn); wmpn_mul (rp, ap, bp, an, bn);
#endif #endif
#ifdef BENCH #ifdef BENCH
...@@ -257,6 +258,7 @@ int main () { ...@@ -257,6 +258,7 @@ int main () {
abort(); abort();
} }
#endif #endif
//free(ws);
} }
#ifdef COMPARE #ifdef COMPARE
printf ("toom ok\n"); printf ("toom ok\n");
......
This diff is collapsed.
...@@ -31,6 +31,9 @@ module C ...@@ -31,6 +31,9 @@ module C
val null () : ptr 'a val null () : ptr 'a
ensures { result.zone = null_zone } ensures { result.zone = null_zone }
val predicate is_not_null (p:ptr 'a) : bool
ensures { result <-> p.zone <> null_zone }
val incr (p:ptr 'a) (ofs:int32) : ptr 'a val incr (p:ptr 'a) (ofs:int32) : ptr 'a
requires { p.min <= p.offset + ofs <= p.max } requires { p.min <= p.offset + ofs <= p.max }
ensures { result.offset = p.offset + ofs } ensures { result.offset = p.offset + ofs }
...@@ -69,7 +72,8 @@ module C ...@@ -69,7 +72,8 @@ module C
p.min <= p.offset + i < p.max p.min <= p.offset + i < p.max
predicate valid (p:ptr 'a) (sz:int) = predicate valid (p:ptr 'a) (sz:int) =
in_bounds sz /\ 0 <= sz /\ 0 <= p.min <= p.offset /\ p.offset + sz <= p.max <= plength p in_bounds sz /\ 0 <= sz /\ 0 <= p.min <= p.offset
/\ p.offset + sz <= p.max <= plength p
let lemma valid_itv_to_shift (p:ptr 'a) (sz:int) let lemma valid_itv_to_shift (p:ptr 'a) (sz:int)
requires { valid p sz } requires { valid p sz }
...@@ -83,6 +87,19 @@ module C ...@@ -83,6 +87,19 @@ module C
ensures { result.min = 0 } ensures { result.min = 0 }
ensures { result.max = plength result } ensures { result.max = plength result }
exception StackOverflow
let salloc sz
requires { 0 <= sz }
ensures { plength result = sz }
ensures { result.offset = 0 }
ensures { result.min = 0 }
ensures { result.max = sz }
raises { StackOverflow -> true }
= let p = malloc sz in
if is_not_null p then p
else raise StackOverflow
val free (p:ptr 'a) : unit val free (p:ptr 'a) : unit
requires { p.offset = 0 } requires { p.offset = 0 }
requires { p.min = 0 } requires { p.min = 0 }
...@@ -90,6 +107,14 @@ module C ...@@ -90,6 +107,14 @@ module C
writes { p } writes { p }
writes { p.data } writes { p.data }
let sfree p
requires { p.offset = 0 }
requires { p.min = 0 }
requires { p.max = plength p }
writes { p }
writes { p.data }
= free p
val realloc (p:ptr 'a) (sz:int32) : ptr 'a val realloc (p:ptr 'a) (sz:int32) : ptr 'a
requires { 0 <= sz } requires { 0 <= sz }
requires { p.offset = 0 } requires { p.offset = 0 }
...@@ -107,9 +132,6 @@ module C ...@@ -107,9 +132,6 @@ module C
(pelts result)[i] = (pelts (old p))[i] } (pelts result)[i] = (pelts (old p))[i] }
ensures { result.zone = null_zone -> p = old p } ensures { result.zone = null_zone -> p = old p }
val predicate is_not_null (p:ptr 'a) : bool
ensures { result <-> p.zone <> null_zone }
val incr_split (p:ptr 'a) (i:int32) : ptr 'a val incr_split (p:ptr 'a) (i:int32) : ptr 'a
requires { 0 <= i } requires { 0 <= i }
requires { p.min <= p.offset + i <= p.max } requires { p.min <= p.offset + i <= p.max }
......
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