plugins/microc/mc_main.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Why3
  13 open Pmodule
  14 open Mc_ast
  15 open Ptree
  16 open Wstdlib
  17
  18 let debug = Debug.register_flag "micro-C"
  19   ~desc:"micro-C plugin debug flag"
  20
  21 let mk_id ~loc name =
  22   { id_str = name; id_ats = []; id_loc = loc }
  23
  24 let infix  ~loc s = Qident (mk_id ~loc (Ident.op_infix s))
  25 let prefix ~loc s = Qident (mk_id ~loc (Ident.op_prefix s))
  26 let get_op ~loc   = Qident (mk_id ~loc (Ident.op_get ""))
  27 let set_op ~loc   = Qident (mk_id ~loc (Ident.op_set ""))
  28
  29 let mk_expr ~loc d =
  30   { expr_desc = d; expr_loc = loc }
  31 let mk_pat ~loc d =
  32   { pat_desc = d; pat_loc = loc }
  33 let mk_unit ~loc =
  34   mk_expr ~loc (Etuple [])
  35 let mk_var ~loc id =
  36   mk_expr ~loc (Eident (Qident id))
  37 let mk_ref ~loc e =
  38   mk_expr ~loc (Eidapp (Qident (mk_id ~loc "ref"), [e]))
  39 let array_set ~loc a i v =
  40   mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
  41 let constant ~loc i =
  42   mk_expr ~loc (Econst (Constant.int_const_of_int i))
  43 let constant_s ~loc s =
  44   let int_lit = Number.(int_literal ILitDec ~neg:false s) in
  45   mk_expr ~loc (Econst (Constant.ConstInt int_lit))
  46 let break ~loc =
  47   Qident (mk_id ~loc "Break")
  48 let break_handler ~loc =
  49   [break ~loc, None, mk_unit ~loc]
  50 let return ~loc =
  51   Qident (mk_id ~loc "Return")
  52 let return_handler ~loc =
  53   let x = mk_id ~loc "x" in
  54   [return ~loc, Some (mk_pat ~loc (Pvar x)), mk_var ~loc x]
  55 let array_id ~loc id = Qdot (Qident (mk_id ~loc "Array"), id)
  56
  57 let set_ref id =
  58   { id with id_ats = ATstr Pmodule.ref_attr :: id.id_ats }
  59
  60 type env = {
  61   vars: ident Mstr.t;
  62 }
  63
  64 let empty_env =
  65   { vars = Mstr.empty }
  66
  67 let add_var env (_, id) =
  68   { vars = Mstr.add id.id_str id env.vars }
  69
  70 let rec has_stmt p s =
  71   p s || begin match s.stmt_desc with
  72     | Sskip | Sbreak  | Sreturn _ | Svar _ | Sassign _ | Slabel _
  73     | Seval _ | Sset _ | Sassert _ -> false
  74     | Sif (_, s1, s2) -> has_stmt p s1 || has_stmt p s2
  75     | Swhile (_, _, s) -> has_stmt p s
  76     | Sblock sl -> has_stmtl p sl end
  77 and has_stmtl p bl = List.exists (has_stmt p) bl
  78
  79 let has_break = has_stmt (fun s -> s.stmt_desc = Sbreak)
  80 let has_return = has_stmt (function { stmt_desc = Sreturn _ } -> true | _ -> false)
  81
  82 let rec expr_has_call id e = match e.Mc_ast.expr_desc with
  83   | Eunit | Eint _ | Estring _ | Eaddr _ | Mc_ast.Eident _ -> false
  84   | Eget (e1, e2) | Ebinop (_, e1, e2) ->
  85     expr_has_call id e1 || expr_has_call id e2
  86   | Eunop (_, e1) -> expr_has_call id e1
  87   | Ecall (f, el) -> id.id_str = f.id_str || List.exists (expr_has_call id) el
  88
  89 let rec stmt_has_call id s = match s.stmt_desc with
  90   | Sskip | Sbreak | Slabel _ | Sassert _ -> false
  91   | Sreturn e | Svar (_, _, e) | Sassign (_, e) | Seval e -> expr_has_call id e
  92   | Sset (e1, e2, e3) ->
  93     expr_has_call id e1 || expr_has_call id e2 || expr_has_call id e3
  94   | Sif (e, s1, s2) -> expr_has_call id e || stmt_has_call id s1 || stmt_has_call id s2
  95   | Swhile (e, _, s) -> expr_has_call id e || stmt_has_call id s
  96   | Sblock bl -> block_has_call id bl
  97 and block_has_call id = has_stmtl (stmt_has_call id)
  98
  99 let rec expr env ({Mc_ast.expr_loc = loc; Mc_ast.expr_desc = d } as e) =
 100   match d with
 101   | Mc_ast.Eunit ->
 102     mk_unit ~loc
 103   | Mc_ast.Eint s ->
 104     constant_s ~loc s
 105   | Mc_ast.Estring _s ->
 106     mk_unit ~loc (*FIXME*)
 107   | Mc_ast.Eaddr id | Mc_ast.Eident id
 108     when not (Mstr.mem id.id_str env.vars) ->
 109      Loc.errorm ~loc "unbound variable %s" id.id_str
 110   | Mc_ast.Eaddr id ->
 111      mk_expr ~loc (Eident (Qident id))
 112   | Mc_ast.Eident id ->
 113     if not (Mstr.mem id.id_str env.vars) then
 114       Loc.errorm ~loc "unbound variable %s" id.id_str;
 115     mk_expr ~loc (Eident (Qident id))
 116   | Mc_ast.Ebinop (Mc_ast.Badd | Mc_ast.Bsub | Mc_ast.Bmul |
 117                    Mc_ast.Bdiv | Mc_ast.Bmod as op, e1, e2) ->
 118     let e1 = expr env e1 in
 119     let e2 = expr env e2 in
 120     mk_expr ~loc (match op with
 121       | Mc_ast.Badd -> Eidapp (infix ~loc "+", [e1; e2])
 122       | Mc_ast.Bsub -> Eidapp (infix ~loc "-", [e1; e2])
 123       | Mc_ast.Bmul -> Eidapp (infix ~loc "*", [e1; e2])
 124       | Mc_ast.Bdiv -> Eidapp (infix ~loc "/", [e1; e2])
 125       | Mc_ast.Bmod -> Eidapp (infix ~loc "%", [e1; e2])
 126       | _ -> assert false)
 127   | Mc_ast.Ebinop _ | Mc_ast.Eunop (Mc_ast.Unot, _) ->
 128      mk_expr ~loc (Eif (bool env e, constant ~loc 1, constant ~loc 0))
 129   | Mc_ast.Eunop (Mc_ast.Uneg, e) ->
 130     mk_expr ~loc (Eidapp (prefix ~loc "-", [expr env e]))
 131   | Mc_ast.Ecall ({id_str = "printf"}, el) ->
 132      let el = match el with
 133        | {Mc_ast.expr_desc=Estring _} :: el -> el
 134        | _ :: _ -> Loc.errorm ~loc "first argument of printf must be a string"
 135        | [] -> Loc.errorm ~loc "two few arguments to function printf" in
 136     let eval res e =
 137       mk_expr ~loc
 138         (Elet (mk_id ~loc "_", false, Expr.RKnone, expr env e, res)) in
 139     List.fold_left eval (mk_unit ~loc) el
 140   | Mc_ast.Ecall (id, el) ->
 141      let el = if el = [] then [mk_unit ~loc] else List.map (expr env) el in
 142      mk_expr ~loc (Eidapp (Qident id, el))
 143   | Mc_ast.Eget (e1, e2) ->
 144     mk_expr ~loc (Eidapp (get_op ~loc, [expr env e1; expr env e2]))
 145
 146 and bool env ({Mc_ast.expr_loc = loc; Mc_ast.expr_desc = d } as e) =
 147   match d with
 148   | Mc_ast.Ebinop (Mc_ast.Band | Mc_ast.Bor as op, e1, e2) ->
 149     let e1 = bool env e1 in
 150     let e2 = bool env e2 in
 151     mk_expr ~loc (match op with
 152       | Mc_ast.Band -> Eand (e1, e2)
 153       | Mc_ast.Bor  -> Eor  (e1, e2)
 154       | _ -> assert false)
 155   | Mc_ast.Ebinop (Mc_ast.Beq | Mc_ast.Bneq | Mc_ast.Blt |
 156                    Mc_ast.Ble | Mc_ast.Bgt | Mc_ast.Bge as op, e1, e2) ->
 157     let e1 = expr env e1 in
 158     let e2 = expr env e2 in
 159     mk_expr ~loc (match op with
 160       | Mc_ast.Beq  -> Eidapp (infix ~loc "=", [e1; e2])
 161       | Mc_ast.Bneq ->
 162          Enot (mk_expr ~loc (Eidapp (infix ~loc "=", [e1; e2])))
 163       | Mc_ast.Blt  -> Eidapp (infix ~loc "<", [e1; e2])
 164       | Mc_ast.Ble  -> Eidapp (infix ~loc "<=", [e1; e2])
 165       | Mc_ast.Bgt  -> Eidapp (infix ~loc ">", [e1; e2])
 166       | Mc_ast.Bge  -> Eidapp (infix ~loc ">=", [e1; e2])
 167       | _ -> assert false)
 168   | Mc_ast.Eunop (Mc_ast.Unot, e) ->
 169     mk_expr ~loc (Enot (bool env e))
 170   | _ ->
 171      let e = Eidapp (infix ~loc "=", [expr env e; constant ~loc 0]) in
 172      mk_expr ~loc (Enot (mk_expr ~loc e))
 173
 174 let no_params ~loc = [loc, None, false, Some (PTtuple [])]
 175
 176 let rec stmt env {Mc_ast.stmt_loc = loc; Mc_ast.stmt_desc = d } =
 177   match d with
 178   | Mc_ast.Sskip ->
 179     mk_unit ~loc
 180   | Mc_ast.Seval e ->
 181      let dummy = mk_id ~loc "_" in
 182      mk_expr ~loc (Elet (dummy, false, Expr.RKnone, expr env e, mk_unit ~loc))
 183   | Mc_ast.Sif (e, s1, s2) ->
 184     mk_expr ~loc (Eif (bool env e, stmt env s1, stmt env s2))
 185   | Mc_ast.Sreturn e ->
 186     mk_expr ~loc (Eraise (return ~loc, Some (expr env e)))
 187   | Mc_ast.Svar _ ->
 188      assert false
 189   | Mc_ast.Sassign (id, _)
 190     when not (Mstr.mem id.id_str env.vars) ->
 191      Loc.errorm ~loc "unbound variable %s" id.id_str
 192   | Mc_ast.Sassign (id, e) ->
 193     let e = expr env e in
 194     let x = let loc = id.id_loc in mk_expr ~loc (Eident (Qident id)) in
 195     mk_expr ~loc (Einfix (x, mk_id ~loc (Ident.op_infix ":="), e))
 196   | Mc_ast.Sset (e1, e2, e3) ->
 197     array_set ~loc (expr env e1) (expr env e2) (expr env e3)
 198   | Mc_ast.Sassert (k, t) ->
 199     mk_expr ~loc (Eassert (k, t))
 200   | Mc_ast.Swhile (e, (inv, var), s) ->
 201     let loop = mk_expr ~loc
 202       (Ewhile (bool env e, inv, var, stmt env s)) in
 203     if has_break s then mk_expr ~loc (Ematch (loop, [], break_handler ~loc))
 204     else loop
 205   | Mc_ast.Sbreak ->
 206     mk_expr ~loc (Eraise (break ~loc, None))
 207   | Mc_ast.Slabel _ ->
 208     mk_unit ~loc (* ignore lonely marks *)
 209   | Mc_ast.Sblock bl ->
 210      block env ~loc bl
 211
 212 and block env ~loc = function
 213   | [] ->
 214     mk_unit ~loc
 215   | { stmt_loc = loc; stmt_desc = Slabel id } :: sl ->
 216     mk_expr ~loc (Elabel (id, block env ~loc sl))
 217   | { Mc_ast.stmt_loc = loc; stmt_desc = Mc_ast.Svar (ty, id, e) } :: sl ->
 218     let e = expr env e in (* check e *before* adding id to environment *)
 219     let env = add_var env (ty, id) in
 220     let ee = mk_ref ~loc e in
 221     mk_expr ~loc (Elet (set_ref id, false, Expr.RKnone, ee, block env ~loc sl))
 222   | ({ Mc_ast.stmt_loc = loc } as s) :: sl ->
 223     let s = stmt env s in
 224     if sl = [] then s else mk_expr ~loc (Esequence (s, block env ~loc sl))
 225
 226 let type_unit loc = PTtyapp (Qident (mk_id ~loc "unit"), [])
 227 let type_int loc = PTtyapp (Qident (mk_id ~loc "int"), [])
 228 let type_array loc ty = PTtyapp (array_id ~loc (mk_id ~loc "array"), [ty])
 229
 230 let type_ loc = function
 231   | Tvoid -> type_unit loc
 232   | Tint -> type_int loc
 233   | Tarray -> type_array loc (type_int loc)
 234
 235 let logic_param (ty, id) =
 236   id.id_loc, Some id, false, type_ id.id_loc ty
 237
 238 let decl = function
 239   | Mc_ast.Dinclude _ ->
 240      ()
 241   | Mc_ast.Dfun (ty, id, idl, sp, bl) ->
 242     (* f(x1,...,xn): body ==>
 243       let f x1 ... xn =
 244         let x1 = ref x1 in ... let xn = ref xn in
 245         try body with Return x -> x *)
 246     let loc = id.id_loc in
 247     let rty = type_ loc ty in
 248     let env' = List.fold_left add_var empty_env idl in
 249     let body = stmt env' bl in
 250     let body =
 251       if not (has_return bl) then begin
 252         if ty <> Tvoid then Loc.errorm ~loc "missing return";
 253         body end else
 254       mk_expr ~loc (Ematch (body, [], return_handler ~loc)) in
 255     let local bl = function
 256       | Tint, id ->
 257         let loc = id.id_loc in
 258         let ref = mk_ref ~loc (mk_var ~loc id) in
 259         mk_expr ~loc (Elet (set_ref id, false, Expr.RKnone, ref, bl))
 260       | Tarray, _ -> bl
 261       | Tvoid, _ -> assert false in
 262     let body = List.fold_left local body idl in
 263     let param (ty, id) =
 264       id.id_loc, Some id, false, Some (type_ id.id_loc ty) in
 265     let params = if idl = [] then no_params ~loc else List.map param idl in
 266     let p = mk_pat ~loc Pwild in
 267     let d = if stmt_has_call id bl then
 268       Drec ([id, false, Expr.RKnone, params, Some rty,
 269              p, Ity.MaskVisible, sp, body])
 270     else
 271       let e = Efun (params, Some rty, p, Ity.MaskVisible, sp, body) in
 272       Dlet (id, false, Expr.RKnone, mk_expr ~loc e) in
 273     Typing.add_decl loc d
 274   | Mc_ast.Dlogic (ty, id, idl, def) ->
 275     let d = { ld_loc = id.id_loc;
 276               ld_ident = id;
 277               ld_params = List.map logic_param idl;
 278               ld_type = Option.map (type_ id.id_loc) ty;
 279               ld_def = def } in
 280     Typing.add_decl id.id_loc (Dlogic [d])
 281   | Mc_ast.Dprop (pk, id, t) ->
 282      Typing.add_decl id.id_loc (Dprop (pk, id, t))
 283
 284 let translate dl =
 285   List.iter decl dl
 286
 287 let read_channel env path file c =
 288   let f : Mc_ast.file = Mc_lexer.parse file c in
 289   Debug.dprintf debug "%s parsed successfully.@." file;
 290   let file = Filename.basename file in
 291   let file = Filename.chop_extension file in
 292   let name = Strings.capitalize file in
 293   Debug.dprintf debug "building module %s.@." name;
 294   Typing.open_file env path;
 295   let loc = Loc.user_position file 0 0 0 0 in
 296   Typing.open_module (mk_id ~loc name);
 297   let use_import (f, m) =
 298     let m = mk_id ~loc m in
 299     let qid = Qdot (Qident (mk_id ~loc f), m) in
 300     let decl = Ptree.Duseimport(loc,false,[(qid,None)]) in
 301     Typing.add_decl loc decl in
 302   List.iter use_import
 303     ["int", "Int"; "ref", "Refint"; "microc", "MicroC"];
 304   translate f;
 305   Typing.close_module loc;
 306   let mm = Typing.close_file () in
 307   if path = [] && Debug.test_flag debug then begin
 308     let add_m _ m modm = Ident.Mid.add m.mod_theory.Theory.th_name m modm in
 309     let print_m _ m = Pmodule.print_module Format.err_formatter m in
 310     Ident.Mid.iter print_m (Mstr.fold add_m mm Ident.Mid.empty)
 311   end;
 312   mm
 313
 314 let () =
 315   Env.register_format mlw_language "micro-C" ["c"] read_channel
 316     ~desc:"micro-C format"
 317
 318 (* Add an extension of task printing *)
 319 let () = Itp_server.add_registered_lang "micro-C"
 320     (fun _ -> Mc_printer.microc_ext_printer)
 321
 322 (* Add transformation arguments parsing *)
 323 let () = Args_wrapper.set_argument_parsing_functions "micro-C"
 324     ~parse_term:(fun _ lb -> Mc_lexer.parse_term lb)
 325     ~parse_term_list:(fun _ lb -> Mc_lexer.parse_term_list lb)
 326     ~parse_list_ident:(fun lb -> Mc_lexer.parse_list_ident lb)
 327     (* TODO for qualids, add a similar funciton *)
 328     ~parse_qualid:(fun lb -> Lexer.parse_qualid lb)
 329     ~parse_list_qualid:(fun lb -> Lexer.parse_list_qualid lb)