diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-05-01 23:42:53 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:23 -0400 |
| commit | a1f1613e4a968efd47c8f1464ec1a68986cadc44 (patch) | |
| tree | d8d159af7a0b7da7bcd144f8387a4c552deed72d /src/Assembly/QhasmCommon.v | |
| parent | 49ed9cfaa635bfa0a12bfe1231b103f247ffc141 (diff) | |
A little progress on PseudoConversion
actually-decent PseudoConversion semantics
actually-decent PseudoConversion semantics
Diffstat (limited to 'src/Assembly/QhasmCommon.v')
| -rw-r--r-- | src/Assembly/QhasmCommon.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index c2b68bc77..410389638 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -19,6 +19,10 @@ Notation "'contra'" := (False_rec _ _) : state_scope. Obligation Tactic := abstract intuition. (* Asm Types *) +Inductive ISize: nat -> Type := + | I32: ISize 32 + | I64: ISize 64. + Inductive IConst: nat -> Type := | constInt32: word 32 -> IConst 32 | constInt64: word 64 -> IConst 64. @@ -89,6 +93,12 @@ Definition getStackWords {n} (x: Stack n) := | stack128 loc => 4 end. +Definition getIConstValue {n} (x: IConst n): nat := + match x with + | constInt32 v => wordToNat v + | constInt64 v => wordToNat v + end. + Definition getIRegIndex {n} (x: IReg n): nat := match x with | regInt32 loc => loc |