Skip to content

GitLab

why3
why3
Commit 226ba5b0 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Merge branch 'beautify_c' into 'master' 

Beautify C extraction

See merge request !370
parents 3cc3c446 e53acad2
Hide whitespace changes
Inline Side-by-side
Showing with 223 additions and 229 deletions
drivers/c.drv
View file @ 226ba5b0
......@@ -33,6 +33,9 @@ module mach.int.Int32
syntax val (<) "%1 < %2" prec 6 6 5
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
remove module
end
module mach.int.Int32BV
......@@ -47,6 +50,7 @@ module mach.int.Int32GMP
syntax val bxor "%1 ^ %2" prec 9 9 8
end
module mach.int.UInt32Gen
prelude export "#include <stdint.h>"
......@@ -56,6 +60,8 @@ module mach.int.UInt32Gen
syntax val max_uint32 "0xffffffff" prec 0
syntax val length "32" prec 0
remove module
end
module mach.int.UInt32BV
......@@ -81,48 +87,53 @@ module mach.int.UInt32
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
remove module
end
module mach.int.UInt32GMP
interface "\
\nstruct __add32_with_carry_result\
\n{ uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __add32_with_carry_result\
\n add32_with_carry(uint32_t x, uint32_t y, uint32_t c);\
\n\
\nstruct __sub32_with_borrow_result\
\n{ uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __sub32_with_borrow_result\
\n sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b);\
\n\
\nstruct __mul32_double_result\
\n{ uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __mul32_double_result mul32_double(uint32_t x, uint32_t y);\
\n\
\nstruct __add32_3_result\
\n{ uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z);\
\n\
\nstruct __lsld32_result\
\n{ uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);\
"
\nstruct __add32_with_carry_result {\
\n uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __add32_with_carry_result\
\nadd32_with_carry(uint32_t x, uint32_t y, uint32_t c);\
\n\
\nstruct __sub32_with_borrow_result {\
\n uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __sub32_with_borrow_result\
\nsub32_with_borrow(uint32_t x, uint32_t y, uint32_t b);\
\n\
\nstruct __mul32_double_result {\
\n uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __mul32_double_result\
\nmul32_double(uint32_t x, uint32_t y);\
\n\
\nstruct __add32_3_result {\
\n uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __add32_3_result\
\nadd32_3(uint32_t x, uint32_t y, uint32_t z);\
\n\
\nstruct __lsld32_result {\
\n uint32_t __field_0;\
\n uint32_t __field_1;\
\n};\
\n\
\nstruct __lsld32_result\
\nlsld32(uint32_t x, uint32_t cnt);\
"
syntax literal uint32 "%cU"
......@@ -170,6 +181,7 @@ blacklist "__builtin_clz" "__builtin_ctz" "add32_with_carry" "sub32_with_borrow"
blacklist "mul32_double" "add32_3" "lsld32"
module mach.int.Int64
syntax type int64 "int64_t"
syntax literal int64 "INT64_C(%c)"
......@@ -185,6 +197,8 @@ module mach.int.Int64
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
remove module
end
module mach.int.UInt64Gen
......@@ -196,6 +210,8 @@ module mach.int.UInt64Gen
syntax val max_uint64 "0xffffffffffffffff" prec 0
syntax val length "64" prec 0
remove module
end
module mach.int.UInt64
......@@ -214,76 +230,80 @@ module mach.int.UInt64
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
remove module
end
module mach.int.UInt64GMP
interface "\
\nstruct __add64_with_carry_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __add64_with_carry_result\
\nadd64_with_carry(uint64_t x, uint64_t y, uint64_t c)\
\n{\
\n struct __add64_with_carry_result result;\
\n uint64_t r = x + y + c;\
\n result.__field_0 = r;\
\n if (r == x) result.__field_1 = c;\
\n else result.__field_1 = (r < x);\
\n return result;\
\n}\
\n\
\nstruct __sub64_with_borrow_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __sub64_with_borrow_result\
\n sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)\
\n{\
\n struct __sub64_with_borrow_result result;\
\n uint64_t r = x - y - b;\
\n result.__field_0 = r;\
\n if (r > x) result.__field_1 = 1;\
\n else if (r == x) result.__field_1 = b;\
\n else result.__field_1 = 0;\
\n return result;\
\n}\
\n\
\nstruct __add64_3_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __add64_3_result\
\n add64_3(uint64_t x, uint64_t y, uint64_t z)\
\n{\
\n struct __add64_3_result result;\
\n uint64_t r, c1, c2;\
\n r = x + y;\
\n c1 = r < y;\
\n r += z;\
\n c2 = r < z;\
\n result.__field_1 = c1 + c2;\
\n result.__field_0 = r;\
\n return result;\
\n}\
\n\
\nstruct __lsld64_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)\
\n{\
\n struct __lsld64_result result;\
\n result.__field_1 = x >> (64 - cnt);\
\n result.__field_0 = x << cnt;\
\n return result;\
\n}\
"
\nstruct __add64_with_carry_result {\
\n uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __add64_with_carry_result\
\nadd64_with_carry(uint64_t x, uint64_t y, uint64_t c)\
\n{\
\n struct __add64_with_carry_result result;\
\n uint64_t r = x + y + c;\
\n result.__field_0 = r;\
\n if (r == x) result.__field_1 = c;\
\n else result.__field_1 = (r < x);\
\n return result;\
\n}\
\n\
\nstruct __sub64_with_borrow_result {\
\n uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __sub64_with_borrow_result\
\nsub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)\
\n{\
\n struct __sub64_with_borrow_result result;\
\n uint64_t r = x - y - b;\
\n result.__field_0 = r;\
\n if (r > x) result.__field_1 = 1;\
\n else if (r == x) result.__field_1 = b;\
\n else result.__field_1 = 0;\
\n return result;\
\n}\
\n\
\nstruct __add64_3_result {\
\n uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __add64_3_result\
\nadd64_3(uint64_t x, uint64_t y, uint64_t z)\
\n{\
\n struct __add64_3_result result;\
\n uint64_t r, c1, c2;\
\n r = x + y;\
\n c1 = r < y;\
\n r += z;\
\n c2 = r < z;\
\n result.__field_1 = c1 + c2;\
\n result.__field_0 = r;\
\n return result;\
\n}\
\n\
\nstruct __lsld64_result\
\n{ uint64_t __field_0;\
\n uint64_t __field_1;\
\n};\
\n\
\nstatic inline struct __lsld64_result\
\nlsld64(uint64_t x, uint64_t cnt)\
\n{\
\n struct __lsld64_result result;\
\n result.__field_1 = x >> (64 - cnt);\
\n result.__field_0 = x << cnt;\
\n return result;\
\n}\
"
syntax literal uint64 "UINT64_C(%c)"
syntax val uint64_max "0xffffffffffffffffUL" prec 0
......@@ -444,6 +464,8 @@ module mach.c.UChar
syntax val open_from_charptr "(unsigned char *)%1" prec 2 2
syntax val close_from_charptr "IGNORE2"
remove module
end
module mach.c.SChar
......@@ -499,97 +521,65 @@ end
(* exclude some stdlib modules from extraction *)
module array.Array
remove module
end
module bool.Bool
remove module
end
module map.Map
remove module
end
module map.Const
remove module
end
module number.Divisibility
remove module
end
module int.Int
remove module
end
module int.Abs
remove module
end
module int.ComputerDivision
remove module
end
module int.EuclideanDivision
remove module
end
module int.MinMax
remove module
end
module int.Power
remove module
end
module real.Real
remove module
end
module real.ExpLog
remove module
end
module real.RealInfix
remove module
end
module real.Square
remove module
end
module mach.int.Unsigned
remove module
end
\ No newline at end of file
end
examples/multiprecision/Makefile
View file @ 226ba5b0
......@@ -59,9 +59,9 @@ extract: $(EXTRACTED)
CFILES = \
zutil.c z.c zcmp.c zcmpabs.c zabs.c zadd.c zsub.c zmul.c zdiv.c zmul2exp.c zdiv2exp.c zget_str.c zset_str.c \
set.c get_str.c set_str.c baseinfo.c powm.c fxp.c sqrt.c sqrt1.c toom.c div.c \
set.c get_str.c set_str.c baseinfo.c powm.c sqrt.c sqrt1.c toom.c div.c \
logical.c logicalold.c logicalutil.c mul_basecase.c sub.c sub_1.c add.c add_1.c \
compare.c util.c utilold.c int32.c
compare.c util.c utilold.c
ifneq ($(OVERLAY),gmp)
CFILES += mul.c addold.c subold.c
......
examples/multiprecision/wmpn.drv
View file @ 226ba5b0
......@@ -80,53 +80,53 @@ blacklist "mul64_double" "div64_2by1"
module ptralias.Alias
interface "\n\
struct __open_sep_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
};\n\
\n\
struct __open_rx_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
};\n\
\n\
struct __open_shift_sep_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
};\n\
\n\
static inline struct __open_sep_result\n\
open_sep (uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy)\n\
{\n\
struct __open_sep_result result;\n\
result.__field_0 = r;\n\
result.__field_1 = x;\n\
result.__field_2 = y;\n\
return result;\n\
}\n\
\n\
static inline struct __open_rx_result\n\
open_rx (uint64_t * x, int32_t sx, uint64_t * y, int32_t sy)\n\
{\n\
struct __open_rx_result result;\n\
result.__field_0 = x;\n\
result.__field_1 = x;\n\
result.__field_2 = y;\n\
return result;\n\
}\n\
\n\
static inline struct __open_shift_sep_result\n\
open_shift_sep (uint64_t * r, uint64_t * x, int32_t sz)\n\
{\n\
struct __open_shift_sep_result result;\n\
result.__field_0 = r;\n\
result.__field_1 = x;\n\
return result;\n\
}\n\
"
interface "\
\nstruct __open_sep_result {\
\n uint64_t *__field_0;\
\n uint64_t *__field_1;\
\n uint64_t *__field_2;\
\n};\
\n\
\nstruct __open_rx_result {\
\n uint64_t *__field_0;\
\n uint64_t *__field_1;\
\n uint64_t *__field_2;\
\n};\
\n\
\nstruct __open_shift_sep_result {\
\n uint64_t *__field_0;\
\n uint64_t *__field_1;\
\n};\
\n\
\nstatic inline struct __open_sep_result\
\nopen_sep (uint64_t *r, uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\n{\
\n struct __open_sep_result result;\
\n result.__field_0 = r;\
\n result.__field_1 = x;\
\n result.__field_2 = y;\
\n return result;\
\n}\
\n\
\nstatic inline struct __open_rx_result\
\nopen_rx (uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)\
\n{\
\n struct __open_rx_result result;\
\n result.__field_0 = x;\
\n result.__field_1 = x;\
\n result.__field_2 = y;\
\n return result;\
\n}\
\n\
\nstatic inline struct __open_shift_sep_result\
\nopen_shift_sep (uint64_t *r, uint64_t *x, int32_t sz)\
\n{\
\n struct __open_shift_sep_result result;\
\n result.__field_0 = r;\
\n result.__field_1 = x;\
\n return result;\
\n}\
"
syntax val open_sep "open_sep"
syntax val open_rx "open_rx"
......@@ -201,4 +201,8 @@ void __wmpz_init (wmpz_ptr);\
end
blacklist "__wmpz_init"
\ No newline at end of file
blacklist "__wmpz_init"
module types.Types
remove module
end
src/extract/c.ml
View file @ 226ba5b0
......@@ -88,6 +88,7 @@ module C = struct
| Dinclude of ident * include_kind
| Dproto of ident * proto
| Ddecl of names
| Dextern of ty * ident
| Dstruct of struct_def
| Dstruct_decl of string
| Dtypedef of ty * ident
......@@ -220,7 +221,7 @@ module C = struct
| Dinclude (i,k) -> Dinclude (i,k), true
| Dstruct _ -> raise (Unsupported "struct declaration inside function")
| Dfun _ -> raise (Unsupported "nested function")
| Dtypedef _ | Dproto _ | Dstruct_decl _ -> assert false
| Dextern _ | Dtypedef _ | Dproto _ | Dstruct_decl _ -> assert false
and propagate_in_block id v (dl, s) =
let dl, b = List.fold_left
......@@ -549,9 +550,9 @@ module Print = struct
(* prints the c inline keyword *)
let print_local_ident fmt id =
fprintf fmt "%s" (id_unique (Opt.get !local_printer) id)
pp_print_string fmt (id_unique (Opt.get !local_printer) id)
let print_global_ident fmt id =
fprintf fmt "%s" (id_unique (Opt.get !global_printer) id)
pp_print_string fmt (id_unique (Opt.get !global_printer) id)
let clear_local_printer () = Ident.forget_all (Opt.get !local_printer)
......@@ -697,7 +698,7 @@ module Print = struct
gen_syntax_arguments_prec fmt s pr pl
and print_const fmt = function
| Cint (s,_) | Cfloat s -> fprintf fmt "%s" s
| Cint (s,_) | Cfloat s -> pp_print_string fmt s
| Cchar s -> fprintf fmt "'%s'" Constant.(escape char_escape s)
| Cstring s -> fprintf fmt "\"%s\"" Constant.(escape default_escape s)
let print_id_init ?(size=None) ~stars fmt ie =
......@@ -754,9 +755,9 @@ module Print = struct
if Sattr.mem c_static_inline id.id_attrs
then fprintf fmt "static inline "
else fprintf fmt "" in
try match def with
match def with
| Dfun (id,(rt,args),body) ->
let s = sprintf "@[@\n@[<hv 2>%a%a %a(@[%a@]) {@\n@[%a@]@]\n}@]"
fprintf fmt "@[@\n@[<hv 2>%a%a %a(@[%a@]) {@\n@[%a@]@]\n}@]"
print_inline id
(print_ty ~paren:false) rt
print_global_ident id
......@@ -764,42 +765,36 @@ module Print = struct
(print_pair_delim nothing space_nolinebreak nothing
(print_ty ~paren:false) print_local_ident))
args
print_body body in
(* print into string first to print nothing in case of exception *)
fprintf fmt "%s" s
print_body body
| Dproto (id, (rt, args)) ->
let s = sprintf "@\n%a %a(@[%a@]);"
fprintf fmt "@\n%a %a(@[%a@]);"
(print_ty ~paren:false) rt
print_global_ident id
(print_list comma
(print_pair_delim nothing space_nolinebreak nothing
(print_ty ~paren:false) print_local_ident))
args in
fprintf fmt "%s" s
args
| Ddecl (Tarray(ty, e), lie) ->
let s = sprintf "%a @[<hov>%a@];"
fprintf fmt "%a @[<hov>%a@];"
(print_ty ~paren:false) ty
(print_list comma (print_id_init ~stars:0 ~size:(Some e)))
lie in
fprintf fmt "%s" s
lie
| Ddecl (ty, lie) ->
let nb, ty = extract_stars ty in
assert (nb=0);
let s = sprintf "%a @[<hov>%a@];"
if global then pp_force_newline fmt ();
let nb, ty = extract_stars ty in
assert (nb = 0);
fprintf fmt "%a @[<hov>%a@];"
(print_ty ~paren:false) ty
(print_list comma (print_id_init ~stars:nb ~size:None))
lie in
if global
then fprintf fmt "@\n%s" s
else fprintf fmt "%s" s
lie
| Dextern (ty, id) ->
fprintf fmt "@\nextern %a %a;" (print_ty ~paren:false) ty print_local_ident id
| Dstruct (s, lf) ->
let s = sprintf "@\nstruct %s@ @[<hov>{@;<1 2>@[<hov>%a@]@\n};@]"
s
(print_list newline
(fun fmt (s,ty) -> fprintf fmt "%a %s;"
(print_ty ~paren:false) ty s))
lf in
fprintf fmt "%s" s
fprintf fmt "@\nstruct %s {@\n%a};" s
(print_list_suf newline
(fun fmt (s,ty) -> fprintf fmt " %a %s;"
(print_ty ~paren:false) ty s))
lf
| Dstruct_decl s ->
fprintf fmt "struct %s;@;" s
| Dinclude (id, Sys) ->
......@@ -807,16 +802,8 @@ module Print = struct
| Dinclude (id, Proj) ->
fprintf fmt "#include \"%s.h\"" (sanitizer id.id_string)
| Dtypedef (ty,id) ->
let s = sprintf "@[<hov>typedef@ %a@;%a;@]"
(print_ty ~paren:false) ty print_global_ident id in
fprintf fmt "%s" s
with
Unprinted s ->
if Debug.test_noflag debug_c_no_error_msgs
then
Format.eprintf
"Could not print declaration of %s. Unsupported: %s@."
!current_decl_name s
fprintf fmt "@[<hov>typedef@ %a@;%a;@]"
(print_ty ~paren:false) ty print_global_ident id
and print_body fmt (def, s) =
if def = []
......@@ -828,8 +815,20 @@ module Print = struct
fmt (def,s)
let print_global_def fmt def =
clear_local_printer ();
print_def ~global:true fmt def
try
clear_local_printer ();
let buf = Buffer.create 1024 in
let f = formatter_of_buffer buf in
print_def ~global:true f def;
pp_print_flush f ();
pp_print_string fmt (Buffer.contents buf)