diff options
author | James Pollard <james@pollard.dev> | 2020-07-06 19:27:51 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-07-06 19:27:51 +0100 |
commit | ea44bd696dcfb446f5f980f16d7df41b21357698 (patch) | |
tree | c8c78b64a98dad7e2cbf22e3383e48727523b2e2 /src/translation/HTLgen.v | |
parent | ec97745e4675b72cbabd2a3bd12d6efdd8bfa6d6 (diff) | |
download | vericert-kvx-ea44bd696dcfb446f5f980f16d7df41b21357698.tar.gz vericert-kvx-ea44bd696dcfb446f5f980f16d7df41b21357698.zip |
Fix HTLgenspec.
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 995977c..09af28a 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -414,21 +414,19 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). -Definition add_single_cycle_load (n n' : node) (stack : reg) (addr : expr) (dst : reg) : mon unit := +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 - let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 - in add_instr n n' instr. + let l3 := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. -Definition add_single_cycle_store (n n' : node) (stack : reg) (addr : expr) (src : reg) : mon unit := +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) in - let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3 - in add_instr n n' instr. + let l3 := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) + in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with @@ -442,10 +440,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Iload mem addr args dst n' => do addr' <- translate_eff_addressing addr args; do _ <- declare_reg None dst 32; - add_single_cycle_load n n' stack addr' dst + add_instr n n' $ create_single_cycle_load stack addr' dst | Istore mem addr args src n' => do addr' <- translate_eff_addressing addr args; - add_single_cycle_store n n' stack addr' src + add_instr n n' $ create_single_cycle_store stack addr' src | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") |