From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/LTLintyping.v | 122 --------------------------------------------------
 1 file changed, 122 deletions(-)
 delete mode 100644 backend/LTLintyping.v

(limited to 'backend/LTLintyping.v')

diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
deleted file mode 100644
index 0338667b..00000000
--- a/backend/LTLintyping.v
+++ /dev/null
@@ -1,122 +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 INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Typing rules for LTLin. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
-Require Import Locations.
-Require Import LTLin.
-Require LTLtyping.
-Require Import Conventions.
-
-(** The following predicates define a type system for LTLin similar to that
-  of LTL. *)
-
-Section WT_INSTR.
-
-Variable funsig: signature.
-
-Inductive wt_instr : instruction -> Prop :=
-  | wt_Lopmove:
-      forall r1 r,
-      Loc.type r1 = Loc.type r -> loc_acceptable r1 -> loc_acceptable r ->
-      wt_instr (Lop Omove (r1 :: nil) r)
-  | wt_Lop:
-      forall op args res,
-      op <> Omove ->
-      (List.map Loc.type args, Loc.type res) = type_of_operation op ->
-      locs_acceptable args -> loc_acceptable res ->
-      wt_instr (Lop op args res)
-  | wt_Lload:
-      forall chunk addr args dst,
-      List.map Loc.type args = type_of_addressing addr ->
-      Loc.type dst = type_of_chunk chunk ->
-      locs_acceptable args -> loc_acceptable dst ->
-      wt_instr (Lload chunk addr args dst)
-  | wt_Lstore:
-      forall chunk addr args src,
-      List.map Loc.type args = type_of_addressing addr ->
-      Loc.type src = type_of_chunk chunk ->
-      locs_acceptable args -> loc_acceptable src ->
-      wt_instr (Lstore chunk addr args src)
-  | wt_Lcall:
-      forall sig ros args res,
-      List.map Loc.type args = sig.(sig_args) ->
-      Loc.type res = proj_sig_res sig ->
-      LTLtyping.call_loc_acceptable sig ros ->
-      locs_acceptable args -> loc_acceptable res ->
-      wt_instr (Lcall sig ros args res)
-  | wt_Ltailcall:
-      forall sig ros args,
-      List.map Loc.type args = sig.(sig_args) ->
-      LTLtyping.call_loc_acceptable sig ros ->
-      locs_acceptable args -> 
-      sig.(sig_res) = funsig.(sig_res) ->
-      tailcall_possible sig ->
-      wt_instr (Ltailcall sig ros args)
-  | wt_Lbuiltin:
-      forall ef args res,
-      List.map Loc.type args = (ef_sig ef).(sig_args) ->
-      Loc.type res = proj_sig_res (ef_sig ef) ->
-      arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
-      locs_acceptable args -> loc_acceptable res ->
-       wt_instr (Lbuiltin ef args res)
-  | wt_Llabel: forall lbl,
-      wt_instr (Llabel lbl)
-  | wt_Lgoto: forall lbl,
-      wt_instr (Lgoto lbl)
-  | wt_Lcond:
-      forall cond args lbl,
-      List.map Loc.type args = type_of_condition cond ->
-      locs_acceptable args ->
-      wt_instr (Lcond cond args lbl)
-  | wt_Ljumptable:
-      forall arg tbl,
-      Loc.type arg = Tint ->
-      loc_acceptable arg ->
-      list_length_z tbl * 4 <= Int.max_unsigned ->
-      wt_instr (Ljumptable arg tbl)
-  | wt_Lreturn: 
-      forall optres,
-      option_map Loc.type optres = funsig.(sig_res) ->
-      match optres with None => True | Some r => loc_acceptable r end ->
-      wt_instr (Lreturn optres).
-
-Definition wt_code (c: code) : Prop :=
-  forall i, In i c -> wt_instr i.
-
-End WT_INSTR.
-
-Record wt_function (f: function): Prop :=
-  mk_wt_function {
-    wt_params:
-      List.map Loc.type f.(fn_params) = f.(fn_sig).(sig_args);
-    wt_acceptable:
-      locs_acceptable f.(fn_params);
-    wt_norepet:
-      Loc.norepet f.(fn_params);
-    wt_instrs:
-      wt_code f.(fn_sig) f.(fn_code)
-}.
-
-Inductive wt_fundef: fundef -> Prop :=
-  | wt_fundef_external: forall ef,
-      wt_fundef (External ef)
-  | wt_function_internal: forall f,
-      wt_function f ->
-      wt_fundef (Internal f).
-
-Definition wt_program (p: program): Prop :=
-  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.
-- 
cgit