cprinter.ml 55.2 KB
Newer Older
Andrei Paskevich's avatar
headers  
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
headers  
Andrei Paskevich committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
12
open Ident
13

14
exception Unsupported = Printer.Unsupported
15

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
16
module C = struct
17

18
  (* struct name, fields) *)
19 20 21
  type struct_def = string * (string * ty) list

  and ty =
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
22
    | Tvoid
23
    | Tsyntax of string * ty list
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
24 25
    | Tptr of ty
    | Tarray of ty * expr
26
    | Tstruct of struct_def
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
27 28
    | Tunion of ident * (ident * ty) list
    | Tnamed of ident (* alias from typedef *)
29
    | Tnosyntax (* types that do not have a syntax, can't be printed *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
30 31 32 33 34 35 36 37 38 39 40
    (* enum, const could be added *)

  (* int x=2, *y ... *)
  and names = ty * (ident * expr) list

  (* names with a single declaration *)
  and name = ty * ident * expr

  (* return type, parameter list. Variadic functions not handled. *)
  and proto = ty * (ty * ident) list

41 42
  and binop = Band | Bor | Beq | Bne | Bassign | Blt | Ble | Bgt | Bge
  (* += and co. maybe to add *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
43

44
  and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
45 46 47 48 49

  and expr =
    | Enothing
    | Eunop of unop * expr
    | Ebinop of binop * expr * expr
50
    | Equestion of expr * expr * expr (* c ? t : e *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
51 52 53
    | Ecast of ty * expr
    | Ecall of expr * expr list
    | Econst of constant
54
    | Evar of ident
55 56
    | Elikely of expr (* __builtin_expect(e,1) *)
    | Eunlikely of expr (* __builtin_expect(e,0) *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
57 58 59
    | Esize_expr of expr
    | Esize_type of ty
    | Eindex of expr * expr (* Array access *)
60 61
    | Edot of expr * string (* Field access with dot *)
    | Earrow of expr * string (* Pointer access with arrow *)
62
    | Esyntaxrename of string * expr list (* syntax val f "g" w/o params *)
63
    | Esyntax of string * ty * (ty array) * (expr*ty) list * int list
64
  (* template, type and type arguments of result, typed arguments, precedence level *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82

  and constant =
    | Cint of string
    | Cfloat of string
    | Cchar of string
    | Cstring of string

  type stmt =
    | Snop
    | Sexpr of expr
    | Sblock of body
    | Sseq of stmt * stmt
    | Sif of expr * stmt * stmt
    | Swhile of expr * stmt
    | Sfor of expr * expr * expr * stmt
    | Sbreak
    | Sreturn of expr

83
  and include_kind = Sys | Proj (* include <...> vs. include "..." *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
84
  and definition =
85
    | Dfun of ident * proto * body
86
    | Dinclude of ident * include_kind
87
    | Dproto of ident * proto
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
88
    | Ddecl of names
89
    | Dstruct of struct_def
90
    | Dstruct_decl of string
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
91 92 93 94 95 96
    | Dtypedef of ty * ident

  and body = definition list * stmt

  type file = definition list

97 98
  exception NotAValue

99
  let rec is_nop = function
100
    | Snop | Sexpr Enothing -> true
101 102 103 104
    | Sblock ([], s) -> is_nop s
    | Sseq (s1,s2) -> is_nop s1 && is_nop s2
    | _ -> false

105 106 107 108 109 110 111 112
  let is_true = function
    | Sexpr(Econst(Cint "1")) -> true
    | _ -> false

  let is_false = function
    | Sexpr(Econst(Cint "0")) -> true
    | _ -> false

113 114 115 116 117 118
  let rec one_stmt = function
    | Snop -> true
    | Sexpr _ -> true
    | Sblock (d,s) -> d = [] && one_stmt s
    | _ -> false

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
119 120 121
  (** [assignify v] transforms a statement that computes a value into
     a statement that assigns that value to v *)
  let rec assignify v = function
122
    | Snop -> raise NotAValue
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
123 124 125 126 127 128 129
    | Sexpr e -> Sexpr (Ebinop (Bassign, v, e))
    | Sblock (ds, s) -> Sblock (ds, assignify v s)
    | Sseq (s1, s2) when not (is_nop s2) -> Sseq (s1, assignify v s2)
    | Sseq (s1,_) -> assignify v s1
    | Sif (c,t,e) -> Sif (c, assignify v t, assignify v e)
    | Swhile (c,s) -> Swhile (c, assignify v s) (* can this be a value ?*)
    | Sfor (e0,e1,e2,s) -> Sfor (e0,e1,e2, assignify v s)
130 131 132
    | Sbreak -> raise NotAValue
    | Sreturn _ -> raise NotAValue

133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156

  (** [get_last_expr] extracts the expression computed by the given statement.
     This is needed when loop conditions are more complex than a simple expression. *)
  let rec get_last_expr = function
    | Snop -> raise NotAValue
    | Sexpr e -> Snop, e
    | Sblock (ds,s) ->
      let s',e = get_last_expr s in
      Sblock(ds,s'), e
    | Sseq (s1,s2) when not (is_nop s2) ->
      let s', e = get_last_expr s2 in
      Sseq(s1,s'), e
    | Sseq (s1,_) -> get_last_expr s1
    | Sif (c,Sexpr t,Sexpr e) -> Snop, Equestion(c,t,e)
    | Sif _ -> raise (Unsupported "while (complex if)")
    | Swhile (_c,_s) -> raise (Unsupported "while (while) {}")
    | Sfor _ -> raise (Unsupported "while (for)")
    | Sbreak -> raise NotAValue
    | Sreturn _ -> raise NotAValue

  (** [propagate_in_expr id v] and the associated functions replace
      all instances of [id] by [v] in an
      expression/statement/definition/block. It is used for constant
      propagation to reduce the number of variables. *)
157 158 159 160 161 162 163
  let rec propagate_in_expr id (v:expr) = function
    | Evar i when Ident.id_equal i id -> v
    | Evar i -> Evar i
    | Eunop (u,e) -> Eunop (u, propagate_in_expr id v e)
    | Ebinop (b,e1,e2) -> Ebinop (b,
                                  propagate_in_expr id v e1,
                                  propagate_in_expr id v e2)
164 165 166
    | Equestion (c,t,e) -> Equestion(propagate_in_expr id v c,
                                     propagate_in_expr id v t,
                                     propagate_in_expr id v e)
167 168 169 170 171 172 173 174
    | Ecast (ty,e) -> Ecast (ty, propagate_in_expr id v e)
    | Ecall (e, l) -> Ecall (propagate_in_expr id v e,
                             List.map (propagate_in_expr id v) l)
    | Esize_expr e -> Esize_expr (propagate_in_expr id v e)
    | Eindex (e1,e2) -> Eindex (propagate_in_expr id v e1,
                                propagate_in_expr id v e2)
    | Edot (e,i) -> Edot (propagate_in_expr id v e, i)
    | Earrow (e,i) -> Earrow (propagate_in_expr id v e, i)
175
    | Esyntax (s,t,ta,l,p) ->
176 177 178
       Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l,p)
    | Esyntaxrename (s, l) ->
       Esyntaxrename (s, List.map (propagate_in_expr id v) l)
179 180
    | Enothing -> Enothing
    | Econst c -> Econst c
181 182
    | Elikely e -> Elikely (propagate_in_expr id v e)
    | Eunlikely e -> Eunlikely (propagate_in_expr id v e)
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
    | Esize_type ty -> Esize_type ty

  let rec propagate_in_stmt id v = function
    | Sexpr e -> Sexpr (propagate_in_expr id v e)
    | Sblock b -> Sblock(propagate_in_block id v b)
    | Sseq (s1,s2) -> Sseq (propagate_in_stmt id v s1,
                            propagate_in_stmt id v s2)
    | Sif (e,s1,s2) -> Sif (propagate_in_expr id v e,
                            propagate_in_stmt id v s1,
                            propagate_in_stmt id v s2)
    | Swhile (e, s) -> Swhile (propagate_in_expr id v e,
                               propagate_in_stmt id v s)
    | Sfor (e1,e2,e3,s) -> Sfor (propagate_in_expr id v e1,
                                 propagate_in_expr id v e2,
                                 propagate_in_expr id v e3,
                                 propagate_in_stmt id v s)
    | Sreturn e -> Sreturn (propagate_in_expr id v e)
    | Snop -> Snop
    | Sbreak -> Sbreak

  and propagate_in_def id v d =
    let rec aux = function
      | [] -> [], true
      | (i,e)::t ->
        if Ident.id_equal i id then (i,e)::t, false
        else let t,b = aux t in ((i,propagate_in_expr id v e)::t), b
    in
    match d with
    | Ddecl (ty,l) ->
      let l,b = aux l in
      Ddecl (ty, l), b
214
    | Dinclude (i,k) -> Dinclude (i,k), true
215
    | Dstruct _ -> raise (Unsupported "struct declaration inside function")
216
    | Dfun _ -> raise (Unsupported "nested function")
217
    | Dtypedef _ | Dproto _ | Dstruct_decl _ -> assert false
218 219 220 221 222 223 224 225 226 227 228 229

  and propagate_in_block id v (dl, s) =
    let dl, b = List.fold_left
      (fun (dl, acc) d ->
        if acc
        then
          let d, b = propagate_in_def id v d in
          (d::dl, b)
        else (d::dl, false))
      ([],true) dl in
    (List.rev dl, if b then propagate_in_stmt id v s else s)

230 231
  let is_empty_block s = s = Sblock([], Snop)
  let block_of_expr e = [], Sexpr e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
232

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
(** [flatten_defs d s] appends all definitions in the statement [s] to d. *)
  (* TODO check ident unicity ? *)
  let rec flatten_defs d = function
    | Sseq (s1,s2) ->
      let d, s1' = flatten_defs d s1 in
      let d, s2' = flatten_defs d s2 in
      d, Sseq(s1',s2')
    | Sblock (d',s) ->
      let d',s' = flatten_defs d' s in
      d@d', s'
    | Sif (c,t,e) ->
      let d, t' = flatten_defs d t in
      let d, e' = flatten_defs d e in
      d,Sif(c,t',e')
    | Swhile (c,s) ->
      let d, s' = flatten_defs d s in
      d, Swhile (c, s')
    | Sfor (e1,e2,e3,s) ->
      let d, s' = flatten_defs d s in
      d, Sfor(e1,e2,e3,s')
    | s -> d,s

255 256 257 258
  let rec group_defs_by_type l =
    (* heuristic to reduce the number of lines of defs*)
    let rec group_types t1 t2 =
      match t1, t2 with
259
      | Tvoid, Tvoid -> true
260 261 262
      | Tsyntax (s1, l1), Tsyntax (s2, l2) ->
        List.length l1 = List.length l2
        && List.for_all2 group_types l1 l2
263
        && s1 = s2
264
        && (not (String.contains s1 '*'))
265 266
      | Tptr t, Tptr t' -> group_types t t'
      | Tarray _, _ -> false
267
      | Tstruct (n1, _), Tstruct (n2, _) -> n1 = n2
268 269 270
      | Tunion (id1, _), Tunion (id2, _) -> id_equal id1 id2
      | Tnamed id1, Tnamed id2 -> id_equal id1 id2
      | _,_ -> false
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
    in
    match l with
    | [] | [_] -> l
    | Ddecl (ty1, el1) :: Ddecl (ty2, el2) :: l'
        when group_types ty1 ty2
          -> group_defs_by_type (Ddecl(ty1, el1@el2)::l')
    | Ddecl (ty1, el1) :: Ddecl (ty2, el2) :: Ddecl (ty3, el3) :: l'
        when group_types ty1 ty3
          -> group_defs_by_type (Ddecl (ty1, el1@el3) :: Ddecl (ty2, el2) :: l')
    | Ddecl (ty1, el1) :: Ddecl (ty2, el2) :: Ddecl (ty3, el3) :: l'
        when group_types ty2 ty3
          -> group_defs_by_type (Ddecl (ty1, el1) :: Ddecl (ty2, el2@el3) :: l')
    | Ddecl (ty1, el1) :: l' ->
      Ddecl (ty1, el1) :: group_defs_by_type l'
    | _ -> l

287 288 289 290 291 292 293 294 295
  let rec elim_empty_blocks = function
    | Sblock ([], s) -> elim_empty_blocks s
    | Sblock (d,s) -> Sblock (d, elim_empty_blocks s)
    | Sseq (s1,s2) -> Sseq (elim_empty_blocks s1, elim_empty_blocks s2)
    | Sif (c,t,e) -> Sif(c, elim_empty_blocks t, elim_empty_blocks e)
    | Swhile (c,s) -> Swhile(c, elim_empty_blocks s)
    | Sfor(e1,e2,e3,s) -> Sfor(e1,e2,e3,elim_empty_blocks s)
    | s -> s

296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
  let rec elim_nop = function
    | Sseq (s1,s2) ->
      let s1 = elim_nop s1 in
      let s2 = elim_nop s2 in
      begin match s1,s2 with
      | Snop, Snop -> Snop
      | Snop, s | s, Snop -> s
      | _ -> Sseq(s1,s2)
      end
    | Sblock (d,s) ->
      let s = elim_nop s in
      begin match d, s with
      | [], Snop -> Snop
      | _ -> Sblock(d,s)
      end
    | Sif (c,t,e) -> Sif(c, elim_nop t, elim_nop e)
    | Swhile (c,s) -> Swhile (c, elim_nop s)
    | Sfor(e1,e2,e3,s) -> Sfor(e1,e2,e3,elim_nop s)
    | s -> s

  let rec add_to_last_call params = function
    | Sblock (d,s) -> Sblock (d, add_to_last_call params s)
    | Sseq (s1,s2) when not (is_nop s2) ->
      Sseq (s1, add_to_last_call params s2)
    | Sseq (s1,_) -> add_to_last_call params s1
    | Sexpr (Ecall(fname, args)) ->
      Sexpr (Ecall(fname, params@args)) (*change name to ensure no renaming ?*)
    | Sreturn (Ecall (fname, args)) ->
      Sreturn (Ecall(fname, params@args))
    | _ -> raise (Unsupported "tuple pattern matching with too complex def")
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
326

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
327 328 329 330 331 332
  let rec stmt_of_list (l: stmt list) : stmt =
    match l with
    | [] -> Snop
    | [s] -> s
    | h::t -> Sseq (h, stmt_of_list t)

333 334 335 336
  let is_expr = function
    | Sexpr _ -> true
    | _ -> false

337
  let rec simplify_expr (d,s) : expr =
338
    match (d,elim_empty_blocks(elim_nop s)) with
339
    | [], Sblock([],s) -> simplify_expr ([],s)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
340
    | [], Sexpr e -> e
341 342
    | [], Sif(c,t,e) ->
       Equestion (c, simplify_expr([],t), simplify_expr([],e))
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
    | _ -> raise (Invalid_argument "simplify_expr")

  let rec simplify_cond (cd, cs) =
    match cd,elim_empty_blocks(elim_nop cs) with
    | [], Sexpr c -> ([], Sexpr c)
    | ([], Sif (c', t', e') as b) ->
       let _,t' = simplify_cond ([], t') in
       let _,e' = simplify_cond ([], e') in
       if is_false e' && is_expr t'(* c' && t' *)
       then
         let t' = simplify_expr ([],t') in
         [], Sexpr(Ebinop(Band, c', t'))
       else if is_true e' && is_expr t' (* !c' || t' *)
       then
         let t' = simplify_expr ([],t') in
         [], Sexpr(Ebinop(Bor,Eunop(Unot,c'),t'))
       else if is_true t' && is_expr e' (* c' || e' *)
       then
         let e' = simplify_expr ([],e') in
         [], Sexpr(Ebinop(Bor,c',e'))
       else if is_false t' && is_expr e' (* !c' && e' *)
       then
         let e' = simplify_expr ([],e') in
         [], Sexpr(Ebinop(Band,Eunop(Unot,c'),e'))
       else b
    | d,s -> d, s

370 371 372 373 374 375 376 377 378 379 380 381 382
(* Operator precedence, needed to compute which parentheses can be removed *)

  let prec_unop = function
    | Unot | Ustar | Uaddr | Upreincr | Upredecr -> 2
    | Upostincr  | Upostdecr -> 1

  let prec_binop = function
    | Band -> 11
    | Bor -> 11 (* really 12, but this avoids Wparentheses *)
    | Beq | Bne -> 7
    | Bassign -> 14
    | Blt | Ble | Bgt | Bge -> 6

383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
  let is_const_unop (u:unop) = match u with
    | Unot -> true
    | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr -> false

  let is_const_binop (b:binop) = match b with
    | Band | Bor | Beq | Bne | Blt | Ble | Bgt | Bge -> true
    | Bassign -> false

  let rec is_const_expr = function
    | Enothing -> true
    | Eunop (u,e) -> is_const_unop u && is_const_expr e
    | Ebinop (b,e1,e2) ->
       is_const_binop b && is_const_expr e1 && is_const_expr e2
    | Equestion (c,_,_) -> is_const_expr c
    | Ecast (_,_) -> true
    | Ecall (_,_) -> false
    | Econst _ -> true
    | Evar _ -> false
    | Elikely e | Eunlikely e -> is_const_expr e
    | Esize_expr _ -> false
    | Esize_type _ -> true
    | Eindex (_,_) | Edot (_,_) | Earrow (_,_) -> false
405
    | Esyntax (_,_,_,_,_) -> false
406
    | Esyntaxrename _ -> false
407 408 409 410 411 412 413 414 415 416 417

  let rec get_const_expr (d,s) =
    let fail () = raise (Unsupported "non-constant array size") in
    if (d = [])
    then match elim_empty_blocks (elim_nop s) with
    | Sexpr e -> if is_const_expr e then e
                 else fail ()
    | Sblock (d, s) -> get_const_expr (d,s)
    | _ -> fail ()
    else fail ()

418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
  let rec has_unboxed_struct = function
    | Tstruct _ -> true
    | Tunion (_, lidty)  -> List.exists has_unboxed_struct (List.map snd lidty)
    | Tsyntax (_, lty) -> List.exists has_unboxed_struct lty
    | _ -> false

  let rec has_array = function
    | Tarray _ -> true
    | Tsyntax (_,lty) -> List.exists has_array lty
    | Tstruct (_, lsty) -> List.exists has_array (List.map snd lsty)
    | Tunion (_,lidty) -> List.exists has_array (List.map snd lidty)
    | _ -> false

  let rec should_not_escape = function
    | Tstruct _ -> true
    | Tarray _ -> true
    | Tunion (_, lidty)  -> List.exists should_not_escape (List.map snd lidty)
    | Tsyntax (_, lty) -> List.exists should_not_escape lty
    | _ -> false

438 439 440 441 442 443 444 445
  let left_assoc = function
    | Band | Bor | Beq | Bne | Blt | Ble | Bgt | Bge -> true
    | Bassign -> false

  let right_assoc = function
    | Bassign -> true
    | _ -> false

446 447 448 449 450 451 452 453 454
  (** Integer type bounds *)
  open BigInt
  let min32 = minus (pow_int_pos 2 31)
  let max32 = sub (pow_int_pos 2 31) one
  let maxu32 = sub (pow_int_pos 2 32) one
  let min64 = minus (pow_int_pos 2 63)
  let max64 = sub (pow_int_pos 2 63) one
  let maxu64 = sub (pow_int_pos 2 64) one

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
455
end
456

457
type info = {
458 459 460
  env         : Env.env;
  prelude     : Printer.prelude;
  thprelude   : Printer.prelude_map;
461
  thinterface : Printer.interface_map;
462 463
  blacklist   : Printer.blacklist;
  syntax      : Printer.syntax_map;
464
  literal     : Printer.syntax_map; (*TODO handle literals*)
465
  kn          : Pdecl.known_map;
466
  prec        : (int list) Mid.t;
467 468
}

469 470 471
let debug_c_extraction = Debug.register_info_flag
                           ~desc:"C extraction"
                           "c_extraction"
472

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
473 474 475 476 477 478 479 480 481 482 483 484 485 486
module Print = struct

  open C
  open Format
  open Printer
  open Pp

  exception Unprinted of string

  let c_keywords = ["auto"; "break"; "case"; "char"; "const"; "continue"; "default"; "do"; "double"; "else"; "enum"; "extern"; "float"; "for"; "goto"; "if"; "int"; "long"; "register"; "return"; "short"; "signed"; "sizeof"; "static"; "struct"; "switch"; "typedef"; "union"; "unsigned"; "void"; "volatile"; "while" ]

  let () = assert (List.length c_keywords = 32)

  let sanitizer = sanitizer char_to_lalpha char_to_alnumus
487
  let sanitizer s = Strings.lowercase (sanitizer s)
488 489
  let local_printer = create_ident_printer c_keywords ~sanitizer
  let global_printer = create_ident_printer c_keywords ~sanitizer
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
490

491 492 493 494
  let print_local_ident fmt id = fprintf fmt "%s" (id_unique local_printer id)
  let print_global_ident fmt id = fprintf fmt "%s" (id_unique global_printer id)

  let clear_local_printer () = Ident.forget_all local_printer
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
495

496 497
  let space_nolinebreak fmt () = fprintf fmt " "

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
498 499 500 501
  let protect_on ?(boxed=false) x s =
    if x then "@[<1>(" ^^ s ^^ ")@]"
    else if not boxed then "@[" ^^ s ^^ "@]"
    else s
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
502

503 504 505 506 507 508 509
  let extract_stars ty =
    let rec aux acc = function
      | Tptr t -> aux (acc+1) t
      | t -> (acc, t)
    in
  aux 0 ty

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
510 511 512
  let rec print_ty ?(paren=false) fmt = function
    | Tvoid -> fprintf fmt "void"
    | Tsyntax (s, tl) ->
513
      syntax_arguments s (print_ty ~paren:false) fmt tl
514
    | Tptr ty -> fprintf fmt "%a *" (print_ty ~paren:true) ty
515
    (* should be handled in extract_stars *)
516
    | Tarray (ty, Enothing) ->
517
       fprintf fmt (protect_on paren "%a *")
518 519
         (print_ty ~paren:true) ty
    (* raise (Unprinted "printing array type with unknown size")*)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
520 521
    | Tarray (ty, expr) ->
      fprintf fmt (protect_on paren "%a[%a]")
522
        (print_ty ~paren:true) ty (print_expr ~prec:1) expr
523
    | Tstruct (s,_) -> fprintf fmt "struct %s" s
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
524
    | Tunion _ -> raise (Unprinted "unions")
525
    | Tnamed id -> print_global_ident fmt id
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
526 527 528 529 530 531
    | Tnosyntax -> raise (Unprinted "type without syntax")

  and print_unop fmt = function
    | Unot -> fprintf fmt "!"
    | Ustar -> fprintf fmt "*"
    | Uaddr -> fprintf fmt "&"
532 533 534 535 536 537
    | Upreincr | Upostincr -> fprintf fmt "++"
    | Upredecr | Upostdecr -> fprintf fmt "--"

  and unop_postfix = function
    | Upostincr | Upostdecr -> true
    | _ -> false
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
538 539 540 541 542 543 544

  and print_binop fmt = function
    | Band -> fprintf fmt "&&"
    | Bor -> fprintf fmt "||"
    | Beq -> fprintf fmt "=="
    | Bne -> fprintf fmt "!="
    | Bassign -> fprintf fmt "="
545 546 547 548
    | Blt -> fprintf fmt "<"
    | Ble -> fprintf fmt "<="
    | Bgt -> fprintf fmt ">"
    | Bge -> fprintf fmt ">="
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
549

550
  and print_expr ~prec fmt = function
551
    (* invariant: 0 <= prec <= 15 *)
552
    | Enothing -> ()
553
    | Eunop(u,e) ->
554
       let p = prec_unop u in
555
       if unop_postfix u
556 557 558 559
       then fprintf fmt (protect_on (prec < p) "%a%a")
              (print_expr ~prec:(p-1)) e print_unop u
       else fprintf fmt (protect_on (prec < p) "%a%a")
              print_unop u (print_expr ~prec:(p-1)) e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
560
    | Ebinop(b,e1,e2) ->
561
       let p = prec_binop b in
562 563 564 565
       let pleft = if left_assoc b then p else p-1 in
       let pright = if right_assoc b then p else p-1 in
       fprintf fmt (protect_on (prec < p) "%a %a %a")
         (print_expr ~prec:pleft) e1 print_binop b (print_expr ~prec:pright) e2
566
    | Equestion(c,t,e) ->
567 568 569
      fprintf fmt (protect_on (prec < 13) "%a ? %a : %a")
        (print_expr ~prec:12) c
        (print_expr ~prec:15) t
570
        (print_expr ~prec:13) e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
571
    | Ecast(ty, e) ->
572
      fprintf fmt (protect_on (prec < 2) "(%a)%a")
573
        (print_ty ~paren:false) ty (print_expr ~prec:2) e
574 575
    | Esyntaxrename (s, l) ->
       (* call to function defined in the prelude *)
576
       fprintf fmt (protect_on (prec < 1) "%s(%a)")
577 578
         s (print_list comma (print_expr ~prec:15)) l
    | Ecall (e,l) ->
579
       fprintf fmt (protect_on (prec < 1) "%a(%a)")
580
         (print_expr ~prec:1) e (print_list comma (print_expr ~prec:15)) l
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
581
    | Econst c -> print_const fmt c
582
    | Evar id -> print_local_ident fmt id
583
    | Elikely e -> fprintf fmt
584
                     (protect_on (prec < 1) "__builtin_expect(%a,1)")
585 586
                     (print_expr ~prec:15) e
    | Eunlikely e -> fprintf fmt
587
                       (protect_on (prec < 1) "__builtin_expect(%a,0)")
588
                       (print_expr ~prec:15) e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
589
    | Esize_expr e ->
590
       fprintf fmt (protect_on (prec < 2) "sizeof(%a)") (print_expr ~prec:15) e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
591
    | Esize_type ty ->
592
       fprintf fmt (protect_on (prec < 2) "sizeof(%a)")
593 594
         (print_ty ~paren:false) ty
    | Edot (e,s) ->
595
       fprintf fmt (protect_on (prec < 1) "%a.%s")
596
         (print_expr ~prec:1) e s
597 598 599 600
    | Eindex (e1, e2) ->
       fprintf fmt (protect_on (prec <= 1) "%a[%a]")
                      (print_expr ~prec:1) e1
                      (print_expr ~prec:15) e2
601 602 603
    | Earrow (e,s) ->
       fprintf fmt (protect_on (prec <= 1) "%a->%s")
         (print_expr ~prec:1) e s
604
    | Esyntax (s, t, args, lte, pl) ->
605 606 607 608
       if s = "%1" (*identity*)
       then begin
         assert (List.length lte = 1);
         print_expr ~prec fmt (fst (List.hd lte)) end
609 610 611 612 613 614 615 616 617
       else
         let s =
           if pl = [] || prec < List.hd pl
           then Format.sprintf "(%s)" s
           else s in
         gen_syntax_arguments_typed_prec snd (fun _ -> args)
           s
           (fun p fmt (e,_t) -> print_expr ~prec:p fmt e)
           (print_ty ~paren:false) (C.Enothing,t) pl fmt lte
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
618 619 620 621

  and print_const  fmt = function
    | Cint s | Cfloat s | Cchar s | Cstring s -> fprintf fmt "%s" s

622
  let print_id_init ?(size=None) ~stars fmt ie =
623 624
    (if stars > 0
    then fprintf fmt "%s " (String.make stars '*')
625 626 627 628 629 630 631 632 633 634 635 636
     else ());
    match size, ie with
    | None, (id, Enothing) -> print_local_ident fmt id
    | None, (id,e) ->
       fprintf fmt "%a = %a"
         print_local_ident id (print_expr ~prec:(prec_binop Bassign)) e
    | Some Enothing, (id, Enothing) ->
       (* size unknown, treat as pointer *)
       fprintf fmt "* %a" print_local_ident id
    | Some e, (id, Enothing) ->
       fprintf fmt "%a[%a]" print_local_ident id (print_expr ~prec:15) e
    | Some _es, (_id, _ei) -> raise (Unsupported "array initializer")
637 638

  let print_expr_no_paren fmt expr = print_expr ~prec:max_int fmt expr
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
639 640

  let rec print_stmt ~braces fmt = function
641
    | Snop | Sexpr Enothing -> Debug.dprintf debug_c_extraction "snop"; ()
642
    | Sexpr e -> fprintf fmt "%a;" print_expr_no_paren e;
643
    | Sblock ([] ,s) when not braces ->
644
      (print_stmt ~braces:false) fmt s
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
645 646 647 648
    | Sblock b -> fprintf fmt "@[<hov>{@\n  @[<hov>%a@]@\n}@]" print_body b
    | Sseq (s1,s2) -> fprintf fmt "%a@\n%a"
      (print_stmt ~braces:false) s1
      (print_stmt ~braces:false) s2
649
    | Sif(c,t,e) when is_nop e ->
650
       fprintf fmt "@[<hov 2>if (%a) {@\n@[<hov>%a@]@]@\n}"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
651 652 653
         print_expr_no_paren c (print_stmt ~braces:false) t
    | Sif(c,t,e) ->
       fprintf fmt
654
         "@[<hov 2>if (%a) {@\n@[<hov>%a@]@]@\n@[<hov 2>} else {@\n@[<hov>%a@]@]@\n}"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
655 656 657
         print_expr_no_paren c
         (print_stmt ~braces:false) t
         (print_stmt ~braces:false) e
658
    | Swhile (e,b) -> fprintf fmt "@[<hov 2>while (%a) {@\n@[<hov>%a@]@]@\n}"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
659
      print_expr_no_paren e (print_stmt ~braces:false) b
660
    | Sfor (einit, etest, eincr, s) ->
661
       fprintf fmt "@[<hov 2>for (%a; %a; %a) {@\n@[<hov>%a@]@\n}@]"
662 663 664
         print_expr_no_paren einit
         print_expr_no_paren etest
         print_expr_no_paren eincr
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
665
         (print_stmt ~braces:false) s
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
666
    | Sbreak -> fprintf fmt "break;"
667
    | Sreturn Enothing -> fprintf fmt "return;"
668
    | Sreturn e -> fprintf fmt "return %a;" print_expr_no_paren e
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
669

670 671
  and print_def fmt def =
    try match def with
672 673 674
      | Dfun (id,(rt,args),body) ->
         let s = sprintf "%a %a(@[%a@])@ @[<hov>{@;<1 2>@[<hov>%a@]@\n}@\n@]"
                   (print_ty ~paren:false) rt
675
                   print_global_ident id
676
                   (print_list comma
677
		      (print_pair_delim nothing space_nolinebreak nothing
678
			 (print_ty ~paren:false) print_local_ident))
679 680 681 682 683 684 685
	           args
                   print_body body in
         (* print into string first to print nothing in case of exception *)
         fprintf fmt "%s" s
      | Dproto (id, (rt, args)) ->
         let s = sprintf "%a %a(@[%a@]);@;"
                   (print_ty ~paren:false) rt
686
                   print_global_ident id
687
                   (print_list comma
688
                      (print_pair_delim nothing space_nolinebreak nothing
689
		         (print_ty ~paren:false) print_local_ident))
690 691
	           args in
         fprintf fmt "%s" s
692 693 694 695 696 697
      | Ddecl (Tarray(ty, e), lie) ->
         let s = sprintf "%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
698 699 700 701 702
      | Ddecl (ty, lie) ->
         let nb, ty = extract_stars ty in
         assert (nb=0);
         let s = sprintf "%a @[<hov>%a@];"
	           (print_ty ~paren:false) ty
703
	           (print_list comma (print_id_init ~stars:nb ~size:None)) lie in
704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720
         fprintf fmt "%s" s
      | Dstruct (s, lf) ->
         let s = sprintf "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 in
         fprintf fmt "%s" s
      | Dstruct_decl s ->
         fprintf fmt "struct %s;@;" s
      | Dinclude (id, Sys) ->
         fprintf fmt "#include <%s.h>@;"  (sanitizer id.id_string)
      | Dinclude (id, Proj) ->
         fprintf fmt "#include \"%s.h\"@;" (sanitizer id.id_string)
      | Dtypedef (ty,id) ->
         let s = sprintf "@[<hov>typedef@ %a@;%a;@]"
721
	           (print_ty ~paren:false) ty print_global_ident id in
722
         fprintf fmt "%s" s
723 724
    with Unprinted s ->
      Debug.dprintf debug_c_extraction "Missed a def because : %s@." s
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
725

726 727 728
  and print_body fmt (def, s) =
    if def = []
    then print_stmt ~braces:true fmt s
729 730 731 732
    else
      print_pair_delim nothing newline nothing
        (print_list newline print_def)
        (print_stmt ~braces:true)
733
        fmt (def,s)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
734

735 736 737 738
  let print_global_def fmt def =
    clear_local_printer ();
    print_def fmt def

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
739 740 741
  let print_file fmt info ast =
    Mid.iter (fun _ sl -> List.iter (fprintf fmt "%s\n") sl) info.thprelude;
    newline fmt ();
742
    fprintf fmt "@[<v>%a@]@." (print_list newline print_global_def) ast
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
743 744

end
745

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
746 747 748 749 750 751 752
module MLToC = struct

  open Ity
  open Ty
  open Expr
  open Term
  open Printer
753
  open Mltree
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
754 755
  open C

756 757 758
  let field i = "__field_"^(string_of_int i)

  let structs : struct_def Hid.t = Hid.create 16
759
  let aliases : C.ty Hid.t = Hid.create 16
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
760

761 762 763 764 765
  let array = create_attribute "ex:array"
  let array_mk = create_attribute "ex:array_make"
  let likely = create_attribute "ex:likely"
  let unlikely = create_attribute "ex:unlikely"

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
766 767 768 769 770 771 772 773
  let rec ty_of_ty info ty = (*FIXME try to use only ML tys*)
    match ty.ty_node with
    | Tyvar v ->
      begin match query_syntax info.syntax v.tv_name
        with
        | Some s -> C.Tsyntax (s, [])
        | None -> C.Tnamed (v.tv_name)
      end
774 775
    | Tyapp (ts, [t]) when Sattr.mem array ts.ts_name.id_attrs ->
       Tarray (ty_of_ty info t, Enothing)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
776 777 778 779
    | Tyapp (ts, tl) ->
       begin match query_syntax info.syntax ts.ts_name
        with
        | Some s -> C.Tsyntax (s, List.map (ty_of_ty info) tl)
780 781 782 783
        | None ->
           if tl = []
           then if is_ts_tuple ts
                then C.Tvoid
784 785 786
                else
                  if Hid.mem aliases ts.ts_name
                  then Hid.find aliases ts.ts_name
787 788 789 790 791 792 793 794 795 796 797 798
                else try Tstruct (Hid.find structs ts.ts_name)
                     with Not_found -> Tnosyntax
           else C.Tnosyntax
       end

  let rec ty_of_mlty info = function
    | Tvar { tv_name = id } ->
      begin match query_syntax info.syntax id
        with
        | Some s -> C.Tsyntax (s, [])
        | None -> C.Tnamed id
      end
799 800
    | Tapp (id, [t]) when Sattr.mem array id.id_attrs ->
       Tarray (ty_of_mlty info t, Enothing)
801 802 803 804 805 806
    | Tapp (id, tl) ->
       begin match query_syntax info.syntax id
        with
        | Some s -> C.Tsyntax (s, List.map (ty_of_mlty info) tl)
        | None ->
           if tl = []
807 808 809 810
           then if Hid.mem aliases id
                then Hid.find aliases id
                else try Tstruct (Hid.find structs id)
                     with Not_found -> Tnosyntax
811
           else Tnosyntax
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
812
       end
813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833
    | Ttuple [] -> C.Tvoid
    | Ttuple _ -> raise (Unsupported "tuple parameters")

  let struct_of_rs info rs : struct_def =
    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)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
834 835 836 837 838 839 840

  let ity_of_expr e = match e.e_ity with
    | I i -> i
    | _ -> assert false

  let pv_name pv = pv.pv_vs.vs_name

841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857
  let is_constructor rs its =
    List.exists (rs_equal rs) its.Pdecl.itd_constructors

  let is_struct_constructor info rs =
    let open Pdecl in
    if is_rs_tuple rs then false
    else match Mid.find_opt rs.rs_name info.kn with
      | Some { pd_node = PDtype its } ->
         List.exists (is_constructor rs) its
      | _ -> false

  let struct_of_constructor info rs =
    let open Pdecl in
    match Mid.find rs.rs_name info.kn with
    | { pd_node = PDtype its } ->
         let its = List.find (is_constructor rs) its in
         let id = its.itd_its.its_ts.ts_name in
858 859
         (try Hid.find structs id
         with Not_found -> raise (Unsupported "bad struct"))
860 861
    | _ -> assert false

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
862 863
  type syntax_env = { in_unguarded_loop : bool;
                      computes_return_value : bool;
864
                      current_function : rsymbol;
865
                      ret_regs : Sreg.t;
866
		      breaks : Sid.t;
867 868
                      returns : Sid.t;
                      array_sizes : C.expr Mid.t;
869
                      boxed : unit Hreg.t; (* is this struct boxed or passed by value? *)
870
                    }
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
871 872 873 874 875 876 877 878 879 880 881 882 883

  let is_true e = match e.e_node with
    | Eapp (s, []) -> rs_equal s rs_true
    | _ -> false

  let is_false e = match e.e_node with
    | Eapp (s, []) -> rs_equal s rs_false
    | _ -> false

  let is_unit = function
    | I i -> ity_equal i Ity.ity_unit
    | C _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
884 885 886
  let handle_likely attrs (e:C.expr) =
    let lkl = Sattr.mem likely attrs in
    let ulk = Sattr.mem unlikely attrs in
887 888 889 890 891 892 893 894 895
    if lkl
    then (if ulk then e else Elikely e)
    else (if ulk then Eunlikely e else e)

  let reverse_likely = function
    | Elikely e -> Eunlikely e
    | Eunlikely e -> Elikely e
    | e -> e

896 897 898 899 900
  (* /!\ Do not use if e may have type unit and not be Enothing *)
  let expr_or_return env e =
    if env.computes_return_value
    then Sreturn e
    else Sexpr e
901

902
  let rec expr info env (e:Mltree.expr) : C.body =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
903 904
    assert (not e.e_effect.eff_ghost);
    match e.e_node with
905
    | Eblock [] -> ([], expr_or_return env Enothing)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
906 907
    | Eblock [_] -> assert false
    | Eblock l ->
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
908
       let env_f = { env with computes_return_value = false } in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
909
       let rec aux = function
910
         | [] -> ([], expr_or_return env Enothing)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
911 912
         | [s] -> ([], C.Sblock (expr info env s))
         | h::t -> ([], C.Sseq (C.Sblock (expr info env_f h),
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
913 914 915 916
                                C.Sblock (aux t)))
       in
       aux l
    | Eapp (rs, []) when rs_equal rs rs_true ->
917 918
       Debug.dprintf debug_c_extraction "true@.";
       ([],expr_or_return env (C.Econst (Cint "1")))
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
919
    | Eapp (rs, []) when rs_equal rs rs_false ->
920 921
       Debug.dprintf debug_c_extraction "false@.";
       ([],expr_or_return env (C.Econst (Cint "0")))
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
922
    | Mltree.Evar pv ->
923 924
       let id = pv_name pv in
       let e = C.Evar id in
925
       ([], expr_or_return env e)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
926
    | Mltree.Econst ic ->
927 928
       let open Number in
       let print fmt ic =
929
        let n = ic.il_int in
930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951
        if BigInt.lt n BigInt.zero
        then Format.fprintf fmt "-%a" (print_in_base 10 None) (BigInt.abs n)
        else
          match ic.il_kind with
          | ILitHex -> Format.fprintf fmt "0x%a" (print_in_base 16 None) n
          | ILitOct -> Format.fprintf fmt "0%a" (print_in_base 8 None) n
          | _ ->
             (* default to base 10 *)
             Format.fprintf fmt "%a" (print_in_base 10 None) n in
        let s = match e.e_ity with
        | I i ->
           let ts = match (ty_of_ity i) with
             | { ty_node = Tyapp (ts, []) } -> ts
             | _ -> assert false in
           begin match query_syntax info.literal ts.ts_name with
           | Some st ->
              Format.asprintf "%a" (syntax_range_literal ~cb:(Some print) st) ic
           | _ ->
              let s = ts.ts_name.id_string in
              raise (Unsupported ("unspecified number format for type "^s)) end
        | _ -> assert false in
        let e = C.(Econst (Cint s)) in
952
        ([], expr_or_return env e)
953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976
    | Eapp (rs, el)
         when is_struct_constructor info rs
              && query_syntax info.syntax rs.rs_name = None ->
       Debug.dprintf debug_c_extraction "constructor %s@." rs.rs_name.id_string;
       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
       let args = List.map (fun e -> simplify_expr (expr info env_f e)) args in
       let ((sname, sfields) as sd) = struct_of_constructor info rs in
       let id = id_register (id_fresh sname) in
       let defs = [ Ddecl (Tstruct sd, [id, Enothing]) ] in
       let st = Evar id in
       let assign_expr f arg = Sexpr (Ebinop (Bassign, Edot (st, f), arg)) in
       let inits =
         List.fold_left2
           (fun acc (f, _ty) arg -> Sseq (acc,assign_expr f arg))
           Snop sfields args in
       (defs, Sseq (inits, expr_or_return env st))
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
977
    | Eapp (rs, el) ->
978
       Debug.dprintf debug_c_extraction "call to %s@." rs.rs_name.id_string;
979 980 981 982 983 984 985 986 987 988
       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
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
989
       if is_rs_tuple rs && env.computes_return_value
990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005
       then begin
         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
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
1006
       else
1007
	 let e' =
1008 1009 1010 1011