cprinter.ml 17.3 KB
Newer Older
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
1
open Ident
2

3 4
exception Unsupported of string

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
5
module C = struct
6

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
7 8
  type ty =
    | Tvoid
9
    | Tsyntax of string * ty list
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
10 11 12 13 14
    | Tptr of ty
    | Tarray of ty * expr
    | Tstruct of ident * (ident * ty) list
    | Tunion of ident * (ident * ty) list
    | Tnamed of ident (* alias from typedef *)
15
    | Tnosyntax (* types that do not have a syntax, can't be printed *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
    (* 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

  and binop = Band | Bor | Beq | Bne | Bassign (* += and co. maybe to add *)

  and unop = Unot | Ustar | Uaddr (* (pre|post)(incr|decr) maybe to add *)

  and expr =
    | Enothing
    | Eunop of unop * expr
    | Ebinop of binop * expr * expr
    | Ecast of ty * expr
    | Ecall of expr * expr list
    | Econst of constant
38
    | Evar of ident
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
39 40 41
    | Esize_expr of expr
    | Esize_type of ty
    | Eindex of expr * expr (* Array access *)
42 43
    | Edot of expr * ident (* Field access with dot *)
    | Earrow of expr * ident (* Pointer access with arrow *)
44
    | Esyntax of string * ty * (ty array) * (expr*ty) list
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63

  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

  and definition =
64
    | Dfun of ident * proto * body
65
    | Dinclude of ident
66
    | Dproto of ident * proto
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
67 68 69 70 71 72 73
    | Ddecl of names
    | Dtypedef of ty * ident

  and body = definition list * stmt

  type file = definition list

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
  exception NotAValue

  (* [assignify id] transforms a statement that computes a value into
     a statement that assigns that value to id *)
  let rec assignify id = function
    | Snop -> raise NotAValue
    | Sexpr e -> Sexpr (Ebinop (Bassign, Evar id, e))
    | Sblock (ds, s) -> Sblock (ds, assignify id s)
    | Sseq (s1, s2) -> Sseq (s1, assignify id s2)
    | Sif (c,t,e) -> Sif (c, assignify id t, assignify id e)
    | Swhile (c,s) -> Swhile (c, assignify id s) (* can this be a value ?*)
    | Sfor (e0,e1,e2,s) -> Sfor (e0,e1,e2, assignify id s)
    | Sbreak -> raise NotAValue
    | Sreturn _ -> raise NotAValue

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
  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)
    | 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)
104 105
    | Esyntax (s,t,ta,l) ->
      Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l)
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
    | Enothing -> Enothing
    | Econst c -> Econst c
    | 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
    | Dinclude i -> Dinclude i, true
    | Dfun _ -> raise (Unsupported "nested function")
141 142
    | Dtypedef _ -> raise (Unsupported "typedef inside function")
    | Dproto _ -> raise (Unsupported "prototype inside function")
143 144 145 146 147 148 149 150 151 152 153 154

  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)

155 156
  let is_empty_block s = s = Sblock([], Snop)
  let block_of_expr e = [], Sexpr e
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
end

type info = Pdriver.printer_args = private {
  env         : Env.env;
  prelude     : Printer.prelude;
  thprelude   : Printer.prelude_map;
  blacklist   : Printer.blacklist;
  syntax      : Printer.syntax_map;
  converter   : Printer.syntax_map;
}

module Translate = struct
  open Pdecl
  open Ity
  open Ty
  open Expr
  open Term
  open Printer
175
  open Pmodule
176

177
  let rec ty_of_ty info ty =
178 179 180 181
    match ty.ty_node with
    | Tyvar v ->
      begin match query_syntax info.syntax v.tv_name
        with
182
        | Some s -> C.Tsyntax (s, [])
183 184
        | None -> C.Tnamed (v.tv_name)
      end
185
    | Tyapp (ts, tl) ->
186 187
       begin match query_syntax info.syntax ts.ts_name
        with
188
        | Some s -> C.Tsyntax (s, List.map (ty_of_ty info) tl)
189
        | None -> C.Tnosyntax
190 191 192 193
       end

  let pv_name pv = pv.pv_vs.vs_name

194 195 196 197 198 199 200 201 202
  let rec expr info ?(is_return=false) (e:expr) : C.body =
    if e_ghost e then (Format.printf "translating ghost expr@."; C.([], Snop))
    else if is_e_void e then C.([], Snop)
    else if is_e_true e then expr info ~is_return (e_nat_const 1)
    else if is_e_false e then expr info ~is_return (e_nat_const 0)
    else match e.e_node with
    | Evar pv ->
       let e = C.Evar(pv_name pv) in
       C.([], if is_return then Sreturn e else Sexpr e)
