Commit 2d6e7027 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Remove most unused variables from extracted C

parent 356ab202
......@@ -221,8 +221,8 @@ struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
uint64_t q,r;
udiv_qrnnd(q,r,uh,ul,d);
uint64_t q,_dummy;
udiv_qrnnd(q,_dummy,uh,ul,d);
return q;
}
......
......@@ -1442,7 +1442,6 @@ module N
writes { x.data.elts }
=
let ghost ox = { x } in
let r : ref limb = ref 0 in
let ghost b : ref limb = ref 1 in
let lx : ref limb = ref 0 in
let i : ref int32 = ref 0 in
......@@ -1462,7 +1461,6 @@ module N
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let res = sub_mod !lx 1 in
r := res;
ghost (if Limb.(=) !lx 0 then b := 1 else b := 0);
assert { res - radix * !b = !lx - 1 };
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
......@@ -2528,7 +2526,7 @@ module N
assert { 1 <= k <= d };
let l,h = mul_double v uh in
let sl,c = add_with_carry l ul zero in
let sh,c' = add_with_carry uh h c in (* <c',sh,sl> = <uh, ul> + <h,l> *)
let (sh,ghost c') = add_with_carry uh h c in (* <c',sh,sl> = <uh, ul> + <h,l> *)
assert { sl + radix * sh + radix * radix * c'
= l + radix * h + ul + radix * uh };
assert { c' = 0
......@@ -3041,7 +3039,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
let r1 = ref zero in
let l,h = mul_double v uh in
let sl, c = add_with_carry um l zero in
let sh, c' = add_with_carry uh h c in
let sh, ghost c' = add_with_carry uh h c in
assert { sl + radix * sh + radix * radix * c'
= um + radix * uh + v * uh };
assert { c' = 0
......@@ -3072,11 +3070,11 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
by !r1 = mod (um - dh * sh) radix };*)
let tl, th = mul_double sh dl in
let il, b = sub_with_borrow ul tl zero in
let (ih, b') = sub_with_borrow !r1 th b in
let (ih, ghost b') = sub_with_borrow !r1 th b in
assert { il + radix * ih - radix * radix * b'
= ul + radix * !r1 - sh * dl };
let bl,b2 = sub_with_borrow il dl zero in
let bh, b2' = sub_with_borrow ih dh b2 in
let bh, ghost b2' = sub_with_borrow ih dh b2 in
assert { bl + radix * bh - radix * radix * b2'
= il + radix * ih - dl - radix * dh };
mod_mult (radix * radix) (l2i b')
......@@ -3448,7 +3446,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
so !q1 = mod (cq - 1) radix = cq - 1
};
let rl, c = add_with_carry !r0 dl zero in
let rh, c' = add_with_carry !r1 dh c in
let rh, ghost c' = add_with_carry !r1 dh c in
assert { rl + radix * rh = mod (r' + d) (radix * radix)
by radix * radix * c' + rl + radix * rh
= r' + d
......@@ -3505,7 +3503,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
if [@ex:unlikely] (Limb.(>) !r1 dh) || (Limb.(=) !r1 dh && Limb.(>=) !r0 dl)
then begin
let bl, b = sub_with_borrow !r0 dl zero in
let bh, b'= sub_with_borrow !r1 dh b in
let bh, ghost b'= sub_with_borrow !r1 dh b in
assert { b' = 0 };
assert { bl + radix * bh = !r0 + radix * !r1 - d };
assert { !q1 < radix - 1
......@@ -3871,7 +3869,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
if (not (Limb.(=) qh limb_zero))
then begin
assert { qh = 1 };
let b = sub_in_place xd y sy sy in
let ghost b = sub_in_place xd y sy sy in
begin
ensures { value (x at PreAdjust) sx =
(value !qp (sx - sy - !i)
......@@ -4136,7 +4134,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
label SubMax in
let ghost xc = Array.copy (x.data) in
value_sub_frame (pelts x) xc.elts x.offset (x.offset + p2i !i);
let b = submul_limb xd y !ql sy in
let ghost b = submul_limb xd y !ql sy in
begin
ensures { value x !i
= value (x at SubMax) !i }
......@@ -5965,7 +5963,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
ensures { !rl + radix * !rh < dl + radix * dh }
ensures { !qh = 1 }
let (r0, b) = sub_with_borrow !rl dl uzero in
let (r1, b') = sub_with_borrow !rh dh b in
let (r1, ghost b') = sub_with_borrow !rh dh b in
assert { b' = 0 };
assert { r0 + radix * r1 = !rl + radix * !rh - (dl + radix * dh) };
value_sub_tail (pelts x) x.offset (x.offset + p2i sx - 1);
......
......@@ -3008,62 +3008,43 @@
<proof prover="9" timelimit="1"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
<goal name="VC decr_1.9" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="30"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="VC decr_1.10" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC decr_1.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.12" expl="precondition" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="122"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="121"/></proof>
</goal>
<goal name="VC decr_1.13" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="49"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="VC decr_1.14" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.09" steps="109"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.08" steps="108"/></proof>
</goal>
<goal name="VC decr_1.15" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.17" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="49"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="VC decr_1.18" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC decr_1.19" expl="assertion" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC decr_1.19.0" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="VC decr_1.19.1" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.19.2" expl="VC for decr_1" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC decr_1.19.3" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.19.4" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.19.5" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
<proof prover="9" timelimit="1"><result status="valid" time="0.59" steps="263"/></proof>
</goal>
<goal name="VC decr_1.20" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC decr_1.21" expl="loop invariant preservation" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.08" steps="117"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.08" steps="116"/></proof>
</goal>
<goal name="VC decr_1.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -3075,52 +3056,71 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.25" expl="loop invariant preservation" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="51"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="50"/></proof>
</goal>
<goal name="VC decr_1.26" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="61"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="60"/></proof>
</goal>
<goal name="VC decr_1.27" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="64"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="63"/></proof>
</goal>
<goal name="VC decr_1.28" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="47"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="VC decr_1.29" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC decr_1.30" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.31" expl="precondition" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="123"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="122"/></proof>
</goal>
<goal name="VC decr_1.32" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="50"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
<goal name="VC decr_1.33" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.08" steps="107"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.09" steps="106"/></proof>
</goal>
<goal name="VC decr_1.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.35" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.36" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="43"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="42"/></proof>
</goal>
<goal name="VC decr_1.37" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC decr_1.38" expl="assertion" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="48"/></proof>
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC decr_1.38.0" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="VC decr_1.38.1" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC decr_1.38.2" expl="VC for decr_1" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC decr_1.38.3" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.38.4" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.38.5" expl="VC for decr_1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC decr_1.39" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC decr_1.40" expl="loop invariant preservation" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="117"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="116"/></proof>
</goal>
<goal name="VC decr_1.41" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -3132,13 +3132,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC decr_1.44" expl="loop invariant preservation" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="51"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.03" steps="50"/></proof>
</goal>
<goal name="VC decr_1.45" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.02" steps="61"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.06" steps="60"/></proof>
</goal>
<goal name="VC decr_1.46" expl="VC for decr_1" proved="true">
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="64"/></proof>
<proof prover="9" timelimit="1"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="VC decr_1.47" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -58,8 +58,10 @@ void init_valid (mp_ptr ap, mp_ptr bp, mp_size_t an, mp_size_t bn) {
int main () {
mp_ptr ap, bp, rp, refp, rq, rr, refq, refr;
mp_size_t max_n, an, bn, rn;
#ifdef BENCH
struct timeval begin, end;
double elapsed;
#endif
uint64_t c, refc;
//gmp_randstate_t rands;
//TMP_DECL;
......
......@@ -907,7 +907,7 @@ module MLToC = struct
| Efor _ -> raise (Unsupported "for loops") (*TODO*)
| Ematch (({e_node = Eapp(rs,_)} as e1), [Ptuple rets,e2], [])
when List.for_all
(function Pvar _ -> true |_-> false)
(function | Pwild (*ghost*) | Pvar _ -> true |_-> false)
rets
->
let id_struct = id_register (id_fresh "struct_res") in
......@@ -920,6 +920,7 @@ module MLToC = struct
match p with
| Pvar vs -> C.Ddecl(ty_of_ty info vs.vs_ty,
[vs.vs_name, C.Enothing])::acc
| Pwild -> acc
| _ -> assert false )
rets [d_struct] in
let d,s = expr info {env with computes_return_value = false} e1 in
......@@ -930,6 +931,7 @@ module MLToC = struct
match rets with
| [] -> C.Snop
| Pvar vs :: t -> C.Sseq ((assign vs.vs_name i), (assigns t (i+1)))
| Pwild :: t -> assigns t (i+1) (* ghost variable, skip *)
| _ -> assert false in
let assigns = assigns rets 0 in
let b = expr info env e2 in
......
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