Commit 9011a613 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Extraction of open/close

parent 9dbc63b2
......@@ -453,8 +453,14 @@ end
module mach.c.C
prelude "#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
interface "#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
prelude
"#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
prelude
"#define IGNORE3(x,y,z) do { (void(x); (void)(y); (void)(z); } while (0)"
interface
"#define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)"
interface
"#define IGNORE3(x,y,z) do { (void(x); (void)(y); (void)(z); } while (0)"
syntax type ptr "%1 *"
syntax type bool "int" (* ? *)
......@@ -501,4 +507,4 @@ module mach.fxp.Fxp
syntax val fxp_asr "(uint64_t)((int64_t)%1 >> %2)" prec 2 1 2
syntax val fxp_asr' "(uint64_t)((int64_t)%1 >> %2)" prec 2 1 2
end
end
\ No newline at end of file
......@@ -21,7 +21,7 @@ module AddAlias
val open_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, m:mem)
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid r sx /\ valid x sx /\ valid y sy }
requires { 0 <= sy <= sx }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
......@@ -41,13 +41,13 @@ module AddAlias
/\ plength y = old plength y }
ensures { min r = old min r /\ min x = old min x /\ min y = old min y }
ensures { data nr = data nx = data ny }
writes { r.max, x.max, y.max, r, x, y }
writes { r, x, y }
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_sep (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (m:mem) : unit
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -77,7 +77,7 @@ module AddAlias
r.data, r.max, x.data, x.max, y.data, y.max, m.ok }
val open_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, m:mem)
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid x sx /\ valid y sy }
requires { 0 <= sy <= sx }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
......@@ -94,13 +94,13 @@ module AddAlias
ensures { plength x = old plength x /\ plength y = old plength y }
ensures { min x = old min x /\ min y = old min y }
ensures { data nr = data nx = data ny }
writes { x.max, y.max, x, y }
writes { x, y }
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val open_ry (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, m:mem)
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid x sx /\ valid y sx }
requires { 0 <= sy <= sx }
ensures { value nx sx = old value x sx /\ value ny sy = old value y sy }
......@@ -117,13 +117,13 @@ module AddAlias
ensures { plength x = old plength x /\ plength y = old plength y }
ensures { min x = old min x /\ min y = old min y }
ensures { data nr = data nx = data ny }
writes { x.max, y.max, x, y }
writes { x, y }
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val open_rxy (x:ptr limb) (sx:int32) :
(nr:ptr limb, nx:ptr limb, ny:ptr limb, m:mem)
(nr:ptr limb, nx:ptr limb, ny:ptr limb, ghost m:mem)
requires { valid x sx }
requires { 0 <= sx }
ensures { value nx sx = old value x sx }
......@@ -139,13 +139,13 @@ module AddAlias
ensures { pelts x = old pelts x }
ensures { plength x = old plength x }
ensures { min x = old min x }
writes { x.max, x }
writes { x }
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
val close_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (m:mem) : unit
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -170,7 +170,7 @@ module AddAlias
x.data, x.max, y.data, y.max, m.ok }
val close_ry (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
(nr nx ny:ptr limb) (m:mem) : unit
(nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -194,7 +194,7 @@ module AddAlias
writes { nr, nx, ny, nr.data, nx.data, ny.data,
x.data, x.max, y.data, y.max, m.ok }
val close_rxy (x:ptr limb) (sx:int32) (nr nx ny:ptr limb) (m:mem) : unit
val close_rxy (x:ptr limb) (sx:int32) (nr nx ny:ptr limb) (ghost m:mem) : unit
alias { nr.data with nx.data }
alias { nr.data with ny.data }
alias { nx.data with ny.data }
......@@ -409,7 +409,7 @@ module AddAlias
done;
c
let add_n (r x y:ptr limb) (sz:int32) : limb
let add_n [@extraction:inline] (r x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid r sz /\ valid x sz /\ valid y sz }
ensures { value r sz + power radix sz * result
......@@ -444,7 +444,7 @@ module AddAlias
= (pelts oy)[offset y + j] };
res
let add_n_rx (x y:ptr limb) (sz:int32) : limb
let add_n_rx [@extraction:inline] (x y:ptr limb) (sz:int32) : limb
requires { 0 <= sz }
requires { valid x sz /\ valid y sz }
ensures { value x sz + power radix sz * result
......@@ -468,7 +468,8 @@ module AddAlias
= (pelts oy)[offset y + j] };
res
let add (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
let add [@extraction:inline] (r x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32)
: limb
requires { 0 <= sy <= sx }
requires { valid r sx /\ valid x sx /\ valid y sy }
ensures { value r sx + power radix sx * result
......@@ -503,7 +504,8 @@ module AddAlias
= (pelts oy)[offset y + j] };
res
let add_rx (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
let add_rx [@extraction:inline] (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sy }
ensures { value x sx + power radix sx * result
......@@ -528,7 +530,8 @@ module AddAlias
= (pelts oy)[offset y + j] };
res
let add_ry (x:ptr limb) (sx:int32) (y:ptr limb) (sy:int32) : limb
let add_ry [@extraction:inline] (x:ptr limb) (sx:int32)
(y:ptr limb) (sy:int32) : limb
requires { 0 <= sy <= sx }
requires { valid x sx /\ valid y sx }
ensures { value y sx + power radix sx * result
......@@ -553,7 +556,7 @@ module AddAlias
= (pelts ox)[offset x + j] };
res
let add_n_rxy (x:ptr limb) (sx:int32) : limb
let add_n_rxy [@extraction:inline] (x:ptr limb) (sx:int32) : limb
requires { 0 <= sx }
requires { valid x sx }
ensures { value x sx + power radix sx * result
......
......@@ -89,3 +89,122 @@ static uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
syntax val div2by1 "div64_2by1"
end
module add_alias.AddAlias
prelude "
struct __open_sep_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rx_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_ry_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rxy_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = r;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = y;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx)
{
struct __open_sep_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = x;
return result;
}
"
interface "
struct __open_sep_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rx_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_ry_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rxy_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx);
"
syntax val open_sep "open_sep"
syntax val open_rx "open_rx"
syntax val open_ry "open_ry"
syntax val open_rxy "open_rxy"
syntax val close_sep "IGNORE3(%1,%2,%4)"
syntax val close_rx "IGNORE3(%1,%2,%4)"
syntax val close_ry "IGNORE3(%1,%2,%4)"
syntax val close_rxy "IGNORE3(%1,%2,%4)"
end
\ No newline at end of file
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