diff options
| author | James Pollard <james@pollard.dev> | 2020-07-06 23:20:00 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-06 23:20:00 +0100 |
| commit | 897b2b15a810e996895dda0d863dcefb27dfabaf (patch) | |
| tree | 40d8b2d12c00edbc15b7eed9e29235f47f679e27 /src/translation | |
| parent | b0e1a1383890d9b0a14ffaabce4c3d6453eb0a9c (diff) | |
| download | vericert-kvx-897b2b15a810e996895dda0d863dcefb27dfabaf.tar.gz vericert-kvx-897b2b15a810e996895dda0d863dcefb27dfabaf.zip | |
Concatenation style loads.
Diffstat (limited to 'src/translation')
| -rw-r--r-- | src/translation/HTLgen.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 35203f8..d1c1363 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -427,17 +427,13 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := (enumerate 0 ns). Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt := - let l0 := Vnonblock (Vvarb0 dst) (Vvari stack addr) in - let l1 := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in - let l2 := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in - let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) - in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. + Vnonblock (Vvar dst) (Vload stack addr). Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt := let l0 := Vnonblock (Vvari stack addr) (Vvarb0 src) in let l1 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in let l2 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in - let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 3)) (Vvarb3 src) in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := |