Merge pull request #170 from AbsInt/remove_cminor

Remove CompCert's ability to parse and compile source files written in Cminor

This facility is no longer used (as far as we know) and is painful to maintain.

1 files changed, 0 insertions, 350 deletions

diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
deleted file mode 100644
index cd0d25dc..00000000
--- a/backend/CMtypecheck.ml
+++ /dev/null
@@ -1,350 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* A type-checker for Cminor *)
-
-(* FIXME: proper support for type Tsingle *)
-
-open Printf
-open Camlcoq
-open AST
-open PrintAST
-open Cminor
-
-exception Error of string
-
-type ty = Base of typ | Var of ty option ref
-
-let newvar () = Var (ref None)
-let tint = Base Tint
-let tfloat = Base Tfloat
-let tlong = Base Tlong
-let tsingle = Base Tsingle
-let tany32 = Base Tany32
-let tany64 = Base Tany64
-
-let ty_of_typ = function
-  | Tint -> tint
-  | Tfloat -> tfloat
-  | Tlong -> tlong
-  | Tsingle -> tsingle
-  | Tany32 -> tany32
-  | Tany64 -> tany64
-
-let ty_of_sig_args tyl = List.map ty_of_typ tyl
-
-let rec repr t =
-  match t with
-  | Base _ -> t
-  | Var r -> match !r with None -> t | Some t' -> repr t'
-
-let unify t1 t2 =
-  match (repr t1, repr t2) with
-  | Base b1, Base b2 ->
-      if b1 <> b2 then
-        raise (Error (sprintf "Expected type %s, actual type %s\n"
-                              (name_of_type b1) (name_of_type b2)))
-  | Base b, Var r -> r := Some (Base b)
-  | Var r, Base b -> r := Some (Base b)
-  | Var r1, Var r2 -> if r1 != r2 then r1 := Some (Var r2)
-
-let unify_list l1 l2 =
-  let ll1 = List.length l1 and ll2 = List.length l2 in
-  if ll1 <> ll2 then
-    raise (Error (sprintf "Arity mismatch: expected %d, actual %d\n" ll1 ll2));
-  List.iter2 unify l1 l2
-
-let type_var env id =
-  try
-    List.assoc id env
-  with Not_found ->
-    raise (Error (sprintf "Unbound variable %s\n" (extern_atom id)))
-
-let type_constant = function
-  | Ointconst _ -> tint
-  | Ofloatconst _ -> tfloat
-  | Osingleconst _ -> tsingle
-  | Olongconst _ -> tlong
-  | Oaddrsymbol _ -> tint
-  | Oaddrstack _ -> tint
-
-let type_unary_operation = function
-  | Ocast8signed -> tint, tint
-  | Ocast16signed -> tint, tint
-  | Ocast8unsigned -> tint, tint
-  | Ocast16unsigned -> tint, tint
-  | Onegint -> tint, tint
-  | Onotint -> tint, tint
-  | Onegf -> tfloat, tfloat
-  | Oabsf -> tfloat, tfloat
-  | Onegfs -> tsingle, tsingle
-  | Oabsfs -> tsingle, tsingle
-  | Osingleoffloat -> tfloat, tsingle
-  | Ofloatofsingle -> tsingle, tfloat
-  | Ointoffloat -> tfloat, tint
-  | Ointuoffloat -> tfloat, tint
-  | Ofloatofint -> tint, tfloat
-  | Ofloatofintu -> tint, tfloat
-  | Ointofsingle -> tsingle, tint
-  | Ointuofsingle -> tsingle, tint
-  | Osingleofint -> tint, tsingle
-  | Osingleofintu -> tint, tsingle
-  | Onegl -> tlong, tlong
-  | Onotl -> tlong, tlong
-  | Ointoflong -> tlong, tint
-  | Olongofint -> tint, tlong
-  | Olongofintu -> tint, tlong
-  | Olongoffloat -> tfloat, tlong
-  | Olonguoffloat -> tfloat, tlong
-  | Ofloatoflong -> tlong, tfloat
-  | Ofloatoflongu -> tlong, tfloat
-  | Olongofsingle -> tsingle, tlong
-  | Olonguofsingle -> tsingle, tlong
-  | Osingleoflong -> tlong, tfloat
-  | Osingleoflongu -> tlong, tfloat
-
-let type_binary_operation = function
-  | Oadd -> tint, tint, tint
-  | Osub -> tint, tint, tint
-  | Omul -> tint, tint, tint
-  | Odiv -> tint, tint, tint
-  | Odivu -> tint, tint, tint
-  | Omod -> tint, tint, tint
-  | Omodu -> tint, tint, tint
-  | Oand -> tint, tint, tint
-  | Oor -> tint, tint, tint
-  | Oxor -> tint, tint, tint
-  | Oshl -> tint, tint, tint
-  | Oshr -> tint, tint, tint
-  | Oshru -> tint, tint, tint
-  | Oaddf -> tfloat, tfloat, tfloat
-  | Osubf -> tfloat, tfloat, tfloat
-  | Omulf -> tfloat, tfloat, tfloat
-  | Odivf -> tfloat, tfloat, tfloat
-  | Oaddfs -> tsingle, tsingle, tsingle
-  | Osubfs -> tsingle, tsingle, tsingle
-  | Omulfs -> tsingle, tsingle, tsingle
-  | Odivfs -> tsingle, tsingle, tsingle
-  | Oaddl -> tlong, tlong, tlong
-  | Osubl -> tlong, tlong, tlong
-  | Omull -> tlong, tlong, tlong
-  | Odivl -> tlong, tlong, tlong
-  | Odivlu -> tlong, tlong, tlong
-  | Omodl -> tlong, tlong, tlong
-  | Omodlu -> tlong, tlong, tlong
-  | Oandl -> tlong, tlong, tlong
-  | Oorl -> tlong, tlong, tlong
-  | Oxorl -> tlong, tlong, tlong
-  | Oshll -> tlong, tint, tlong
-  | Oshrl -> tlong, tint, tlong
-  | Oshrlu -> tlong, tint, tlong
-  | Ocmp _ -> tint, tint, tint
-  | Ocmpu _ -> tint, tint, tint
-  | Ocmpf _ -> tfloat, tfloat, tint
-  | Ocmpfs _ -> tsingle, tsingle, tint
-  | Ocmpl _ -> tlong, tlong, tint
-  | Ocmplu _ -> tlong, tlong, tint
-
-let name_of_unary_operation = PrintCminor.name_of_unop
-
-let name_of_binary_operation = PrintCminor.name_of_binop
-
-let type_chunk = function
-  | Mint8signed -> tint
-  | Mint8unsigned -> tint
-  | Mint16signed -> tint
-  | Mint16unsigned -> tint
-  | Mint32 -> tint
-  | Mint64 -> tlong
-  | Mfloat32 -> tsingle
-  | Mfloat64 -> tfloat
-  | Many32 -> tany32
-  | Many64 -> tany64
-
-let name_of_chunk = PrintAST.name_of_chunk
-
-let rec type_expr env lenv e =
-  match e with
-  | Evar id ->
-      type_var env id
-  | Econst cst ->
-      type_constant cst
-  | Eunop(op, e1) ->
-      let te1 = type_expr env lenv e1 in
-      let (targ, tres) = type_unary_operation op in
-      begin try
-        unify targ te1
-      with Error s ->
-        raise (Error (sprintf "In application of operator %s:\n%s"
-                              (name_of_unary_operation op) s))
-      end;
-      tres
-  | Ebinop(op, e1, e2) ->
-      let te1 = type_expr env lenv e1 in
-      let te2 = type_expr env lenv e2 in
-      let (targ1, targ2, tres) = type_binary_operation op in
-      begin try
-        unify targ1 te1; unify targ2 te2
-      with Error s ->
-        raise (Error (sprintf "In application of operator %s:\n%s"
-                              (name_of_binary_operation op) s))
-      end;
-      tres
-  | Eload(chunk, e) ->
-      let te = type_expr env lenv e in
-      begin try
-        unify tint te
-      with Error s ->
-        raise (Error (sprintf "In load %s:\n%s"
-                              (name_of_chunk chunk) s))
-      end;
-      type_chunk chunk
-
-and type_exprlist env lenv el =
-  match el with
-  | [] -> []
-  | e1 :: et ->
-      let te1 = type_expr env lenv e1 in
-      let tet = type_exprlist env lenv et in
-      (te1 :: tet)
-
-and type_condexpr env lenv e =
-  let te = type_expr env lenv e in
-  begin try
-    unify tint te
-  with Error s ->
-    raise (Error (sprintf "In condition:\n%s" s))
-  end
-
-let rec type_stmt env blk ret s =
-  match s with
-  | Sskip -> ()
-  | Sassign(id, e1) ->
-      let tid = type_var env id in
-      let te1 = type_expr env [] e1 in
-      begin try
-        unify tid te1
-      with Error s ->
-        raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s))
-      end
-  | Sstore(chunk, e1, e2) ->
-      let te1 = type_expr env [] e1 in
-      let te2 = type_expr env [] e2 in
-      begin try
-        unify tint te1;
-        unify (type_chunk chunk) te2
-      with Error s ->
-        raise (Error (sprintf "In store %s:\n%s"
-                              (name_of_chunk chunk) s))
-      end
-  | Scall(optid, sg, e1, el) ->
-      let te1 = type_expr env [] e1 in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify tint te1;
-        unify_list (ty_of_sig_args sg.sig_args) tel;
-        let ty_res =
-          match sg.sig_res with
-          | None -> tint (*???*)
-          | Some t -> ty_of_typ t in
-        begin match optid with
-        | None -> ()
-        | Some id -> unify (type_var env id) ty_res
-        end
-      with Error s ->
-        raise (Error (sprintf "In call:\n%s" s))
-      end
-  | Sbuiltin(optid, ef, el) ->
-      let sg = ef_sig ef in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify_list (ty_of_sig_args sg.sig_args) tel;
-        let ty_res =
-          match sg.sig_res with
-          | None -> tint (*???*)
-          | Some t -> ty_of_typ t in
-        begin match optid with
-        | None -> ()
-        | Some id -> unify (type_var env id) ty_res
-        end
-      with Error s ->
-        raise (Error (sprintf "In builtin call:\n%s" s))
-      end
-  | Sseq(s1, s2) ->
-      type_stmt env blk ret s1;
-      type_stmt env blk ret s2
-  | Sifthenelse(ce, s1, s2) ->
-      type_condexpr env [] ce;
-      type_stmt env blk ret s1;
-      type_stmt env blk ret s2
-  | Sloop s1 ->
-      type_stmt env blk ret s1
-  | Sblock s1 ->
-      type_stmt env (blk + 1) ret s1
-  | Sexit n ->
-      if Nat.to_int n >= blk then
-        raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n)))
-  | Sswitch(islong, e, cases, deflt) ->
-      unify (type_expr env [] e) (if islong then tlong else tint)
-  | Sreturn None ->
-      begin match ret with
-      | None -> ()
-      | Some tret -> raise (Error ("return without argument"))
-      end
-  | Sreturn (Some e) ->
-      begin match ret with
-      | None -> raise (Error "return with argument")
-      | Some tret ->
-          begin try
-            unify (type_expr env [] e) (ty_of_typ tret)
-          with Error s ->
-            raise (Error (sprintf "In return:\n%s" s))
-          end
-      end
-  | Stailcall(sg, e1, el) ->
-      let te1 = type_expr env [] e1 in
-      let tel = type_exprlist env [] el in
-      begin try
-        unify tint te1;
-        unify_list (ty_of_sig_args sg.sig_args) tel
-      with Error s ->
-        raise (Error (sprintf "In tail call:\n%s" s))
-      end
-  | Slabel(lbl, s1) ->
-      type_stmt env blk ret s1
-  | Sgoto lbl ->
-      ()
-
-let rec env_of_vars idl =
-  match idl with
-  | [] -> []
-  | id1 :: idt -> (id1, newvar()) :: env_of_vars idt
-
-let type_function id f =
-  try
-    type_stmt
-       (env_of_vars f.fn_vars @ env_of_vars f.fn_params)
-       0 f.fn_sig.sig_res f.fn_body
-  with Error s ->
-    raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
-
-let type_globdef (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> type_function id f
-  | Gfun(External ef) -> ()
-  | Gvar v -> ()
-
-let type_program p =
-  List.iter type_globdef p.prog_defs; p