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

3 4 5
exception Unsupported of string
exception NoSyntax of string

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

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  type ty =
    | Tvoid
    | Tsyntax of string (* ints, floats, doubles, chars are here *)
    | Tptr of ty
    | Tarray of ty * expr
    | Tstruct of ident * (ident * ty) list
    | Tunion of ident * (ident * ty) list
    | Tproto of proto
    | Tnamed of ident (* alias from typedef *)
    (* 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
    | Eternary of expr * expr * expr (* c ? then : else *)
    | Ecast of ty * expr
    | Ecall of expr * expr list
    | Econst of constant
40
    | Evar of ident
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
41 42 43
    | Esize_expr of expr
    | Esize_type of ty
    | Eindex of expr * expr (* Array access *)
44 45
    | Edot of expr * ident (* Field access with dot *)
    | Earrow of expr * ident (* Pointer access with arrow *)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65

  and constant =
    | Cint of string
    | Cfloat of string
    | Cchar of string
    | Cstring of string
    | Ccompound of expr list

  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 =
66
    | Dfun of ident * proto * body
67
    | Dinclude of ident
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
68 69 70 71 72 73 74 75
    | Ddecl of names
    | Dtypedef of ty * ident
    | Dstructural of names (* struct, union... *)

  and body = definition list * stmt

  type file = definition list

76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
  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

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 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 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
  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)
    | Eternary (c,t,e) -> Eternary (propagate_in_expr id v c,
                                    propagate_in_expr id v t,
                                    propagate_in_expr id v e)
    | 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)
    | 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")
    | Dtypedef _ -> raise (Unsupported "typedef inside body")
    | Dstructural (ty,l) ->
      let l,b = aux l in
      Dstructural (ty, l), b

  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)


161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
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
179
  open Pmodule
180 181 182 183 184 185 186 187 188 189 190 191 192

  let ty_of_ty info ty =
    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
    | Tyapp (ts, _tl) ->
       begin match query_syntax info.syntax ts.ts_name
        with
        | Some s -> C.Tsyntax s (*TODO something with the %[tv][1-9] logic ?*)
193
        | None -> raise (NoSyntax ts.ts_name.id_string)
194 195 196 197 198 199
       end

  let ty_of_ts info ts =
    match query_syntax info.syntax ts.ts_name
        with
        | Some s -> C.Tsyntax s (*TODO something with the %[tv][1-9] logic ?*)
200
        | None -> raise (NoSyntax ts.ts_name.id_string)
201 202 203 204 205 206 207 208

  let ty_of_ity info ity =
    match ity.ity_node with
    | Ityvar (tv,_) ->
      begin match query_syntax info.syntax tv.tv_name with
      | Some s -> C.Tsyntax s
      | None -> C.Tnamed (tv.tv_name)
      end
209
    | Ityapp (its,_,_) | Ityreg {reg_its=its} -> ty_of_ts info its.its_ts
210 211 212 213 214 215

  let pv_name pv = pv.pv_vs.vs_name

  let rec expr info (e:expr) : C.body =
    match e.e_node with
    | Evar pv -> C.([], Sexpr(Evar (pv_name pv)))
216 217 218 219 220
    | Econst (Number.ConstInt ic) ->
      let n = Number.compute_int ic in
      C.([], Sexpr(Econst (Cint (BigInt.to_string n))))
    | Econst _ -> assert false (*TODO*)
    | Eexec (ce, _cty) ->
221 222 223 224 225 226 227 228 229 230 231 232 233
      begin match ce.c_node with
      | Cfun e -> expr info e
      | Capp (rs, pvsl) ->
        let args = List.filter (fun pv -> not pv.pv_ghost) pvsl in
        C.([],
           Sexpr(Ecall(Evar(rs.rs_name),
                       List.map (fun pv -> Evar(pv_name pv)) args)))
      | _ -> assert false
      end
    | Eassign _ -> assert false
    | 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 e
