Commit a1cc4c0a authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Add support for mutually recursive definitions in C extractions

Toom multiplication can now be extracted
parent 8c916bc6
......@@ -27,17 +27,17 @@ module mach.int.Int32
syntax type int32 "int32_t"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
end
module mach.int.UInt32Gen
......@@ -53,16 +53,17 @@ module mach.int.UInt32
syntax converter of_int "%1U"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
end
......@@ -184,16 +185,16 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
syntax converter of_int "%1U"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
syntax val add_with_carry "add32_with_carry"
syntax val sub_with_borrow "sub32_with_borrow"
......@@ -201,23 +202,42 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
syntax val add3 "add32_3"
syntax val lsld "lsld32"
syntax val add_mod "%1 + %2"
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val add_mod "(%1) + (%2)"
syntax val sub_mod "(%1) - (%2)"
syntax val mul_mod "(%1) * (%2)"
syntax val div2by1
"(uint32_t)(((uint64_t)%1 | ((uint64_t)%2 << 32))/(uint64_t)%3)"
"(uint32_t)((((uint64_t)%1) | (((uint64_t)%2) << 32))/(uint64_t)(%3))"
syntax val lsl "%1 << %2"
syntax val lsr "%1 >> %2"
syntax val lsl "(%1) << (%2)"
syntax val lsr "(%1) >> (%2)"
syntax val is_msb_set "%1 & 0x80000000U"
syntax val is_msb_set "(%1) & 0x80000000U"
syntax val count_leading_zeros "__builtin_clz(%1)"
syntax val of_int32 "(uint32_t)%1"
syntax val of_int32 "(uint32_t)(%1)"
end
module mach.int.Int64
syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int64 "int64_t"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
end
module mach.int.UInt64Gen
......@@ -233,17 +253,17 @@ module mach.int.UInt64
syntax converter of_int "%1ULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (-_) "-(%1)"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
end
......@@ -434,16 +454,16 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
"
syntax converter of_int "%1ULL"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val (*) "%1 * %2"
syntax val (/) "%1 / %2"
syntax val (%) "%1 % %2"
syntax val (=) "%1 == %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val (+) "(%1) + (%2)"
syntax val (-) "(%1) - (%2)"
syntax val (*) "(%1) * (%2)"
syntax val (/) "(%1) / (%2)"
syntax val (%) "(%1) % (%2)"
syntax val (=) "(%1) == (%2)"
syntax val (<=) "(%1) <= (%2)"
syntax val (<) "(%1) < (%2)"
syntax val (>=) "(%1) >= (%2)"
syntax val (>) "(%1) > (%2)"
syntax val add_with_carry "add64_with_carry"
syntax val add_double "add64_double"
......@@ -458,20 +478,20 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
syntax val add3 "add64_3"
syntax val lsld "lsld64"
syntax val add_mod "%1 + %2"
syntax val sub_mod "%1 - %2"
syntax val mul_mod "%1 * %2"
syntax val add_mod "(%1) + (%2)"
syntax val sub_mod "(%1) - (%2)"
syntax val mul_mod "(%1) * (%2)"
syntax val lsl "%1 << %2"
syntax val lsr "%1 >> %2"
syntax val lsl "(%1) << (%2)"
syntax val lsr "(%1) >> (%2)"
syntax val is_msb_set "%1 & 0x8000000000000000ULL"
syntax val is_msb_set "(%1) & 0x8000000000000000ULL"
syntax val count_leading_zeros "__builtin_clzll(%1)"
syntax val of_int32 "(uint64_t)%1"
syntax val to_int64 "(int64_t)%1"
syntax val of_int64 "(uint64_t)%1"
syntax val of_int32 "(uint64_t)(%1)"
syntax val to_int64 "(int64_t)(%1)"
syntax val of_int64 "(uint64_t)(%1)"
end
......@@ -480,6 +500,8 @@ end
module mach.c.C
prelude "#include <assert.h>"
prelude "#define IGNORE2(x,y) do {} while (0)"
interface "#define IGNORE2(x,y) do {} while (0)"
syntax type ptr "%1 *"
syntax type bool "int" (* ? *)
......@@ -501,7 +523,9 @@ module mach.c.C
syntax val set_ofs "*(%1+(%2)) = %3"
syntax val incr_split "%1+(%2)"
syntax val join "(void)0"
syntax val decr_split "%1-(%2)"
syntax val join "IGNORE2"
syntax val join_r "IGNORE2"
syntax val c_assert "assert ( %1 )"
......
......@@ -380,9 +380,9 @@ module Sub
writes { x.data.elts }
=
let ghost ox = { x } in
let ghost b : ref limb = ref 1 in
let lx : ref limb = ref 0 in
let i : ref int32 = ref 0 in
let ghost b = ref (Limb.of_int 1) in
let lx = ref (Limb.of_int 0) in
let i = ref (Int32.of_int 0) in
while (Limb.(=) !lx 0) do
invariant { 0 <= !i <= sz }
invariant { !i = sz -> !lx <> 0 }
......
......@@ -1034,197 +1034,206 @@
</goal>
<goal name="VC wmpn_decr_1" expl="VC for wmpn_decr_1" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_decr_1.0" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<goal name="VC wmpn_decr_1.0" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_decr_1.1" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<goal name="VC wmpn_decr_1.1" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<goal name="VC wmpn_decr_1.2" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.4" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.5" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.06" steps="20"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.6" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.7" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="90"/></proof>
<goal name="VC wmpn_decr_1.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.8" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.01" steps="40"/></proof>
<goal name="VC wmpn_decr_1.8" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC wmpn_decr_1.9" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="29"/></proof>
<goal name="VC wmpn_decr_1.9" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.06" steps="18"/></proof>
</goal>
<goal name="VC wmpn_decr_1.10" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="111"/></proof>
</goal>
<goal name="VC wmpn_decr_1.11" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.01" steps="43"/></proof>
</goal>
<goal name="VC wmpn_decr_1.12" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC wmpn_decr_1.13" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.11" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.14" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.12" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="130"/></proof>
<goal name="VC wmpn_decr_1.15" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="151"/></proof>
</goal>
<goal name="VC wmpn_decr_1.13" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="54"/></proof>
<goal name="VC wmpn_decr_1.16" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="57"/></proof>
</goal>
<goal name="VC wmpn_decr_1.14" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.08" steps="114"/></proof>
<goal name="VC wmpn_decr_1.17" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.09" steps="134"/></proof>
</goal>
<goal name="VC wmpn_decr_1.15" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.18" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.16" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.19" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.17" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="54"/></proof>
<goal name="VC wmpn_decr_1.20" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="57"/></proof>
</goal>
<goal name="VC wmpn_decr_1.18" expl="integer overflow" proved="true">
<goal name="VC wmpn_decr_1.21" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19" expl="assertion" proved="true">
<goal name="VC wmpn_decr_1.22" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_decr_1.19.0" expl="assertion" proved="true">
<goal name="VC wmpn_decr_1.22.0" expl="assertion" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19.1" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.22.1" expl="VC for wmpn_decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19.2" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.22.2" expl="VC for wmpn_decr_1" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19.3" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.22.3" expl="VC for wmpn_decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19.4" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.22.4" expl="VC for wmpn_decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19.5" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.22.5" expl="VC for wmpn_decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_decr_1.20" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<goal name="VC wmpn_decr_1.23" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.21" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="122"/></proof>
<goal name="VC wmpn_decr_1.24" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="135"/></proof>
</goal>
<goal name="VC wmpn_decr_1.22" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.25" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.23" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.26" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.24" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.27" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.25" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="50"/></proof>
<goal name="VC wmpn_decr_1.28" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="53"/></proof>
</goal>
<goal name="VC wmpn_decr_1.26" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="66"/></proof>
<goal name="VC wmpn_decr_1.29" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="VC wmpn_decr_1.27" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="69"/></proof>
<goal name="VC wmpn_decr_1.30" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC wmpn_decr_1.28" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="52"/></proof>
<goal name="VC wmpn_decr_1.31" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="VC wmpn_decr_1.29" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.32" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.30" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.33" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.31" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="131"/></proof>
<goal name="VC wmpn_decr_1.34" expl="precondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="152"/></proof>
</goal>
<goal name="VC wmpn_decr_1.32" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="55"/></proof>
<goal name="VC wmpn_decr_1.35" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="VC wmpn_decr_1.33" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.09" steps="112"/></proof>
<goal name="VC wmpn_decr_1.36" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.08" steps="131"/></proof>
</goal>
<goal name="VC wmpn_decr_1.34" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.37" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.35" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.38" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.36" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="42"/></proof>
<goal name="VC wmpn_decr_1.39" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="45"/></proof>
</goal>
<goal name="VC wmpn_decr_1.37" expl="integer overflow" proved="true">
<goal name="VC wmpn_decr_1.40" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC wmpn_decr_1.38" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="47"/></proof>
<goal name="VC wmpn_decr_1.41" expl="assertion" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="50"/></proof>
</goal>
<goal name="VC wmpn_decr_1.39" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<goal name="VC wmpn_decr_1.42" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.40" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.08" steps="122"/></proof>
<goal name="VC wmpn_decr_1.43" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.08" steps="135"/></proof>
</goal>
<goal name="VC wmpn_decr_1.41" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.44" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.42" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.45" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.43" expl="loop invariant preservation" proved="true">
<goal name="VC wmpn_decr_1.46" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.44" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="50"/></proof>
<goal name="VC wmpn_decr_1.47" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="53"/></proof>
</goal>
<goal name="VC wmpn_decr_1.45" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="66"/></proof>
<goal name="VC wmpn_decr_1.48" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="VC wmpn_decr_1.46" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="69"/></proof>
<goal name="VC wmpn_decr_1.49" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC wmpn_decr_1.47" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.50" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.48" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.51" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.49" expl="assertion" proved="true">
<goal name="VC wmpn_decr_1.52" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_decr_1.49.0" expl="assertion" proved="true">
<goal name="VC wmpn_decr_1.52.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.49.1" expl="assertion" proved="true">
<goal name="VC wmpn_decr_1.52.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr_1.49.2" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.52.2" expl="VC for wmpn_decr_1" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC wmpn_decr_1.49.3" expl="VC for wmpn_decr_1" proved="true">
<goal name="VC wmpn_decr_1.52.3" expl="VC for wmpn_decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_decr_1.50" expl="precondition" proved="true">
<goal name="VC wmpn_decr_1.53" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.51" expl="postcondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="26"/></proof>
<goal name="VC wmpn_decr_1.54" expl="postcondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.03" steps="29"/></proof>
</goal>
<goal name="VC wmpn_decr_1.52" expl="postcondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.06" steps="40"/></proof>
<goal name="VC wmpn_decr_1.55" expl="postcondition" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.06" steps="43"/></proof>
</goal>
</transf>
</goal>
......
......@@ -857,9 +857,9 @@ with toom32_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
-> (pelts scratch)[j] = old (pelts scratch)[j] }
variant { k + k }
=
let n = 1 + (if 2 * sx >= 3 * sy
then Int32.(/) (sx - 1) 3
else Int32.(/) (sy - 1) 2) in
let n = 1 + (if 2 * sx >= 3 * sy
then Int32.(/) (sx - 1) 3
else Int32.(/) (sy - 1) 2) in
let s = sx - 2 * n in
let t = sy - n in
assert { 0 < s <= n };
......
......@@ -327,9 +327,12 @@ module C = struct
| Sexpr _ -> true
| _ -> false
let simplify_expr (d,s) : expr =
let rec simplify_expr (d,s) : expr =
match (d,s) with
| [], Sblock([],s) -> simplify_expr ([],s)
| [], Sexpr e -> e
| [], Sif(c,t,e) ->
Equestion (c, simplify_expr([],t), simplify_expr([],e))
| _ -> raise (Invalid_argument "simplify_expr")
let rec simplify_cond (cd, cs) =
......@@ -459,6 +462,9 @@ module Print = struct
| Ecast(ty, e) ->
fprintf fmt (protect_on paren "(%a)%a")
(print_ty ~paren:false) ty (print_expr ~paren:true) e
| Ecall (Esyntax (s, _, _, [], _), l) -> (* function defined in the prelude *)
fprintf fmt (protect_on paren "%s(%a)")
s (print_list comma (print_expr ~paren:false)) l
| Ecall (e,l) -> fprintf fmt (protect_on paren "%a(%a)")
(print_expr ~paren:true) e (print_list comma (print_expr ~paren:false)) l
| Econst c -> print_const fmt c
......@@ -754,6 +760,7 @@ module MLToC = struct
let e = C.(Econst (Cint (BigInt.to_string n))) in
([], return_or_expr env e)
| Eapp (rs, el) ->
Debug.dprintf debug_c_extraction "call to %s@." rs.rs_name.id_string;
if is_rs_tuple rs && env.computes_return_value
then begin
let args =
......@@ -1063,53 +1070,55 @@ module MLToC = struct
let translate_decl (info:info) (d:decl) : C.definition list
=
let translate_fun rs vl e =
Debug.dprintf debug_c_extraction "print %s@." rs.rs_name.id_string;
if rs_ghost rs
then begin Debug.dprintf debug_c_extraction "is ghost@."; [] end
else
let params =
List.map (fun (id, ty, _gh) -> (ty_of_mlty info ty, id))
(List.filter (fun (_,_, gh) -> not gh) vl) in
let params = List.filter (fun (ty, _) -> ty <> C.Tvoid) params in
let env = { computes_return_value = true;
in_unguarded_loop = false;
current_function = rs;
returns = Sid.empty;
breaks = Sid.empty; } in
let rity = rs.rs_cty.cty_result in
let is_simple_tuple ity =
let arity_zero = function
| Ityapp(_,a,r) -> a = [] && r = []
| Ityreg { reg_args = a; reg_regs = r } ->
a = [] && r = []
| Ityvar _ -> true
in
(match ity.ity_node with
| Ityapp ({its_ts = s},_,_)
| Ityreg { reg_its = {its_ts = s}; }
-> is_ts_tuple s
| _ -> false)
&& (ity_fold
(fun acc ity ->
acc && arity_zero ity.ity_node) true ity)
in
(* FIXME is it necessary to have arity 0 in regions ?*)
let rtype = ty_of_ty info (ty_of_ity rity) in
let rtype,sdecls =
if rtype=C.Tnosyntax && is_simple_tuple rity
then
let st = struct_of_rs info rs in
C.Tstruct st, [C.Dstruct st]
else rtype, [] in
let d,s = expr info env e in
(*TODO check if we want this flatten*)
let d,s = C.flatten_defs d s in
let d = C.group_defs_by_type d in
let s = C.elim_nop s in
let s = C.elim_empty_blocks s in
sdecls@[C.Dfun (rs.rs_name, (rtype,params), (d,s))] in
try
begin match d with
| Dlet (Lsym(rs, _, vl, e)) ->
if rs_ghost rs
then begin Debug.dprintf debug_c_extraction "is ghost@."; [] end
else
let params =
List.map (fun (id, ty, _gh) -> (ty_of_mlty info ty, id))
(List.filter (fun (_,_, gh) -> not gh) vl) in
let params = List.filter (fun (ty, _) -> ty <> C.Tvoid) params in
let env = { computes_return_value = true;
in_unguarded_loop = false;
current_function = rs;
returns = Sid.empty;
breaks = Sid.empty; } in
let rity = rs.rs_cty.cty_result in
let is_simple_tuple ity =
let arity_zero = function
| Ityapp(_,a,r) -> a = [] && r = []
| Ityreg { reg_args = a; reg_regs = r } ->
a = [] && r = []
| Ityvar _ -> true
in
(match ity.ity_node with
| Ityapp ({its_ts = s},_,_)
| Ityreg { reg_its = {its_ts = s}; }
-> is_ts_tuple s
| _ -> false)
&& (ity_fold
(fun acc ity ->
acc && arity_zero ity.ity_node) true ity)
in
(* FIXME is it necessary to have arity 0 in regions ?*)
let rtype = ty_of_ty info (ty_of_ity rity) in
let rtype,sdecls =
if rtype=C.Tnosyntax && is_simple_tuple rity
then
let st = struct_of_rs info rs in
C.Tstruct st, [C.Dstruct st]
else rtype, [] in
let d,s = expr info env e in
(*TODO check if we want this flatten*)
let d,s = C.flatten_defs d s in
let d = C.group_defs_by_type d in
let s = C.elim_nop s in
let s = C.elim_empty_blocks s in
sdecls@[C.Dfun (rs.rs_name, (rtype,params), (d,s))]
| Dlet (Lsym(rs, _, vl, e)) -> translate_fun rs vl e
| Dtype [{its_name=id; its_def=idef}] ->
Debug.dprintf debug_c_extraction "PDtype %s@." id.id_string;
begin
......@@ -1125,7 +1134,15 @@ module MLToC = struct
^id.id_string))
end
end
| Dlet (Lrec rl) ->
let translate_rdef rd =
translate_fun rd.rec_sym rd.rec_args rd.rec_exp in
let defs = List.flatten (List.map translate_rdef rl) in