diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 19:56:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 19:56:30 +0100 |
| commit | 59413cb4018d09fb3b641a49ab062bc933d5274c (patch) | |
| tree | 5599db40a806497089df856604d5917ea5549ea1 /backend/CSE3analysisproof.v | |
| parent | 76c887ad132aa7b0c7ac72dca5d56e4c2bf1747a (diff) | |
| download | compcert-kvx-59413cb4018d09fb3b641a49ab062bc933d5274c.tar.gz compcert-kvx-59413cb4018d09fb3b641a49ab062bc933d5274c.zip | |
starts compiling but still fake
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index c0a9be48..f805d2b8 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -134,9 +134,9 @@ Lemma get_kills_has_lhs : PTree.get j eqs = Some {| eq_lhs := lhs; eq_op := sop; eq_args:= args |} -> - PSet.contains (Regmap.get lhs (get_kills eqs)) j = true. + PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true. Proof. - unfold get_kills. + unfold get_reg_kills. intros. rewrite PTree.fold_spec. change (fold_left @@ -154,9 +154,9 @@ Lemma get_kills_has_arg : eq_op := sop; eq_args:= args |} -> In arg args -> - PSet.contains (Regmap.get arg (get_kills eqs)) j = true. + PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true. Proof. - unfold get_kills. + unfold get_reg_kills. intros. rewrite PTree.fold_spec. change (fold_left @@ -232,14 +232,14 @@ Section SOUNDNESS. eq_op := SOp op; eq_args:= args |} -> op_depends_on_memory op = true -> - PSet.contains (eq_kill_mem ctx) j = true. + PSet.contains (eq_kill_mem ctx tt) j = true. Hypothesis ctx_kill_mem_has_load : forall lhs chunk addr args j, eq_catalog ctx j = Some {| eq_lhs := lhs; eq_op := SLoad chunk addr; eq_args:= args |} -> - PSet.contains (eq_kill_mem ctx) j = true. + PSet.contains (eq_kill_mem ctx tt) j = true. Theorem kill_reg_sound : forall rel rs m dst v, |