aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE2.v6
-rw-r--r--backend/CSE2proof.v5
-rw-r--r--backend/CSE3.v2
-rw-r--r--backend/CSE3analysis.v8
-rw-r--r--backend/CSE3analysisproof.v44
-rw-r--r--backend/CSE3proof.v5
-rw-r--r--mppa_k1c/Asmblockgenproof1.v2
-rw-r--r--mppa_k1c/Asmvliw.v20
-rw-r--r--mppa_k1c/ConstpropOpproof.v6
-rw-r--r--mppa_k1c/Op.v118
-rw-r--r--mppa_k1c/SelectLongproof.v33
-rw-r--r--mppa_k1c/SelectOpproof.v40
-rw-r--r--mppa_k1c/ValueAOp.v314
-rw-r--r--test/c/Results/mandelbrot-mppa_k1cbin409 -> 209 bytes
-rw-r--r--test/monniaux/licm/addv.c6
15 files changed, 444 insertions, 165 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v
index 8e2307b0..00b1821e 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -276,10 +276,10 @@ Definition apply_external_call ef (rel : RELATION.t) : RELATION.t :=
| Some bf => rel
| None => kill_mem rel
end
- | EF_malloc (* FIXME *)
+ | EF_malloc (* would need lessdef *)
| EF_external _ _
| EF_vstore _
- | EF_free (* FIXME *)
+ | EF_free (* would need lessdef? *)
| EF_memcpy _ _ (* FIXME *)
| EF_inline_asm _ _ _ => kill_mem rel
| _ => rel
@@ -363,7 +363,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t))
| Some src => Iop Omove (src::nil) dst s
end
| Istore chunk addr args src s =>
- Istore chunk addr (subst_args fmap pc args) src s
+ Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s
| Icall sig ros args dst s =>
Icall sig ros (subst_args fmap pc args) dst s
| Itailcall sig ros args =>
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 9e0ad909..f9c7b400 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1527,7 +1527,10 @@ Proof.
assert (eval_addressing tge sp addr rs ## args = Some a).
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
eapply exec_Istore; eauto.
- rewrite (subst_args_ok' sp m); assumption.
+ - rewrite (subst_args_ok' sp m) by assumption.
+ eassumption.
+ - rewrite (subst_arg_ok' sp m) by assumption.
+ eassumption.
}
constructor; auto.
diff --git a/backend/CSE3.v b/backend/CSE3.v
index 352cc895..2203ad14 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -57,7 +57,7 @@ Definition transf_instr (fmap : PMap.t RB.t)
| Some src => Iop Omove (src::nil) dst s
end
| Istore chunk addr args src s =>
- Istore chunk addr (subst_args fmap pc args) src s
+ Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s
| Icall sig ros args dst s =>
Icall sig ros (subst_args fmap pc args) dst s
| Itailcall sig ros args =>
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index bc5d3244..b495371d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -64,6 +64,7 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
Qed.
Definition lub := PSet.inter.
+ Definition glb := PSet.union.
Lemma ge_lub_left: forall x y, ge (lub x y) x.
Proof.
@@ -274,7 +275,8 @@ Section OPERATIONS.
Definition oper (dst : reg) (op: sym_op) (args : list reg)
(rel : RELATION.t) : RELATION.t :=
match rhs_find op (forward_move_l rel args) rel with
- | Some r => move r dst rel
+ | Some r => RELATION.glb (move r dst rel)
+ (oper1 dst op args rel)
| None => oper1 dst op args rel
end.
@@ -323,7 +325,7 @@ Section OPERATIONS.
(chunk : memory_chunk) (addr: addressing) (args : list reg)
(src : reg) (ty: typ)
(rel : RELATION.t) : RELATION.t :=
- store1 chunk addr (forward_move_l rel args) src ty rel.
+ store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel.
Definition kill_builtin_res res rel :=
match res with
@@ -354,7 +356,7 @@ Section OPERATIONS.
| Icond _ _ _ _ _
| Ijumptable _ _ => Some rel
| Istore chunk addr args src _ =>
- Some (store chunk addr args src (tenv src) rel)
+ Some (store chunk addr args src (tenv (forward_move rel src)) rel)
| Iop op args dst _ => Some (oper dst (SOp op) args rel)
| Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
| Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index f4ec7a10..3ea5e078 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -361,6 +361,30 @@ Section SOUNDNESS.
eq_catalog ctx i = Some eq ->
sem_eq eq rs m.
+ Lemma sem_rel_glb:
+ forall rel1 rel2 rs m,
+ (sem_rel (RELATION.glb rel1 rel2) rs m) <->
+ ((sem_rel rel1 rs m) /\
+ (sem_rel rel2 rs m)).
+ Proof.
+ intros.
+ unfold sem_rel, RELATION.glb.
+ split.
+ - intro IMPLIES.
+ split;
+ intros i eq CONTAINS;
+ specialize IMPLIES with (i:=i) (eq0:=eq);
+ rewrite PSet.gunion in IMPLIES;
+ rewrite orb_true_iff in IMPLIES;
+ intuition.
+ - intros (IMPLIES1 & IMPLIES2) i eq.
+ rewrite PSet.gunion.
+ rewrite orb_true_iff.
+ specialize IMPLIES1 with (i:=i) (eq0:=eq).
+ specialize IMPLIES2 with (i:=i) (eq0:=eq).
+ intuition.
+ Qed.
+
Hypothesis ctx_kill_reg_has_lhs :
forall lhs sop args j,
eq_catalog ctx j = Some {| eq_lhs := lhs;
@@ -755,11 +779,13 @@ Section SOUNDNESS.
intros REL RHS.
unfold oper.
destruct rhs_find as [src |] eqn:RHS_FIND.
- - pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
- eapply forward_move_rhs_sound in RHS.
- 2: eassumption.
- rewrite <- (sem_rhs_det SOUND RHS).
- apply move_sound; auto.
+ - apply sem_rel_glb; split.
+ + pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
+ eapply forward_move_rhs_sound in RHS.
+ 2: eassumption.
+ rewrite <- (sem_rhs_det SOUND RHS).
+ apply move_sound; auto.
+ + apply oper1_sound; auto.
- apply oper1_sound; auto.
Qed.
@@ -848,14 +874,14 @@ Section SOUNDNESS.
Qed.
Hint Resolve store1_sound : cse3.
-
+
Theorem store_sound:
forall no chunk addr args a src rel tenv rs m m',
sem_rel rel rs m ->
wt_regset tenv rs ->
eval_addressing genv sp addr (rs ## args) = Some a ->
Mem.storev chunk m a (rs#src) = Some m' ->
- sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'.
+ sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'.
Proof.
unfold store.
intros until m'.
@@ -863,8 +889,8 @@ Section SOUNDNESS.
rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial.
rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
apply store1_sound with (a := a) (m := m); trivial.
- rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
- assumption.
+ (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial.
+ assumption. *)
Qed.
Hint Resolve store_sound : cse3.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 53872e62..ccbfd198 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -689,10 +689,13 @@ Proof.
- (* Istore *)
exists (State ts tf sp pc' rs m'). split.
- + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
+ + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args))
+ (src := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc src)) ; try eassumption.
* TR_AT. reflexivity.
* rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved.
+ eassumption.
+ * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial.
assumption.
+ econstructor; eauto.
IND_STEP.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 00df01e3..9c836037 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1535,7 +1535,6 @@ Opaque Int.eq.
+ apply exec_straight_one. simpl. eauto.
+ repeat split.
* rewrite Pregmap.gss.
- subst v.
destruct (rs x0); simpl; trivial.
unfold Val.maketotal.
destruct (Int.ltu _ _); simpl; trivial.
@@ -1546,7 +1545,6 @@ Opaque Int.eq.
+ apply exec_straight_one. simpl. eauto.
+ repeat split.
* rewrite Pregmap.gss.
- subst v.
destruct (rs x0); simpl; trivial.
unfold Val.maketotal.
destruct (Int.ltu _ _); simpl; trivial.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 946007c1..819120a0 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -988,16 +988,16 @@ Definition arith_eval_rr n v :=
| Pfinvw => ExtValues.invfs v
| Pfnarrowdw => Val.singleoffloat v
| Pfwidenlwd => Val.floatofsingle v
- | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
- | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
- | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
- | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
- | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
- | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
- | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
- | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end
- | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end
- | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end
+ | Pfloatwrnsz => Val.maketotal (Val.singleofint v)
+ | Pfloatuwrnsz => Val.maketotal (Val.singleofintu v)
+ | Pfloatudrnsz => Val.maketotal (Val.floatoflongu v)
+ | Pfloatdrnsz => Val.maketotal (Val.floatoflong v)
+ | Pfixedwrzz => Val.maketotal (Val.intofsingle v)
+ | Pfixeduwrzz => Val.maketotal (Val.intuofsingle v)
+ | Pfixeddrzz => Val.maketotal (Val.longoffloat v)
+ | Pfixedudrzz => Val.maketotal (Val.longuoffloat v)
+ | Pfixeddrzz_i32 => Val.maketotal (Val.intoffloat v)
+ | Pfixedudrzz_i32 => Val.maketotal (Val.intuoffloat v)
end.
Definition arith_eval_ri32 n i :=
diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v
index ae11a220..4dd0441d 100644
--- a/mppa_k1c/ConstpropOpproof.v
+++ b/mppa_k1c/ConstpropOpproof.v
@@ -276,7 +276,8 @@ Proof.
inv H; auto.
destruct (Int.is_power2 n) eqn:?.
destruct (Int.ltu i (Int.repr 31)) eqn:?.
- exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
+ exists v; split; auto. simpl.
+ erewrite Val.divs_pow2; eauto. reflexivity. congruence.
exists v; auto.
exists v; auto.
Qed.
@@ -449,7 +450,8 @@ Lemma make_divlimm_correct:
Proof.
intros; unfold make_divlimm.
destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?.
- rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto.
+ rewrite H0 in H. econstructor; split. simpl; eauto.
+ erewrite Val.divls_pow2; eauto. auto.
exists v; auto.
exists v; auto.
Qed.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 4caac9e1..012d67d0 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -374,7 +374,7 @@ Definition eval_operation
| Ororimm n, v1 :: nil => Some (Val.ror v1 (Vint n))
| Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2)
| Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n))
- | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
+ | Oshrximm n, v1::nil => Some (Val.maketotal (Val.shrx v1 (Vint n)))
| Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3))
| (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n)))
| Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3))
@@ -424,7 +424,7 @@ Definition eval_operation
| Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n))
| Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
| Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
- | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
+ | Oshrxlimm n, v1::nil => Some (Val.maketotal (Val.shrxl v1 (Vint n)))
| Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3))
| (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n)))
| Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3))
@@ -454,20 +454,20 @@ Definition eval_operation
| Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
| Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
- | Ointoffloat, v1::nil => Val.intoffloat v1
- | Ointuoffloat, v1::nil => Val.intuoffloat v1
- | Ointofsingle, v1::nil => Val.intofsingle v1
- | Ointuofsingle, v1::nil => Val.intuofsingle v1
- | Osingleofint, v1::nil => Val.singleofint v1
- | Osingleofintu, v1::nil => Val.singleofintu v1
- | Olongoffloat, v1::nil => Val.longoffloat v1
- | Olonguoffloat, v1::nil => Val.longuoffloat v1
- | Ofloatoflong, v1::nil => Val.floatoflong v1
- | Ofloatoflongu, v1::nil => Val.floatoflongu v1
- | Olongofsingle, v1::nil => Val.longofsingle v1
- | Olonguofsingle, v1::nil => Val.longuofsingle v1
- | Osingleoflong, v1::nil => Val.singleoflong v1
- | Osingleoflongu, v1::nil => Val.singleoflongu v1
+ | Ointoffloat, v1::nil => Some (Val.maketotal (Val.intoffloat v1))
+ | Ointuoffloat, v1::nil => Some (Val.maketotal (Val.intuoffloat v1))
+ | Ointofsingle, v1::nil => Some (Val.maketotal (Val.intofsingle v1))
+ | Ointuofsingle, v1::nil => Some (Val.maketotal (Val.intuofsingle v1))
+ | Osingleofint, v1::nil => Some (Val.maketotal (Val.singleofint v1))
+ | Osingleofintu, v1::nil => Some (Val.maketotal (Val.singleofintu v1))
+ | Olongoffloat, v1::nil => Some (Val.maketotal (Val.longoffloat v1))
+ | Olonguoffloat, v1::nil => Some (Val.maketotal (Val.longuoffloat v1))
+ | Ofloatoflong, v1::nil => Some (Val.maketotal (Val.floatoflong v1))
+ | Ofloatoflongu, v1::nil => Some (Val.maketotal (Val.floatoflongu v1))
+ | Olongofsingle, v1::nil => Some (Val.maketotal (Val.longofsingle v1))
+ | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
+ | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
+ | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
| Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
| (Oextfz stop start), v0::nil => Some (extfz stop start v0)
| (Oextfs stop start), v0::nil => Some (extfs stop start v0)
@@ -840,7 +840,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
- destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
- destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
(* shrx *)
- - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0...
+ - destruct v0; simpl... destruct (Int.ltu n (Int.repr 31)); simpl; trivial.
(* shrimm *)
- destruct v0; simpl...
(* madd *)
@@ -920,7 +920,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
- destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
- destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
(* shrxl *)
- - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
+ - destruct v0; simpl... destruct (Int.ltu n (Int.repr 63)); simpl; trivial.
(* maddl, maddlim *)
- apply type_addl.
- apply type_addl.
@@ -962,26 +962,26 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
- destruct v0...
- destruct v0...
(* intoffloat, intuoffloat *)
- - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
- - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2...
+ - destruct v0; simpl... destruct (Float.to_int f); simpl; trivial.
+ - destruct v0; simpl... destruct (Float.to_intu f); simpl; trivial.
(* intofsingle, intuofsingle *)
- - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2...
- - destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); inv H2...
+ - destruct v0; simpl... destruct (Float32.to_int f); simpl; trivial.
+ - destruct v0; simpl... destruct (Float32.to_intu f); simpl; trivial.
(* singleofint, singleofintu *)
- - destruct v0; simpl in H0; inv H0...
- - destruct v0; simpl in H0; inv H0...
+ - destruct v0; simpl...
+ - destruct v0; simpl...
(* longoffloat, longuoffloat *)
- - destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2...
- - destruct v0; simpl in H0; inv H0. destruct (Float.to_longu f); inv H2...
+ - destruct v0; simpl... destruct (Float.to_long f); simpl; trivial.
+ - destruct v0; simpl... destruct (Float.to_longu f); simpl; trivial.
(* floatoflong, floatoflongu *)
- - destruct v0; simpl in H0; inv H0...
- - destruct v0; simpl in H0; inv H0...
+ - destruct v0; simpl...
+ - destruct v0; simpl...
(* longofsingle, longuofsingle *)
- - destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2...
- - destruct v0; simpl in H0; inv H0. destruct (Float32.to_longu f); inv H2...
+ - destruct v0; simpl... destruct (Float32.to_long f); simpl; trivial.
+ - destruct v0; simpl... destruct (Float32.to_longu f); simpl; trivial.
(* singleoflong, singleoflongu *)
- - destruct v0; simpl in H0; inv H0...
- - destruct v0; simpl in H0; inv H0...
+ - destruct v0; simpl...
+ - destruct v0; simpl...
(* cmp *)
- destruct (eval_condition cond vl m)... destruct b...
(* extfz *)
@@ -1033,15 +1033,7 @@ Qed.
Definition is_trapping_op (op : operation) :=
match op with
| Odiv | Odivl | Odivu | Odivlu
- | Omod | Omodl | Omodu | Omodlu
- | Oshrximm _ | Oshrxlimm _
- | Ointoffloat | Ointuoffloat
- | Ointofsingle | Ointuofsingle
- | Olongoffloat | Olonguoffloat
- | Olongofsingle | Olonguofsingle
- | Osingleofint | Osingleofintu
- | Osingleoflong | Osingleoflongu
- | Ofloatoflong | Ofloatoflongu => true
+ | Omod | Omodl | Omodu | Omodlu => true
| _ => false
end.
@@ -1482,8 +1474,8 @@ Proof.
- inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
- inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
(* shrx *)
- - inv H4; simpl in H1; try discriminate. simpl.
- destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists.
+ - inv H4; simpl; auto.
+ destruct (Int.ltu n (Int.repr 31)); inv H; simpl; auto.
(* rorimm *)
- inv H4; simpl; auto.
(* madd, maddim *)
@@ -1572,8 +1564,8 @@ Proof.
- inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
- inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
(* shrx *)
- - inv H4; simpl in H1; try discriminate. simpl.
- destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists.
+ - inv H4; simpl; auto.
+ destruct (Int.ltu n (Int.repr 63)); simpl; auto.
(* maddl, maddlimm *)
- apply Val.addl_inject; auto.
@@ -1620,34 +1612,26 @@ Proof.
- inv H4; simpl; auto.
- inv H4; simpl; auto.
(* intoffloat, intuoffloat *)
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
- exists (Vint i); auto.
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2.
- exists (Vint i); auto.
+ - inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto.
+ - inv H4; simpl; auto. destruct (Float.to_intu f0); simpl; auto.
(* intofsingle, intuofsingle *)
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2.
- exists (Vint i); auto.
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_intu f0); simpl in H2; inv H2.
- exists (Vint i); auto.
+ - inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto.
+ - inv H4; simpl; auto. destruct (Float32.to_intu f0); simpl; auto.
(* singleofint, singleofintu *)
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+ - inv H4; simpl; auto.
+ - inv H4; simpl; auto.
(* longoffloat, longuoffloat *)
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2.
- exists (Vlong i); auto.
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_longu f0); simpl in H2; inv H2.
- exists (Vlong i); auto.
+ - inv H4; simpl; auto. destruct (Float.to_long f0); simpl; auto.
+ - inv H4; simpl; auto. destruct (Float.to_longu f0); simpl; auto.
(* floatoflong, floatoflongu *)
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+ - inv H4; simpl; auto.
+ - inv H4; simpl; auto.
(* longofsingle, longuofsingle *)
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_long f0); simpl in H2; inv H2.
- exists (Vlong i); auto.
- - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_longu f0); simpl in H2; inv H2.
- exists (Vlong i); auto.
+ - inv H4; simpl; auto. destruct (Float32.to_long f0); simpl; auto.
+ - inv H4; simpl; auto. destruct (Float32.to_longu f0); simpl; auto.
(* singleoflong, singleoflongu *)
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
- - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+ - inv H4; simpl; auto.
+ - inv H4; simpl; auto.
(* cmp *)
- subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index ada02585..5e4f3ed6 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -838,34 +838,7 @@ Proof.
+ predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
-- TrivialExists.
-(*
- intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
-+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
-+ destruct x; simpl in H0; try discriminate.
- destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
- predSpec Int.eq Int.eq_spec n Int.zero.
- - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
- - assert (NZ: Int.unsigned n <> 0).
- { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
- assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
- assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
- { unfold Int.ltu; apply zlt_true.
- unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64.
- rewrite Int.unsigned_repr. omega.
- assert (64 < Int.max_unsigned) by reflexivity. omega. }
- assert (X: eval_expr ge sp e m le
- (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
- (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
- { EvalOp. }
- assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
- (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
- { EvalOp. simpl. rewrite LTU2. auto. }
- TrivialExists.
- constructor. EvalOp. simpl; eauto. constructor.
- simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity.
- change (Int.unsigned Int64.iwordsize') with 64; omega.
-*)
+- TrivialExists. simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_cmplu:
@@ -915,6 +888,7 @@ Proof.
unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
eapply SplitLongproof.eval_longoffloat; eauto.
TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
@@ -922,6 +896,7 @@ Proof.
unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
eapply SplitLongproof.eval_longuoffloat; eauto.
TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
@@ -929,6 +904,7 @@ Proof.
unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
eapply SplitLongproof.eval_floatoflong; eauto.
TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
@@ -936,6 +912,7 @@ Proof.
unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
eapply SplitLongproof.eval_floatoflongu; eauto.
TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index cbe7a814..28294934 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1013,34 +1013,8 @@ Proof.
replace (Int.shrx i Int.zero) with i. auto.
unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
- econstructor; split. EvalOp. auto.
-(*
- intros. destruct x; simpl in H0; try discriminate.
- destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
- unfold shrximm.
- predSpec Int.eq Int.eq_spec n Int.zero.
- - subst n. exists (Vint i); split; auto.
- unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
- - assert (NZ: Int.unsigned n <> 0).
- { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
- assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
- assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
- { unfold Int.ltu; apply zlt_true.
- unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32.
- rewrite Int.unsigned_repr. omega.
- assert (32 < Int.max_unsigned) by reflexivity. omega. }
- assert (X: eval_expr ge sp e m le
- (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
- (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
- { EvalOp. }
- assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
- (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
- { EvalOp. simpl. rewrite LTU2. auto. }
- TrivialExists.
- constructor. EvalOp. simpl; eauto. constructor.
- simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity.
- change (Int.unsigned Int.iwordsize) with 32; omega.
-*)
+ econstructor; split. EvalOp.
+ simpl. rewrite H0. simpl. reflexivity. auto.
Qed.
Theorem eval_shl: binary_constructor_sound shl Val.shl.
@@ -1251,6 +1225,7 @@ Theorem eval_intoffloat:
exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
Proof.
intros; unfold intoffloat. TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_intuoffloat:
@@ -1260,6 +1235,7 @@ Theorem eval_intuoffloat:
exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
Proof.
intros; unfold intuoffloat. TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_floatofintu:
@@ -1279,7 +1255,7 @@ Proof.
constructor. econstructor. constructor. eassumption. constructor.
simpl. f_equal. constructor.
simpl.
- destruct x; simpl; trivial.
+ destruct x; simpl; trivial; try discriminate.
f_equal.
inv H0.
f_equal.
@@ -1303,7 +1279,7 @@ Proof.
constructor. econstructor. constructor. eassumption. constructor.
simpl. f_equal. constructor.
simpl.
- destruct x; simpl; trivial.
+ destruct x; simpl; trivial; try discriminate.
f_equal.
inv H0.
f_equal.
@@ -1318,6 +1294,7 @@ Theorem eval_intofsingle:
exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
Proof.
intros; unfold intofsingle. TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_singleofint:
@@ -1327,6 +1304,7 @@ Theorem eval_singleofint:
exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
Proof.
intros; unfold singleofint; TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_intuofsingle:
@@ -1336,6 +1314,7 @@ Theorem eval_intuofsingle:
exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
Proof.
intros; unfold intuofsingle. TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_singleofintu:
@@ -1345,6 +1324,7 @@ Theorem eval_singleofintu:
exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
Proof.
intros; unfold intuofsingle. TrivialExists.
+ simpl. rewrite H0. reflexivity.
Qed.
Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 7d84447e..901908b5 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -14,6 +14,86 @@ Require Import Coqlib Compopts.
Require Import AST Integers Floats Values Memory Globalenvs.
Require Import Op ExtValues ExtFloats RTL ValueDomain.
+Definition intoffloat_total (x: aval) :=
+ match x with
+ | F f =>
+ match Float.to_int f with
+ | Some i => I i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition intuoffloat_total (x: aval) :=
+ match x with
+ | F f =>
+ match Float.to_intu f with
+ | Some i => I i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition intofsingle_total (x: aval) :=
+ match x with
+ | FS f =>
+ match Float32.to_int f with
+ | Some i => I i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition intuofsingle_total (x: aval) :=
+ match x with
+ | FS f =>
+ match Float32.to_intu f with
+ | Some i => I i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition longoffloat_total (x: aval) :=
+ match x with
+ | F f =>
+ match Float.to_long f with
+ | Some i => L i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition longuoffloat_total (x: aval) :=
+ match x with
+ | F f =>
+ match Float.to_longu f with
+ | Some i => L i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition longofsingle_total (x: aval) :=
+ match x with
+ | FS f =>
+ match Float32.to_long f with
+ | Some i => L i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
+Definition longuofsingle_total (x: aval) :=
+ match x with
+ | FS f =>
+ match Float32.to_longu f with
+ | Some i => L i
+ | None => ntop
+ end
+ | _ => ntop1 x
+ end.
+
Definition minf := binop_float ExtFloat.min.
Definition maxf := binop_float ExtFloat.max.
Definition minfs := binop_single ExtFloat32.min.
@@ -282,18 +362,18 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Ofmsubfs, v1::v2::v3::nil => fmsubfs v1 v2 v3
| Osingleoffloat, v1::nil => singleoffloat v1
| Ofloatofsingle, v1::nil => floatofsingle v1
- | Ointoffloat, v1::nil => intoffloat v1
- | Ointuoffloat, v1::nil => intuoffloat v1
- | Ointofsingle, v1::nil => intofsingle v1
- | Ointuofsingle, v1::nil => intuofsingle v1
+ | Ointoffloat, v1::nil => intoffloat_total v1
+ | Ointuoffloat, v1::nil => intuoffloat_total v1
+ | Ointofsingle, v1::nil => intofsingle_total v1
+ | Ointuofsingle, v1::nil => intuofsingle_total v1
| Osingleofint, v1::nil => singleofint v1
| Osingleofintu, v1::nil => singleofintu v1
- | Olongoffloat, v1::nil => longoffloat v1
- | Olonguoffloat, v1::nil => longuoffloat v1
+ | Olongoffloat, v1::nil => longoffloat_total v1
+ | Olonguoffloat, v1::nil => longuoffloat_total v1
| Ofloatoflong, v1::nil => floatoflong v1
| Ofloatoflongu, v1::nil => floatoflongu v1
- | Olongofsingle, v1::nil => longofsingle v1
- | Olonguofsingle, v1::nil => longuofsingle v1
+ | Olongofsingle, v1::nil => longofsingle_total v1
+ | Olonguofsingle, v1::nil => longuofsingle_total v1
| Osingleoflong, v1::nil => singleoflong v1
| Osingleoflongu, v1::nil => singleoflongu v1
| Ocmp c, _ => of_optbool (eval_static_condition c vl)
@@ -317,6 +397,196 @@ Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.
+Lemma intoffloat_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
+Proof.
+ unfold Val.intoffloat, intoffloat_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve intoffloat_total_sound : va.
+
+Lemma intuoffloat_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
+Proof.
+ unfold Val.intoffloat, intoffloat_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve intuoffloat_total_sound : va.
+
+Lemma intofsingle_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
+Proof.
+ unfold Val.intofsingle, intofsingle_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve intofsingle_total_sound : va.
+
+Lemma intuofsingle_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
+Proof.
+ unfold Val.intofsingle, intofsingle_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve intuofsingle_total_sound : va.
+
+Lemma singleofint_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x).
+Proof.
+ unfold Val.singleofint, singleofint; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve singleofint_total_sound : va.
+
+Lemma singleofintu_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x).
+Proof.
+ unfold Val.singleofintu, singleofintu; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve singleofintu_total_sound : va.
+
+Lemma longoffloat_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
+Proof.
+ unfold Val.longoffloat, longoffloat_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve longoffloat_total_sound : va.
+
+Lemma longuoffloat_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
+Proof.
+ unfold Val.longoffloat, longoffloat_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve longuoffloat_total_sound : va.
+
+Lemma longofsingle_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
+Proof.
+ unfold Val.longofsingle, longofsingle_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve longofsingle_total_sound : va.
+
+Lemma longuofsingle_total_sound:
+ forall v x
+ (MATCH : vmatch bc v x),
+ vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
+Proof.
+ unfold Val.longofsingle, longofsingle_total. intros.
+ inv MATCH; simpl in *; try constructor.
+ all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+ unfold ntop1, provenance.
+ destruct (va_strict tt); constructor.
+Qed.
+
+Hint Resolve longuofsingle_total_sound : va.
+
+Lemma singleoflong_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x).
+Proof.
+ unfold Val.singleoflong, singleoflong; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve singleoflong_total_sound : va.
+
+Lemma singleoflongu_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
+Proof.
+ unfold Val.singleoflongu, singleoflongu; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve singleoflongu_total_sound : va.
+
+Lemma floatoflong_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x).
+Proof.
+ unfold Val.floatoflong, floatoflong; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve floatoflong_total_sound : va.
+
+Lemma floatoflongu_total_sound:
+ forall v x, vmatch bc v x ->
+ vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
+Proof.
+ unfold Val.floatoflongu, floatoflongu; intros.
+ inv H; simpl.
+ all: auto with va.
+ all: unfold ntop1, provenance.
+ all: try constructor.
+Qed.
+
+Hint Resolve floatoflongu_total_sound : va.
+
Lemma minf_sound:
forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
Proof.
@@ -490,6 +760,26 @@ Proof.
destruct addr; trivial; discriminate.
Qed.
+Lemma vmatch_vint_ntop1:
+ forall x y, vmatch bc (Vint x) (ntop1 y).
+Proof.
+ intro. unfold ntop1, provenance.
+ destruct y;
+ destruct (va_strict tt);
+ constructor.
+Qed.
+
+Lemma vmatch_vlong_ntop1:
+ forall x y, vmatch bc (Vlong x) (ntop1 y).
+Proof.
+ intro. unfold ntop1, provenance.
+ destruct y;
+ destruct (va_strict tt);
+ constructor.
+Qed.
+
+Hint Resolve vmatch_vint_ntop1 vmatch_vlong_ntop1: va.
+
Theorem eval_static_operation_sound:
forall op vargs m vres aargs,
eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
@@ -518,6 +808,10 @@ Proof.
end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
+ eauto with va.
+ destruct n; destruct shift; reflexivity.
+ - (* shrx *)
+ inv H1; simpl; try constructor.
+ all: destruct Int.ltu; [simpl | constructor; fail].
+ all: auto with va.
- replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
| Vlong n2 => Vlong (Int64.add n n2)
| Vptr b2 ofs2 =>
@@ -535,6 +829,10 @@ Proof.
end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
+ eauto with va.
+ destruct a1; destruct shift; reflexivity.
+ - (* shrxl *)
+ inv H1; simpl; try constructor.
+ all: destruct Int.ltu; [simpl | constructor; fail].
+ all: auto with va.
- apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
(* extfz *)
diff --git a/test/c/Results/mandelbrot-mppa_k1c b/test/c/Results/mandelbrot-mppa_k1c
index f50961fe..55c5683a 100644
--- a/test/c/Results/mandelbrot-mppa_k1c
+++ b/test/c/Results/mandelbrot-mppa_k1c
Binary files differ
diff --git a/test/monniaux/licm/addv.c b/test/monniaux/licm/addv.c
new file mode 100644
index 00000000..bb0098d0
--- /dev/null
+++ b/test/monniaux/licm/addv.c
@@ -0,0 +1,6 @@
+void addv(double x, double y, int n, int *z)
+{
+ for(int i=0; i<n; i++) {
+ z[i] += (int) (x*y);
+ }
+}
generated by cgit (git 2.34.1) at 2024-06-03 04:12:58 +0000