236 237 238 239 240 241 242 243 244 245 246 247 248 249
        else if ((pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit)
        then ([], C.Sseq (C.Sblock(expr info le), C.Sblock(expr info e)))
        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
            C.propagate_in_block (pv_name pv) cexp (expr info e)
          | _->
            let t = ty_of_ity info pv.pv_ity in
            let initblock = expr info le in
            [ C.Ddecl (t, [pv_name pv, C.Enothing]) ],
            C.Sseq (C.Sblock initblock, C.Sblock (expr info e))
        end
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
      | _ -> assert false
      end
    | Eif (c, t, e) ->
      let t = expr info t in
      let e = expr info e in
      begin match expr info c with
      | [], C.Sexpr c -> [], C.Sif(c,C.Sblock t, C.Sblock e)
      | cblock ->
        let cid = id_register (id_fresh "cond") in (* ? *)
        [ C.Ddecl (C.Tsyntax "int", [cid, C.Enothing]) ],
        C.Sseq (C.Sblock cblock, C.Sif (C.Evar cid, C.Sblock t, C.Sblock e))
      end
    | Ewhile (c,_,_,e) ->
      let cd, cs = expr info c in
      let b = expr info e in
      begin match cs with
      | C.Sexpr ce -> cd, C.Swhile (ce, C.Sblock b)
      | _ ->
        let cid = id_register (id_fresh "cond") in (* ? *)
        [C.Ddecl (C.Tsyntax "int", [cid, C.Enothing])],
        C.Sseq (C.Sblock (cd, cs), C.Swhile (C.Evar cid, C.Sblock b))
      end
272
    | Etry _ | Eraise _ -> raise (Unsupported "try/exceptions") (*TODO*)
273 274 275 276 277 278 279
    | Efor _ -> assert false (*TODO*)
    | Eassert _ -> [], C.Snop
    | Eghost _ | Epure _ | Ecase _ | Eabsurd -> assert false

  let pdecl info (pd:Pdecl.pdecl) : C.definition list =
    match pd.pd_node with
    | PDlet (LDsym (rs, ce)) ->
280 281 282 283 284
      let fname = rs.rs_name in
      Format.printf "PDlet rsymbol %s@." fname.id_string;
      begin try
        if Mid.mem fname info.syntax then []
        else
285 286
        let params = List.map
          (fun pv -> ty_of_ty info pv.pv_vs.vs_ty, pv_name pv)
287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303
          (List.filter
             (fun pv -> not pv.pv_ghost && not (ity_equal pv.pv_ity ity_unit))
             rs.rs_cty.cty_args) in
        match ce.c_node with
        | Cfun e ->
          let rtype = match rs.rs_cty.cty_result.ity_node with
            | Ityapp (its, _,_) ->
              ty_of_ts info its.its_ts
            | _ ->
              raise (Unsupported "variable return type")
          in
          [C.Dfun (fname, (rtype,params), expr info e)]
        | _ -> raise (Unsupported "Non-function with no syntax in toplevel let")
        with
          NoSyntax s ->
            Format.printf "%s has no syntax : not extracted@." s;
            []
304 305 306
      end
    | PDtype [{itd_its = ity}] ->
      let id = ity.its_ts.ts_name in
307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337
      Format.printf "PDtype %s@." id.id_string;
      let def =
        match ity.its_ts.ts_def with
        | Some def -> ty_of_ty info def
        | None ->
          begin match query_syntax info.syntax id with
          | Some s -> C.Tsyntax s
          | None ->
            raise (Unsupported "type declaration without syntax or alias")
          end
      in
      [C.Dtypedef (def, id)]
    | _ -> [] (*TODO exn ? *)


  let munit info = function
    | Udecl pd -> pdecl info pd
    | Uuse _ -> []
    | 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; []
    | NoSyntax s ->
      Format.printf "Failed because %s has no syntax@." s; []
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
338
end
339 340 341 342 343 344 345 346 347 348 349

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"

open Format

let pr args ?old fmt m =
  ignore(old);
350
  let _ast = Translate.translate args m in
351 352 353 354
  (* TODO:
    iterer sur m.mod_units la fonction pr_unit
   *)

355 356 357 358 359 360 361 362 363
  fprintf fmt "#include <stdio.h>\n\
\n\
int main() {\n\
  printf \"Extraction from WhyML to C not yet implemented\\n\";\n\
  return 1;\n\
}\n\
"

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