203 204
    | Econst (Number.ConstInt ic) ->
      let n = Number.compute_int ic in
205 206 207
      let e = C.(Econst (Cint (BigInt.to_string n))) in
      C.([], if is_return then Sreturn e else Sexpr e)
    | Econst _ -> raise (Unsupported "real constants")
208
    | Eexec (ce, _cty) ->
209
      begin match ce.c_node with
210
      | Cfun e -> expr info ~is_return e
211
      | Capp (rs, pvsl) ->
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
         let e =  match query_syntax info.syntax rs.rs_name with
           | Some s ->
              let params =
		List.map (fun pv -> (C.Evar(pv_name pv), ty_of_ty info (ty_of_ity pv.pv_ity)))
			 pvsl in
              let rty = ty_of_ity rs.rs_cty.cty_result 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)
           | None ->
              let args = List.filter (fun pv -> not pv.pv_ghost) pvsl in
              C.(Ecall(Evar(rs.rs_name), List.map (fun pv -> Evar(pv_name pv)) args))
         in
	 C.([], if is_return then Sreturn e else Sexpr e)
      | _ -> raise (Unsupported "Cpur/Cany") (*TODO clarify*)
229
      end
230
    | Eassign _ -> raise (Unsupported "mutable field assign")
231 232 233
    | Elet (ld,e) ->
      begin match ld with
      | LDvar (pv,le) ->
234
        Format.printf "let %s@." pv.pv_vs.vs_name.id_string;
235
        if pv.pv_ghost then expr info ~is_return e
