Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
356ab202
Commit
356ab202
authored
Mar 29, 2018
by
Raphael Rieu-Helft
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Use structs to extract functions that return multiple values
parent
f7b732b8
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
295 additions
and
212 deletions
+295
-212
drivers/c.drv
drivers/c.drv
+102
-53
src/mlw/cprinter.ml
src/mlw/cprinter.ml
+193
-159
No files found.
drivers/c.drv
View file @
356ab202
...
...
@@ -50,39 +50,74 @@ module mach.int.UInt32
"
#define LOW_MASK 0x00000000FFFFFFFFULL
void add32_with_carry(uint32_t * res, uint32_t * carry, uint32_t x, uint32_t y, uint32_t c)
struct __add32_with_carry_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __add32_with_carry_result add32_with_carry(uint32_t x, uint32_t y, uint32_t c)
{
struct __add32_with_carry_result result;
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) c;
*res = (uint32_t)(r & LOW_MASK);
*carry = (uint32_t)(r >> 32);
result.__field_0 = (uint32_t)(r & LOW_MASK);
result.__field_1 = (uint32_t)(r >> 32);
return result;
}
void sub32_with_borrow(uint32_t * res, uint32_t * borrow, uint32_t x, uint32_t y, uint32_t b)
struct __sub32_with_borrow_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __sub32_with_borrow_result sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b)
{
struct __sub32_with_borrow_result result;
uint64_t r = (uint64_t)x - (uint64_t)y - (uint64_t) b;
*res = (uint32_t)(r & LOW_MASK);
*borrow = (uint32_t)(r >> 63);
result.__field_0 = (uint32_t)(r & LOW_MASK);
result.__field_1 = (uint32_t)(r >> 63);
return result;
}
void mul32_double(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y)
struct __mul32_double_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __mul32_double_result mul32_double(uint32_t x, uint32_t y)
{
struct __mul32_double_result result;
uint64_t r = (uint64_t)x * (uint64_t)y;
*low = (uint32_t)(r & LOW_MASK);
*high = (uint32_t)(r >> 32);
result.__field_0 = (uint32_t)(r & LOW_MASK);
result.__field_1 = (uint32_t)(r >> 32);
return result;
}
void add32_3(uint32_t * low, uint32_t * high, uint32_t x, uint32_t y, uint32_t z)
struct __add32_3_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z)
{
struct __add32_3_result result;
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) z;
*low = (uint32_t)(r & LOW_MASK);
*high = (uint32_t)(r >> 32);
result.__field_0 = (uint32_t)(r & LOW_MASK);
result.__field_1 = (uint32_t)(r >> 32);
return result;
}
void lsld32(uint32_t * low, uint32_t * high, uint32_t x, uint32_t cnt)
struct __lsld32_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
{
struct __lsld32_result result;
uint64_t r = (uint64_t)x << cnt;
*low = (uint32_t)(r & LOW_MASK);
*high = (uint32_t)(r >> 32);
result.__field_0 = (uint32_t)(r & LOW_MASK);
result.__field_1 = (uint32_t)(r >> 32);
return result;
}
"
...
...
@@ -141,28 +176,47 @@ module mach.int.UInt64
#undef invert_limb
void add64_with_carry(uint64_t * res, uint64_t * carry, uint64_t x, uint64_t y, uint64_t c)
struct __add64_with_carry_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_with_carry_result add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
{
struct __add64_with_carry_result result;
uint64_t r = x + y + c;
*res = r;
if (r == x) *carry = c;
else *carry = (r < x);
//if (r < x) *carry = 1;
//else *carry = 0;
result.__field_0 = r;
if (r == x) result.__field_1 = c;
else result.__field_1 = (r < x);
return result;
}
void sub64_with_borrow(uint64_t * res, uint64_t * borrow, uint64_t x, uint64_t y, uint64_t b)
struct __sub64_with_borrow_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __sub64_with_borrow_result sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
{
struct __sub64_with_borrow_result result;
uint64_t r = x - y - b;
*res = r;
if (r > x) *borrow = 1;
else if (r == x) *borrow = b;
else *borrow = 0;
result.__field_0 = r;
if (r > x) result.__field_1 = 1;
else if (r == x) result.__field_1 = b;
else result.__field_1 = 0;
return result;
}
void mul64_double(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y)
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
umul_ppmm(*high,*low,x,y);
struct __mul64_double_result result;
umul_ppmm(result.__field_1,result.__field_0,x,y);
return result;
}
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
...
...
@@ -172,42 +226,37 @@ uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
return q;
}
void add64_3(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y, uint64_t z)
struct __add64_3_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
{
struct __add64_3_result result;
uint64_t r, c1, c2;
r = x + y;
c1 = r < y;
r += z;
c2 = r < z;
//add64_with_carry(&r, &c1, x, y, 0);
//add64_with_carry(&r, &c2, r, z, 0);
*high = c1 + c2;
*low = r;
result.__field_1 = c1 + c2;
result.__field_0 = r;
return result;
}
void lsld64(uint64_t * low, uint64_t * high, uint64_t x, uint64_t cnt)
{
*high = x >> (64 - cnt);
*low = x << cnt;
}
"
(*
void mul64_double(uint64_t * low, uint64_t * high, uint64_t x, uint64_t y)
{
uint64_t h, l;
asm(\"mulq %3\" : \"=a\"(l),\"=d\"(h) : \"a\"(x), \"rm\"(y));
*high = h;
*low = l;
}
struct __lsld64_result
{ uint64_t __field_0;
uint64_t __field_1;
};
uint64_t div64_2by1
(uint64_t
ul
, uint64_t
uh, uint64_t d
)
struct __lsld64_result lsld64
(uint64_t
x
, uint64_t
cnt
)
{
uint64_t q,r;
asm(\"divq %4\" : \"=a\"(q),\"=d\"(r) : \"a\"(ul), \"d\"(uh), \"rm\"(d));
return q;
struct __lsld64_result result;
result.__field_1 = x >> (64 - cnt);
result.__field_0 = x << cnt;
return result;
}
*)
"
syntax converter of_int "%1ULL"
...
...
src/mlw/cprinter.ml
View file @
356ab202
...
...
@@ -15,12 +15,14 @@ exception Unsupported of string
module
C
=
struct
type
ty
=
type
struct_def
=
string
*
(
string
*
ty
)
list
and
ty
=
|
Tvoid
|
Tsyntax
of
string
*
ty
list
|
Tptr
of
ty
|
Tarray
of
ty
*
expr
|
Tstruct
of
ident
*
(
ident
*
ty
)
list
|
Tstruct
of
struct_def
|
Tunion
of
ident
*
(
ident
*
ty
)
list
|
Tnamed
of
ident
(* alias from typedef *)
|
Tnosyntax
(* types that do not have a syntax, can't be printed *)
...
...
@@ -53,8 +55,8 @@ module C = struct
|
Esize_expr
of
expr
|
Esize_type
of
ty
|
Eindex
of
expr
*
expr
(* Array access *)
|
Edot
of
expr
*
ident
(* Field access with dot *)
|
Earrow
of
expr
*
ident
(* Pointer access with arrow *)
|
Edot
of
expr
*
string
(* Field access with dot *)
|
Earrow
of
expr
*
string
(* Pointer access with arrow *)
|
Esyntax
of
string
*
ty
*
(
ty
array
)
*
(
expr
*
ty
)
list
*
bool
(* template, type and type arguments of result, typed arguments,
is/is not converter*)
...
...
@@ -81,6 +83,7 @@ module C = struct
|
Dinclude
of
ident
|
Dproto
of
ident
*
proto
|
Ddecl
of
names
|
Dstruct
of
struct_def
|
Dtypedef
of
ty
*
ident
and
body
=
definition
list
*
stmt
...
...
@@ -203,6 +206,7 @@ module C = struct
let
l
,
b
=
aux
l
in
Ddecl
(
ty
,
l
)
,
b
|
Dinclude
i
->
Dinclude
i
,
true
|
Dstruct
_
->
raise
(
Unsupported
"struct declaration inside function"
)
|
Dfun
_
->
raise
(
Unsupported
"nested function"
)
|
Dtypedef
_
->
raise
(
Unsupported
"typedef inside function"
)
|
Dproto
_
->
raise
(
Unsupported
"prototype inside function"
)
...
...
@@ -403,7 +407,7 @@ module Print = struct
|
Tarray
(
ty
,
expr
)
->
fprintf
fmt
(
protect_on
paren
"%a[%a]"
)
(
print_ty
~
paren
:
true
)
ty
(
print_expr
~
paren
:
false
)
expr
|
Tstruct
_
->
raise
(
Unprinted
"struct
s"
)
|
Tstruct
(
s
,_
)
->
fprintf
fmt
"struct
%s"
s
|
Tunion
_
->
raise
(
Unprinted
"unions"
)
|
Tnamed
id
->
print_ident
fmt
id
|
Tnosyntax
->
raise
(
Unprinted
"type without syntax"
)
...
...
@@ -446,8 +450,9 @@ module Print = struct
|
Esize_expr
e
->
fprintf
fmt
(
protect_on
paren
"sizeof(%a)"
)
(
print_expr
~
paren
:
false
)
e
|
Esize_type
ty
->
fprintf
fmt
(
protect_on
paren
"sizeof(%a)"
)
(
print_ty
~
paren
:
false
)
ty
|
Eindex
_
|
Edot
_
|
Earrow
_
->
raise
(
Unprinted
"struct/array access"
)
fprintf
fmt
(
protect_on
paren
"sizeof(%a)"
)
(
print_ty
~
paren
:
false
)
ty
|
Edot
(
e
,
s
)
->
fprintf
fmt
"%a.%s"
(
print_expr
~
paren
:
true
)
e
s
|
Eindex
_
|
Earrow
_
->
raise
(
Unprinted
"struct/array access"
)
|
Esyntax
(
s
,
t
,
args
,
lte
,_
)
->
gen_syntax_arguments_typed
snd
(
fun
_
->
args
)
(
if
paren
then
(
"("
^
s
^
")"
)
else
s
)
...
...
@@ -513,11 +518,18 @@ module Print = struct
fprintf
fmt
"%a @[<hov>%a@];"
(
print_ty
~
paren
:
false
)
ty
(
print_list
comma
(
print_id_init
~
stars
:
nb
))
lie
|
Dstruct
(
s
,
lf
)
->
fprintf
fmt
"struct %s@ @[<hov>{@;<1 2>@[<hov>%a@]@
\n
};@
\n
@]"
s
(
print_list
newline
(
fun
fmt
(
s
,
ty
)
->
fprintf
fmt
"%a %s;"
(
print_ty
~
paren
:
false
)
ty
s
))
lf
|
Dinclude
id
->
fprintf
fmt
"#include<%a.h>@;"
print_ident
id
|
Dtypedef
(
ty
,
id
)
->
fprintf
fmt
"@[<hov>typedef@ %a@;%a;@]"
(
print_ty
~
paren
:
false
)
ty
print_ident
id
(
print_ty
~
paren
:
false
)
ty
print_ident
id
with
Unprinted
s
->
Format
.
printf
"Missed a def because : %s@."
s
and
print_body
fmt
(
def
,
s
)
=
...
...
@@ -561,7 +573,7 @@ module MLToC = struct
|
Some
s
->
C
.
Tsyntax
(
s
,
List
.
map
(
ty_of_mlty
info
)
tl
)
|
None
->
C
.
Tnosyntax
end
|
Ttuple
_
->
raise
(
Unsupported
"t
ype tuple
"
)
|
Ttuple
_
->
raise
(
Unsupported
"t
uple parameters
"
)
let
rec
ty_of_ty
info
ty
=
(*FIXME try to use only ML tys*)
match
ty
.
ty_node
with
...
...
@@ -586,8 +598,8 @@ module MLToC = struct
type
syntax_env
=
{
in_unguarded_loop
:
bool
;
computes_return_value
:
bool
;
returns_tuple
:
bool
*
ident
list
;
breaks
:
Sid
.
t
;
current_function
:
rsymbol
;
breaks
:
Sid
.
t
;
returns
:
Sid
.
t
;
}
...
...
@@ -624,6 +636,27 @@ module MLToC = struct
|
Eunlikely
e
->
Elikely
e
|
e
->
e
let
field
i
=
"__field_"
^
(
string_of_int
i
)
let
struct_of_rs
info
rs
=
let
rty
=
ty_of_ity
rs
.
rs_cty
.
cty_result
in
match
rty
.
ty_node
with
|
Tyapp
(
ts
,
lt
)
->
assert
(
is_ts_tuple
ts
);
let
rec
fields
fr
tys
=
match
tys
with
|
[]
->
[]
|
ty
::
l
->
(
field
fr
,
ty_of_ty
info
ty
)
::
(
fields
(
fr
+
1
)
l
)
in
let
fields
=
fields
0
lt
in
let
s
=
match
query_syntax
info
.
syntax
rs
.
rs_name
with
|
Some
s
->
s
|
None
->
rs
.
rs_name
.
id_string
in
let
name
=
Pp
.
sprintf
"__%s_result"
s
in
(
name
,
fields
)
|
_
->
assert
false
let
struct_of_rs
info
=
Wrs
.
memoize
17
(
fun
rs
->
struct_of_rs
info
rs
)
let
rec
expr
info
env
(
e
:
Mltree
.
expr
)
:
C
.
body
=
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_node
with
...
...
@@ -657,108 +690,110 @@ module MLToC = struct
([]
,
return_or_expr
env
e
)
|
Eapp
(
rs
,
el
)
->
if
is_rs_tuple
rs
&&
env
.
computes_return_value
then
begin
match
env
.
returns_tuple
with
|
true
,
rl
->
let
args
=
List
.
filter
(
fun
e
->
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_ity
with
|
I
i
when
ity_equal
i
Ity
.
ity_unit
->
false
|
_
->
true
)
el
in
assert
(
List
.
length
rl
=
List
.
length
args
);
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
C
.(
[]
,
List
.
fold_right2
(
fun
res
arg
acc
->
let
d
,
s
=
expr
info
env_f
arg
in
let
s
=
assignify
(
Eunop
(
Ustar
,
Evar
(
res
)))
s
in
Sseq
(
Sblock
(
d
,
s
)
,
acc
))
rl
args
(
Sreturn
(
Enothing
)))
|
_
->
assert
false
end
then
begin
let
args
=
List
.
filter
(
fun
e
->
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_ity
with
|
I
i
when
ity_equal
i
Ity
.
ity_unit
->
false
|
_
->
true
)
el
in
(*FIXME still needed with masks? *)
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
let
id_struct
=
id_register
(
id_fresh
"result"
)
in
let
e_struct
=
C
.
Evar
id_struct
in
let
d_struct
=
C
.(
Ddecl
(
Tstruct
(
struct_of_rs
info
env
.
current_function
)
,
[
id_struct
,
Enothing
]))
in
let
assign
i
(
d
,
s
)
=
C
.
Sblock
(
d
,
assignify
C
.(
Edot
(
e_struct
,
field
i
))
s
)
in
let
rec
assigns
args
i
=
match
args
with
|
[]
->
Snop
|
e
::
t
->
let
b
=
expr
info
env_f
e
in
C
.
Sseq
(
assign
i
b
,
assigns
t
(
i
+
1
))
in
C
.([
d_struct
]
,
Sseq
(
assigns
args
0
,
Sreturn
(
e_struct
)))
end
else
let
e'
=
match
(
query_syntax
info
.
syntax
rs
.
rs_name
,
query_syntax
info
.
converter
rs
.
rs_name
)
with
|
_
,
Some
s
|
Some
s
,
_
->
begin
try
let
_
=
Str
.
search_forward
(
Str
.
regexp
"[%]
\\
([tv]?
\\
)[0-9]+"
)
s
0
in
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
let
params
=
List
.
map
(
fun
e
->
(
simplify_expr
(
expr
info
env_f
e
)
,
ty_of_ty
info
(
ty_of_ity
(
ity_of_expr
e
))))
el
in
let
rty
=
ty_of_ity
(
match
e
.
e_ity
with
|
C
_
->
assert
false
|
I
i
->
i
)
in
let
rtyargs
=
match
rty
.
ty_node
with
|
Tyvar
_
->
[
||
]
|
Tyapp
(
_
,
args
)
->
Array
.
of_list
(
List
.
map
(
ty_of_ty
info
)
args
)
in
C
.
Esyntax
(
s
,
ty_of_ty
info
rty
,
rtyargs
,
params
,
Mid
.
mem
rs
.
rs_name
info
.
converter
)
with
Not_found
->
let
args
=
List
.
filter
(
fun
e
->
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_ity
with
|
I
i
when
ity_equal
i
Ity
.
ity_unit
->
false
|
_
->
true
)
el
in
if
args
=
[]
then
C
.(
Esyntax
(
s
,
Tnosyntax
,
[
||
]
,
[]
,
true
))
(*constant*)
else
(*function defined in the prelude *)
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
C
.(
Ecall
(
Esyntax
(
s
,
Tnosyntax
,
[
||
]
,
[]
,
true
)
,
List
.
map
(
fun
e
->
simplify_expr
(
expr
info
env_f
e
))
el
))
end
|
_
->
let
args
=
let
e'
=
match
(
query_syntax
info
.
syntax
rs
.
rs_name
,
query_syntax
info
.
converter
rs
.
rs_name
)
with
|
_
,
Some
s
|
Some
s
,
_
->
begin
try
let
_
=
Str
.
search_forward
(
Str
.
regexp
"[%]
\\
([tv]?
\\
)[0-9]+"
)
s
0
in
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
let
params
=
List
.
map
(
fun
e
->
(
simplify_expr
(
expr
info
env_f
e
)
,
ty_of_ty
info
(
ty_of_ity
(
ity_of_expr
e
))))
el
in
let
rty
=
ty_of_ity
(
match
e
.
e_ity
with
|
C
_
->
assert
false
|
I
i
->
i
)
in
let
rtyargs
=
match
rty
.
ty_node
with
|
Tyvar
_
->
[
||
]
|
Tyapp
(
_
,
args
)
->
Array
.
of_list
(
List
.
map
(
ty_of_ty
info
)
args
)
in
C
.
Esyntax
(
s
,
ty_of_ty
info
rty
,
rtyargs
,
params
,
Mid
.
mem
rs
.
rs_name
info
.
converter
)
with
Not_found
->
let
args
=
List
.
filter
(
fun
e
->
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_ity
with
|
I
i
when
ity_equal
i
Ity
.
ity_unit
->
false
|
_
->
true
)
el
in
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
C
.(
Ecall
(
Evar
(
rs
.
rs_name
)
,
List
.
map
(
fun
e
->
simplify_expr
(
expr
info
env_f
e
))
args
))
el
in
if
args
=
[]
then
C
.(
Esyntax
(
s
,
Tnosyntax
,
[
||
]
,
[]
,
true
))
(*constant*)
else
(*function defined in the prelude *)
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
C
.(
Ecall
(
Esyntax
(
s
,
Tnosyntax
,
[
||
]
,
[]
,
true
)
,
List
.
map
(
fun
e
->
simplify_expr
(
expr
info
env_f
e
))
el
))
end
|
_
->
let
args
=
List
.
filter
(
fun
e
->
assert
(
not
e
.
e_effect
.
eff_ghost
);
match
e
.
e_ity
with
|
I
i
when
ity_equal
i
Ity
.
ity_unit
->
false
|
_
->
true
)
el
in
let
env_f
=
{
env
with
computes_return_value
=
false
}
in
C
.(
Ecall
(
Evar
(
rs
.
rs_name
)
,
List
.
map
(
fun
e
->
simplify_expr
(
expr
info
env_f
e
))
args
))
in
C
.(
[]
,
if
env
.
computes_return_value
then
begin
match
e
.
e_ity
with
|
I
ity
when
ity_equal
ity
Ity
.
ity_unit
->
Sseq
(
Sexpr
e'
,
Sreturn
Enothing
)
|
I
_
->
Sreturn
e'
|
_
->
assert
false
end
else
Sexpr
e'
)
C
.(
[]
,
if
env
.
computes_return_value
then
begin
match
e
.
e_ity
with
|
I
ity
when
ity_equal
ity
Ity
.
ity_unit
->
Sseq
(
Sexpr
e'
,
Sreturn
Enothing
)
|
I
_
->
Sreturn
e'
|
_
->
assert
false
end
else
Sexpr
e'
)
|
Elet
(
ld
,
e
)
->
begin
match
ld
with
|
Lvar
(
pv
,
le
)
->
(* not a block *)
...
...
@@ -820,8 +855,8 @@ module MLToC = struct
let
cd
=
C
.
group_defs_by_type
cd
in
let
env'
=
{
computes_return_value
=
false
;
in_unguarded_loop
=
true
;
returns
_tuple
=
env
.
returns
_tuple
;
returns
=
env
.
returns
;
returns
=
env
.
returns
;
current_function
=
env
.
current_function
;
breaks
=
if
env
.
in_unguarded_loop
then
Sid
.
empty
else
env
.
breaks
}
in
...
...
@@ -856,8 +891,8 @@ module MLToC = struct
in
let
env'
=
{
computes_return_value
=
env
.
computes_return_value
;
in_unguarded_loop
=
false
;
returns_tuple
=
env
.
returns_tuple
;
breaks
=
breaks
;
current_function
=
env
.
current_function
;
breaks
=
breaks
;
returns
=
returns
;
}
in
expr
info
env'
b
...
...
@@ -870,22 +905,35 @@ module MLToC = struct
|
Eraise
(
_
,
None
)
->
assert
false
(* nothing to pass to return *)
|
Eraise
_
->
raise
(
Unsupported
"non break/return exception raised"
)
|
Efor
_
->
raise
(
Unsupported
"for loops"
)
(*TODO*)
|
Ematch
(
e1
,
[
Ptuple
rets
,
e2
]
,
[]
)
|
Ematch
(
({
e_node
=
Eapp
(
rs
,_
)}
as
e1
)
,
[
Ptuple
rets
,
e2
]
,
[]
)
when
List
.
for_all
(
function
Pvar
_
->
true
|_->
false
)
rets
->
let
rets
,
defs
=
List
.
fold_right
(
fun
p
(
r
,
d
)
->
match
p
with
|
Pvar
vs
->
(
C
.(
Eunop
(
Uaddr
,
Evar
vs
.
vs_name
))
::
r
,
C
.
Ddecl
(
ty_of_ty
info
vs
.
vs_ty
,
[
vs
.
vs_name
,
C
.
Enothing
])
::
d
)
|
_
->
assert
false
)
rets
([]
,
[]
)
in
let
d
,
s
=
expr
info
{
env
with
computes_return_value
=
false
}
e1
in
let
s'
=
C
.
add_to_last_call
rets
s
in
let
b
=
expr
info
env
e2
in
d
@
defs
,
C
.(
Sseq
(
s'
,
Sblock
b
))
let
id_struct
=
id_register
(
id_fresh
"struct_res"
)
in
let
e_struct
=
C
.
Evar
id_struct
in
let
d_struct
=
C
.
Ddecl
(
C
.
Tstruct
(
struct_of_rs
info
rs
)
,
[
id_struct
,
C
.
Enothing
])
in
let
defs
=
List
.
fold_right
(
fun
p
acc
->
match
p
with
|
Pvar
vs
->
C
.
Ddecl
(
ty_of_ty
info
vs
.
vs_ty
,
[
vs
.
vs_name
,
C
.
Enothing
])
::
acc
|
_
->
assert
false
)
rets
[
d_struct
]
in
let
d
,
s
=
expr
info
{
env
with
computes_return_value
=
false
}
e1
in
let
s
=
assignify
e_struct
s
in
let
assign
vs
i
=
assignify
(
C
.
Evar
vs
)
C
.(
Sexpr
(
Edot
(
e_struct
,
field
i
)))
in
let
rec
assigns
rets
i
=
match
rets
with
|
[]
->
C
.
Snop
|
Pvar
vs
::
t
->
C
.
Sseq
((
assign
vs
.
vs_name
i
)
,
(
assigns
t
(
i
+
1
)))
|
_
->
assert
false
in
let
assigns
=
assigns
rets
0
in
let
b
=
expr
info
env
e2
in
d
@
defs
,
C
.(
Sseq
(
Sseq
(
s
,
assigns
)
,
Sblock
b
))
|
Ematch
_
->
raise
(
Unsupported
"pattern matching"
)
|
Eabsurd
->
assert
false
|
Eassign
([
pv
,
({
rs_field
=
Some
_
}
as
rs
)
,
v
])
->
...
...
@@ -920,12 +968,12 @@ module MLToC = struct
else
C
.
Snop
)
|
Efun
_
->
raise
(
Unsupported
"higher order"
)
let
translate_decl
(
info
:
info
)
(
d
:
decl
)
:
C
.
definition
option
let
translate_decl
(
info
:
info
)
(
d
:
decl
)
:
C
.
definition
list
=
match
d
with
|
Dlet
(
Lsym
(
rs
,
_
,
vl
,
e
))
->
if
rs_ghost
rs
then
begin
if
debug
then
Format
.
printf
"is ghost@."
;
None
end