Type checking and preservation proof for LTL

Makefile

@@ -86,7 +86,8 @@ BACKEND=\
   CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
   NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
   Unusedglob.v Unusedglobproof.v \
-  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
+  Machregs.v Locations.v Conventions1.v Conventions.v \
+  LTL.v LTLtyping.v \
   Allocation.v Allocproof.v \
   Tunneling.v Tunnelingproof.v \
   Linear.v Lineartyping.v \

arm/Asm.v

@@ -323,11 +323,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
 
 (** Assigning the result of a builtin *)
 
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v)
   end.
 
 Section RELSEM.

arm/Asmexpand.ml

@@ -188,7 +188,7 @@ let expand_builtin_vload_common chunk base ofs res =
      emit (Pldrsh (res, base, SOimm ofs))
   | Mint32, BR(IR res) ->
      emit (Pldr (res, base, SOimm ofs))
-  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
+  | Mint64, BR_splitlong(IR res1, IR res2) ->
      let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
      let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
      if base <> res2 then begin
@@ -351,7 +351,7 @@ let expand_builtin_inline name args res =
      emit (Pfsqrt (res,a1))
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = ah ) rl (fun rl ->
         emit (Prsbs (rl,al,SOimm _0));
         (* No "rsc" instruction in Thumb2.  Emulate based on
@@ -365,20 +365,20 @@ let expand_builtin_inline name args res =
         end)
   | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 			(fun rl ->
 			 emit (Padds (rl,al,SOreg bl));
 			 emit (Padc (rh,ah,SOreg bh)))
   | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 		       (fun rl ->
 			emit (Psubs (rl,al,SOreg bl));
 			emit (Psbc (rh,ah,SOreg bh)))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      emit (Pumull (rl,rh,a,b))
   (* Memory accesses *)
   | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) ->

arm/Conventions1.v

@@ -16,6 +16,7 @@
 Require Import Coqlib.
 Require Import Decidableplus.
 Require Import AST.
+Require Import Values.
 Require Import Events.
 Require Import Locations.
 Require Archi.
@@ -122,6 +123,17 @@ Proof.
   intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
 Qed.
 
+Lemma loc_result_has_type:
+  forall res sig,
+  Val.has_type res (proj_sig_res sig) ->
+  Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type.
+Proof.
+  intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+  destruct sig; simpl. destruct sig_res; simpl in H.
+  destruct t, res, Archi.big_endian; simpl; auto.
+  destruct res; simpl; auto.
+Qed.
+
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:

arm/Op.v

@@ -557,6 +557,17 @@ Proof.
   intros; discriminate.
 Qed.
 
+Lemma is_not_move_operation:
+  forall (F V A: Type) (genv: Genv.t F V) (sp: val)
+         (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val),
+  eval_operation genv sp op (map f args) m = Some v ->
+  is_move_operation op args = None ->
+  op <> Omove.
+Proof.
+  intros. destruct (eq_operation op Omove); auto.
+  subst. destruct args; try destruct args; simpl in *; congruence.
+Qed.
+
 (** [negate_condition cond] returns a condition that is logically
   equivalent to the negation of [cond]. *)
 

backend/Allocation.v

@@ -16,7 +16,7 @@ Require Import FSets FSetAVLplus.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Lattice Kildall Memdata.
 Require Archi.
-Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
+Require Import Op Registers RTL Locations Conventions RTLtyping LTL LTLtyping.
 
 (** The validation algorithm used here is described in
   "Validating register allocation and spilling",
@@ -847,8 +847,10 @@ Definition remove_equations_builtin_res
     (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs :=
   match res, res' with
   | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e)
-  | BR r, BR_splitlong (BR rhi) (BR rlo) =>
+  | BR r, BR_splitlong rhi rlo =>
       assertion (typ_eq (env r) Tlong);
+      assertion (subtype Tint (mreg_type rhi));
+      assertion (subtype Tint (mreg_type rlo));
       if mreg_eq rhi rlo then None else
         Some (remove_equation (Eq Low r (R rlo))
                 (remove_equation (Eq High r (R rhi)) e))
@@ -932,12 +934,6 @@ Definition destroyed_by_move (src dst: loc) :=
   | _, _ => destroyed_by_op Omove
   end.
 
-Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool :=
-  match dst with
-  | R r => true
-  | S sl ofs ty => loc_type_compat env dst e
-  end.
-
 (** Simulate the effect of a sequence of moves [mv] on a set of
   equations [e].  The set [e] is the equations that must hold
   after the sequence of moves.  Return the set of equations that
@@ -950,7 +946,7 @@ Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs :=
   | MV src dst :: mv =>
       do e1 <- track_moves env mv e;
       assertion (can_undef_except dst (destroyed_by_move src dst)) e1;
-      assertion (well_typed_move env dst e1);
+      assertion (loc_type_compat env dst e1);
       subst_loc dst src e1
   | MVmakelong src1 src2 dst :: mv =>
       assertion (negb Archi.ptr64);
@@ -1359,7 +1355,11 @@ Definition transf_function (f: RTL.function) : res LTL.function :=
   | OK env =>
       match regalloc f with
       | Error m => Error m
-      | OK tf => do x <- check_function f tf env; OK tf
+      | OK tf =>
+          if wt_function tf then
+            do x <- check_function f tf env; OK tf
+          else
+            Error (msg "Ill-typed LTL code")
       end
   end.