236
        else if ((pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit)
237 238
        then ([], C.Sseq (C.Sblock(expr info ~is_return:false le),
			  C.Sblock(expr info ~is_return e)))
239 240 241 242 243
        else begin
          match le.e_node with
          | Econst (Number.ConstInt ic) ->
            let n = Number.compute_int ic in
            let cexp = C.(Econst (Cint (BigInt.to_string n))) in
244 245 246
	    Format.printf "propagate constant %s for var %s@."
			  (BigInt.to_string n) (pv_name pv).id_string;
            C.propagate_in_block (pv_name pv) cexp (expr info ~is_return e)
247
          | _->
248
            let t = ty_of_ty info (ty_of_ity pv.pv_ity) in
249 250
            let d,s = expr info ~is_return:false le in
	    let initblock = d, C.assignify (pv_name pv) s in
251
            [ C.Ddecl (t, [pv_name pv, C.Enothing]) ],
252
            C.Sseq (C.Sblock initblock, C.Sblock (expr info ~is_return e))
253
        end
254 255
      | _ -> assert false
      end
256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
    | Eif (cond, th, el) ->
       let c = expr info ~is_return:false cond in
       let t = expr info ~is_return th in
       let e = expr info ~is_return el in
       begin match c with
	     | [], C.Sexpr c ->
		if is_e_false th && is_e_true el
		then C.([], Sexpr(Eunop(Unot, c)))
		else [], C.Sif(c,C.Sblock t, C.Sblock e)
	     | cdef, cs ->
		let cid = id_register (id_fresh "cond") in (* ? *)
		C.Ddecl (C.Tsyntax ("int",[]), [cid, C.Enothing])::cdef,
		C.Sseq (C.assignify cid cs, C.Sif (C.Evar cid, C.Sblock t, C.Sblock e))
       (* TODO detect empty branches and replace with Snop, detect and/or*)
       end
271
    | Ewhile (c,_,_,e) ->
272 273
      let cd, cs = expr info ~is_return:false c in
      let b = expr info ~is_return:false e in
274 275 276 277
      begin match cs with
      | C.Sexpr ce -> cd, C.Swhile (ce, C.Sblock b)
      | _ ->
        let cid = id_register (id_fresh "cond") in (* ? *)
278
        [C.Ddecl (C.Tsyntax ("int",[]), [cid, C.Enothing])],
279 280
        C.Sseq (C.Sblock (cd, cs), C.Swhile (C.Evar cid, C.Sblock b))
      end
281
    | Etry _ | Eraise _ -> raise (Unsupported "try/exceptions") (*TODO*)
282
    | Efor _ -> raise (Unsupported "for loops")  (*TODO*)
283
    | Eassert _ -> [], C.Snop
284 285
    | Ecase _ -> raise (Unsupported "pattern matching")
    | Eghost _ | Epure _ | Eabsurd -> assert false
286 287 288 289

  let pdecl info (pd:Pdecl.pdecl) : C.definition list =
    match pd.pd_node with
    | PDlet (LDsym (rs, ce)) ->
290 291
      let fname = rs.rs_name in
      Format.printf "PDlet rsymbol %s@." fname.id_string;
292 293
      if Mid.mem fname info.syntax then (Format.printf "has syntax@."; [])
      else
294
        let params = List.map
295 296 297 298 299
		       (fun pv -> ty_of_ty info pv.pv_vs.vs_ty, pv_name pv)
		       (List.filter
			  (fun pv -> not pv.pv_ghost && not (ity_equal pv.pv_ity ity_unit))
			  rs.rs_cty.cty_args) in
        begin match ce.c_node with
300
        | Cfun e ->
301 302 303 304 305
           let rity = rs.rs_cty.cty_result in
           let rtype =
             if ity_equal rity ity_unit then C.Tvoid
             else ty_of_ty info (ty_of_ity rity) in
           [C.Dfun (fname, (rtype,params), expr info ~is_return:true e)]
306
        | _ -> raise (Unsupported "Non-function with no syntax in toplevel let")
307
	end
308 309
    | PDtype [{itd_its = its}] ->
      let id = its.its_ts.ts_name in
310
      Format.printf "PDtype %s@." id.id_string;
311 312 313
      begin
        match its.its_ts.ts_def with
        | Some def -> [C.Dtypedef (ty_of_ty info def, id)]
314 315
        | None ->
          begin match query_syntax info.syntax id with
316
          | Some _ -> []
317 318 319
          | None ->
            raise (Unsupported "type declaration without syntax or alias")
          end
320 321
      end

322 323 324 325 326
    | _ -> [] (*TODO exn ? *)


  let munit info = function
    | Udecl pd -> pdecl info pd
327
    | Uuse m -> [C.Dinclude m.mod_theory.Theory.th_name]
328 329 330 331 332 333 334 335 336 337 338
    | Uclone _ -> raise (Unsupported "clone")
    | Umeta _ -> raise (Unsupported "meta")
    | Uscope _ -> []

  let translate (info:info) (m:pmodule) : C.file =
    Format.printf "Translating module %s@."
      m.mod_theory.Theory.th_name.id_string;
    try List.flatten (List.map (munit info) m.mod_units)
    with
    | Unsupported s ->
      Format.printf "Failed because of unsupported construct: %s@." s; []
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
339
end
340
(*TODO simplifications : propagate constants, collapse blocks with only a statement and no def*)
341

342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
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
  let printer = create_ident_printer c_keywords ~sanitizer

  let print_ident fmt id = fprintf fmt "%s" (id_unique printer id)

  let protect_on x s = if x then "(" ^^ s ^^ ")" else s

  let rec print_ty ?(paren=false) fmt = function
    | Tvoid -> fprintf fmt "void"
364
    | Tsyntax (s, tl) -> syntax_arguments s (print_ty ~paren:false) fmt tl
365 366 367 368 369 370 371
    | Tptr ty -> fprintf fmt "(%a)*" (print_ty ~paren:true) ty
    | Tarray (ty, expr) ->
      fprintf fmt (protect_on paren "%a[%a]")
        (print_ty ~paren:true) ty (print_expr ~paren:false) expr
    | Tstruct _ -> raise (Unprinted "structs")
    | Tunion _ -> raise (Unprinted "unions")
    | Tnamed id -> print_ident fmt id
372
    | Tnosyntax -> raise (Unprinted "type without syntax")
373 374 375 376 377 378 379 380 381 382 383 384 385 386

  and print_unop fmt = function
    | Unot -> fprintf fmt "!"
    | Ustar -> fprintf fmt "*"
    | Uaddr -> fprintf fmt "&"

  and print_binop fmt = function
    | Band -> fprintf fmt "&&"
    | Bor -> fprintf fmt "||"
    | Beq -> fprintf fmt "=="
    | Bne -> fprintf fmt "!="
    | Bassign -> fprintf fmt "="

  and print_expr ?(paren=false) fmt = function
387
    | Enothing -> Format.printf "enothing"; ()
388
    | Eunop(u,e) -> fprintf fmt (protect_on paren "%a %a")
389
      print_unop u (print_expr ~paren:true) e
390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
    | Ebinop(b,e1,e2) ->
      fprintf fmt (protect_on paren "%a %a %a")
        (print_expr ~paren:true) e1 print_binop b (print_expr ~paren:true) e2
    | Ecast(ty, e) ->
      fprintf fmt (protect_on paren "(%a)%a")
        (print_ty ~paren:false) ty (print_expr ~paren:true) e
    | Ecall (e,l) -> fprintf fmt (protect_on paren "%a(%a)")
      (print_expr ~paren:true) e (print_list comma (print_expr ~paren:false)) l
    | Econst c -> print_const fmt c
    | Evar id -> print_ident fmt id
    | 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")
    | Esyntax (s, t, args, lte) ->
406 407 408
      gen_syntax_arguments_typed snd (fun _ -> args)
        (if paren then ("("^s^")") else s)
        (fun fmt (e,_t) -> print_expr ~paren:false fmt e)
409 410 411 412 413
        (print_ty ~paren:false) (C.Enothing,t) fmt lte

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

414 415 416
  let print_id_init fmt = function
    | id, Enothing -> print_ident fmt id
    | id,e -> fprintf fmt "%a = %a" print_ident id (print_expr ~paren:false) e
417 418

  let rec print_stmt fmt = function
419 420 421 422 423 424 425
    | Snop -> Format.printf "snop"; ()
    | Sexpr e -> fprintf fmt "%a;" (print_expr ~paren:false) e;
    | Sblock b -> fprintf fmt "@[<hv>{@;<1 2>@[<hv>%a@]@\n}@]" print_body b
    | Sseq (s1,s2) -> fprintf fmt "%a@\n%a" print_stmt s1 print_stmt s2
    | Sif(c,t,e) when is_empty_block e ->
       fprintf fmt "if(%a)@\n%a" (print_expr ~paren:false) c print_stmt t
    | Sif (c,t,e) -> fprintf fmt "if(%a)@\n%a@\nelse@\n%a"
426 427 428 429
      (print_expr ~paren:false) c print_stmt t print_stmt e
    | Swhile (e,b) -> fprintf fmt "while (%a)@ %a"
      (print_expr ~paren:false) e print_stmt b
    | Sfor _ -> raise (Unprinted "for loops")
430 431
    | Sbreak -> fprintf fmt "break;"
    | Sreturn e -> fprintf fmt "return %a;" (print_expr ~paren:true) e
432 433 434

  and print_def fmt = function
    | Dfun (id,(rt,args),body) ->
435 436 437 438 439 440 441 442 443 444
       fprintf fmt "%a %a(@[%a@])@ @[<hv>{@;<1 2>@[<hv>%a@]@;}@;@]"
               (print_ty ~paren:false) rt
               print_ident id
               (print_list comma
			   (print_pair_delim nothing space nothing
					     (print_ty ~paren:false) print_ident))
	       args
               print_body body
    | Dproto (id, (rt, args)) ->
      fprintf fmt "%a %a(@[%a@]);@;"
445 446 447
        (print_ty ~paren:false) rt
        print_ident id
        (print_list comma
448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
           (print_pair_delim nothing space nothing
			     (print_ty ~paren:false) print_ident))
	args
    | Ddecl (ty, lie) ->
       fprintf fmt "%a @[<hov>%a@];@;"
	       (print_ty ~paren:false) ty
	       (print_list comma print_id_init) lie
    | Dinclude id ->
       fprintf fmt "#include<%a>@;" print_ident id
    | Dtypedef (ty,id) ->
       fprintf fmt "@[<hov>typedef@ %a@;%a;@]@;"
	       (print_ty ~paren:false) ty print_ident id

  and print_body fmt body =
    print_pair_delim nothing newline nothing
		     (print_list newline print_def)
		     print_stmt
		     fmt body

  let print_file fmt = fprintf fmt "@[<v>%a@]@." (print_list newline print_def)
468 469 470 471


end

472 473 474 475 476 477 478 479
let fg ?fname m =
  let n = m.Pmodule.mod_theory.Theory.th_name.Ident.id_string in
  match fname with
  | None -> n ^ ".c"
  | Some f -> f ^ "__" ^ n ^ ".c"

let pr args ?old fmt m =
  ignore(old);
480 481 482 483
  let ast = Translate.translate args m in
  try Print.print_file fmt ast
  with Print.Unprinted s -> (Format.printf "Could not print: %s@." s;
		       Format.fprintf fmt "/* Dummy file */@.")
484 485

let () = Pdriver.register_printer "c" ~desc:"printer for C code" fg pr