diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-03 01:05:32 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-03 01:05:32 +0000 |
| commit | 8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 (patch) | |
| tree | edb357c24b7c4a50569cdc32e6d4f17f48673ede /src/hls/HTLPargen.v | |
| parent | 3ddec58aa1ad7d1bd772868d34ab0e11cf8f1ad4 (diff) | |
| download | vericert-8d5047ca436ba42e9253d24d6b5b2c0c62dd7437.tar.gz vericert-8d5047ca436ba42e9253d24d6b5b2c0c62dd7437.zip | |
Fix state generation for if-conversion
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 0508e6f..0804b0e 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -77,7 +77,8 @@ Module HTLState <: State. Definition st_prop := st_incr. Hint Unfold st_prop : htlh. - Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + Lemma st_refl : forall s, st_prop s s. + Proof. auto with htlh. Qed. Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. @@ -552,7 +553,7 @@ Definition poslength {A : Type} (l : list A) : positive := Fixpoint penumerate {A : Type} (p : positive) (l : list A) {struct l} : list (positive * A) := match l with - | x :: xs => (p, x) :: penumerate (Pos.succ p) xs + | x :: xs => (p, x) :: penumerate (Pos.pred p) xs | nil => nil end. @@ -669,7 +670,7 @@ Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * list inst let (n, li) := ni in do _ <- collectlist (translate_inst fin rtrn stack preg n) li; do st <- get; - add_control_instr n (state_goto st.(st_st) (Pos.succ n)). + add_control_instr n (state_goto st.(st_st) (Pos.pred n)). Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) : mon (stmnt * stmnt) := @@ -717,7 +718,7 @@ Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) do _ <- collectlist (translate_inst_list fin rtrn stack preg) (penumerate n bb.(bb_body)); translate_cfi fin rtrn stack preg - ((n + poslength bb.(bb_body))%positive, bb.(bb_exit)). + ((n - poslength bb.(bb_body))%positive, bb.(bb_exit)). Definition transf_module (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then |