diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-04-15 15:04:06 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-04-15 15:04:06 -0400 |
commit | d359a11c80fc9d3efd5a88906af4b81b3197ea32 (patch) | |
tree | 60ccbd1d341c271b300d5edbc64cecc12eaec937 /src/Assembly | |
parent | 16d8288b5b6e31e67da0e7531abec36982cb3397 (diff) |
updating QhasmCommon
Diffstat (limited to 'src/Assembly')
-rw-r--r-- | src/Assembly/QhasmCommon.v | 156 | ||||
-rw-r--r-- | src/Assembly/State.v | 37 | ||||
-rw-r--r-- | src/Assembly/StringConversion.v | 112 |
3 files changed, 173 insertions, 132 deletions
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 4c9022d21..6b40c9d2a 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -1,4 +1,4 @@ -Require Export String List NPeano. +Require Export String List NPeano NArith. Require Export Bedrock.Word. (* A formalization of x86 qhasm *) @@ -9,16 +9,53 @@ Definition Invert := bool. (* A constant upper-bound on the number of operations we run *) Definition maxOps: nat := 1000. -(* Datatypes *) -Inductive Const: nat -> Set := - | const32: word 32 -> Const 32 - | const64: word 64 -> Const 64 - | const128: word 128 -> Const 128. +(* Float Datatype *) -Inductive Reg: nat -> Set := - | reg32: nat -> Reg 32. +Record Float (n: nat) (fractionBits: nat) := mkFloat { + FloatType: Set; -Inductive Stack: nat -> Set := + wordToFloat: word fractionBits -> FloatType; + floatToWord: FloatType -> word fractionBits; + + floatPlus: FloatType -> FloatType -> FloatType; + floatMult: FloatType -> FloatType -> FloatType; + + floatPlus_wordToFloat : forall n m, + (wordToN n < (Npow2 (fractionBits - 1)))%N -> + (wordToN m < (Npow2 (fractionBits - 1)))%N -> + floatPlus (wordToFloat n) (wordToFloat m) + = wordToFloat (wplus n m); + + floatMult_wordToFloat : forall n m, + (wordToN n < (Npow2 (fractionBits / 2)%nat))%N -> + (wordToN m < (Npow2 (fractionBits / 2)%nat))%N -> + floatMult (wordToFloat n) (wordToFloat m) + = wordToFloat (wmult n m); + + wordToFloat_spec : forall x, + floatToWord (wordToFloat x) = x +}. + +Parameter Float32: Float 32 23. + +Parameter Float64: Float 64 53. + +(* Asm Types *) +Inductive IConst: nat -> Type := + | constInt32: word 32 -> IConst 32. + +Inductive FConst: nat -> Type := + | constFloat32: forall b, Float 32 b -> FConst 32 + | constFloat64: forall b, Float 64 b -> FConst 64. + +Inductive IReg: nat -> Type := + | regInt32: nat -> IReg 32. + +Inductive FReg: nat -> Type := + | regFloat32: nat -> FReg 32 + | regFloat64: nat -> FReg 64. + +Inductive Stack: nat -> Type := | stack32: nat -> Stack 32 | stack64: nat -> Stack 64 | stack128: nat -> Stack 128. @@ -26,66 +63,74 @@ Inductive Stack: nat -> Set := Definition CarryState := option bool. (* Assignments *) -Inductive Assignment : Set := - | AStack: forall n, Reg n -> Stack n -> Assignment - | AReg: forall n, Reg n -> Reg n -> Assignment - | AIndex: forall n m, Reg n -> Reg m -> Index (n/m)%nat -> Assignment - | AConst: forall n, Reg n -> Const n -> Assignment - | APtr: forall n, Reg 32 -> Stack n -> Assignment. +Inductive Assignment : Type := + | AStackInt: forall n, IReg n -> Stack n -> Assignment + | AStackFloat: forall n, FReg n -> Stack n -> Assignment + + | ARegInt: forall n, IReg n -> IReg n -> Assignment + | ARegFloat: forall n, FReg n -> FReg n -> Assignment + + | AConstInt: forall n, IReg n -> IConst n -> Assignment + | AConstFloat: forall n, FReg n -> FConst n -> Assignment + + | AIndex: forall n m, IReg n -> IReg m -> Index (n/m)%nat -> Assignment + | APtr: forall n, IReg 32 -> Stack n -> Assignment. Hint Constructors Assignment. (* Operations *) -Inductive QOp := - | QPlus: QOp | QMinus: QOp | QIMult: QOp - | QXor: QOp | QAnd: QOp | QOr: QOp. +Inductive IntOp := + | IPlus: IntOp | IMinus: IntOp + | IXor: IntOp | IAnd: IntOp | IOr: IntOp. -Inductive QFixedOp := - | QMult: QFixedOp | UDiv: QFixedOp. +Inductive FloatOp := + | FPlus: FloatOp | FMinus: FloatOp + | FXor: FloatOp | FAnd: FloatOp | FOr: FloatOp + | FMult: FloatOp | FDiv: FloatOp. -Inductive QRotOp := - | Shl: QRotOp | Shr: QRotOp | QRotl: QRotOp | QRotr: QRotOp. +Inductive RotOp := + | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp. Inductive Operation := - | OpConst: QOp -> Reg 32 -> Const 32 -> Operation - | OpReg: QOp -> Reg 32 -> Reg 32 -> Operation - | OpFixedConst: QFixedOp -> Reg 32 -> Const 32 -> Operation - | OpFixedReg: QFixedOp -> Reg 32 -> Reg 32 -> Operation - | OpRot: QRotOp -> Reg 32 -> Index 32 -> Operation. + | IOpConst: IntOp -> IReg 32 -> IConst 32 -> Operation + | IOpReg: IntOp -> IReg 32 -> IReg 32 -> Operation + + | FOpConst32: FloatOp -> FReg 32 -> FConst 32 -> Operation + | FOpReg32: FloatOp -> FReg 32 -> FReg 32 -> Operation + + | FOpConst64: FloatOp -> FReg 64 -> FConst 64 -> Operation + | FOpReg64: FloatOp -> FReg 64 -> FReg 64 -> Operation + + | OpRot: RotOp -> IReg 32 -> Index 32 -> Operation. Hint Constructors Operation. (* Control Flow *) Inductive TestOp := - | TEq: TestOp - | TLt: TestOp - | TUnsignedLt: TestOp - | TGt: TestOp - | TUnsignedGt: TestOp. + | TEq: TestOp | TLt: TestOp | TLe: TestOp + | TGt: TestOp | TGe: TestOp. Inductive Conditional := | TestTrue: Conditional | TestFalse: Conditional - | TestReg32Reg32: TestOp -> Invert -> Reg 32 -> Reg 32 -> Conditional - | TestReg32Const: TestOp -> Invert -> Reg 32 -> Const 32 -> Conditional. - -Definition invertConditional (c: Conditional): Conditional := - match c with - | TestTrue => TestFalse - | TestFalse => TestTrue - | TestReg32Reg32 o i r0 r1 => TestReg32Reg32 o (negb i) r0 r1 - | TestReg32Const o i r c => TestReg32Const o (negb i) r c - end. + | TestInt: forall n, TestOp -> IReg n -> IReg n -> Conditional + | TestFloat: forall n, TestOp -> FReg n -> FReg n -> Conditional. Hint Constructors Conditional. (* Reg, Stack, Const Utilities *) -Definition getRegWords {n} (x: Reg n) := +Definition getIRegWords {n} (x: IReg n) := + match x with + | regInt32 loc => 1 + end. + +Definition getFRegWords {n} (x: FReg n) := match x with - | reg32 loc => 1 + | regFloat32 loc => 1 + | regFloat64 loc => 2 end. Definition getStackWords {n} (x: Stack n) := @@ -95,11 +140,15 @@ Definition getStackWords {n} (x: Stack n) := | stack128 loc => 4 end. -Definition getRegIndex {n} (x: Reg n): nat := +Definition getIRegIndex {n} (x: IReg n): nat := match x with - | reg32 loc => loc - | reg3232 loc => loc - | reg6464 loc => loc + | regInt32 loc => loc + end. + +Definition getFRegIndex {n} (x: FReg n): nat := + match x with + | regFloat32 loc => loc + | regFloat64 loc => loc end. Definition getStackIndex {n} (x: Stack n): nat := @@ -110,10 +159,15 @@ Definition getStackIndex {n} (x: Stack n): nat := end. (* For register allocation checking *) -Definition regCount (base: nat): nat := +Definition intRegCount (base: nat): nat := match base with - | 32 => 7 | 64 => 8 - | 128 => 8 | 80 => 8 + | 32 => 7 | _ => 0 end. +Definition floatRegCount (base: nat): nat := + match base with + | 32 => 8 + | 64 => 8 + | _ => 0 + end. diff --git a/src/Assembly/State.v b/src/Assembly/State.v index 16b9b12d3..c61a408c3 100644 --- a/src/Assembly/State.v +++ b/src/Assembly/State.v @@ -26,7 +26,7 @@ Module State. (* Sugar and Tactics *) Definition convert {A B: Type} (x: A) (H: A = B): B := - eq_rect A (fun B0 : Type => B0) x B H. + eq_rect A (fun B0 : Type => B0) x B H. Notation "'always' A" := (fun _ => A) (at level 90) : state_scope. Notation "'cast' e" := (convert e _) (at level 20) : state_scope. @@ -38,15 +38,15 @@ Module State. (* The Big Definition *) Inductive State := - | fullState (regState: StateMap) (stackState: DefMap): State. + | fullState (regState: StateMap) (stackState: DefMap) (carryBit: CarryState): State. - Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N). + Definition emptyState: State := fullState (NatM.empty DefMap) (NatM.empty N) None. (* Register State Manipulations *) Definition getReg {n} (reg: Reg n) (state: State): option (word n) := match state with - | fullState regState stackState => + | fullState regState stackState _ => match (NatM.find n regState) with | Some map => match (NatM.find (getRegIndex reg) map) with @@ -59,21 +59,36 @@ Module State. Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State := match state with - | fullState regState stackState => + | fullState regState stackState carryState => match (NatM.find n regState) with | Some map => Some (fullState (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map) regState) - stackState) + stackState + carryState) | None => None end end. + (* Carry State Manipulations *) + + Definition getCarry {n} (reg: Reg n) (state: State): CarryState := + match state with + | fullState _ _ b => b + end. + + Definition setCarry (value: bool) (state: State): State := + match state with + | fullState regState stackState carryState => + fullState regState stackState (Some value) + end. + + (* Per-word Stack Operations *) Definition getStack32 (entry: Stack 32) (state: State): option (word 32) := match state with - | fullState regState stackState => + | fullState regState stackState _ => match entry with | stack32 loc => match (NatM.find loc stackState) with @@ -85,11 +100,13 @@ Module State. Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State := match state with - | fullState regState stackState => + | fullState regState stackState carryState => match entry with | stack32 loc => - (Some (fullState regState - (NatM.add loc (wordToN value) stackState))) + (Some (fullState + regState + (NatM.add loc (wordToN value) stackState) + carryState)) end end. diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v index d1b273c98..d44dbfcbf 100644 --- a/src/Assembly/StringConversion.v +++ b/src/Assembly/StringConversion.v @@ -1,6 +1,5 @@ Require Export Language Conversion. -Require Export Qhasm. -Require Import QhasmCommon QhasmEvalCommon QhasmUtil. +Require Import QhasmCommon QhasmEvalCommon QhasmUtil Qhasm. Require Export String Ascii. Require Import NArith NPeano. Require Export Bedrock.Word. @@ -53,81 +52,56 @@ Module StringConversion <: Conversion Qhasm QhasmString. Section Elements. Local Open Scope string_scope. + Import Util. Definition nameSuffix (n: nat): string := (nToHex (N.of_nat n)). - Definition wordToString {n} (w: word n): string := + Coercion wordToString {n} (w: word n): string := "0x" ++ (nToHex (wordToN w)). - Coercion wordToString : word >-> string. - - Definition constToString {n} (c: Const n): string := + Coercion constToString {n} (c: Const n): string := match c with | const32 w => "0x" ++ w | const64 w => "0x" ++ w | const128 w => "0x" ++ w end. - Coercion constToString : Const >-> string. - - Definition indexToString {n} (i: Index n): string := + Coercion indexToString {n} (i: Index n): string := "0x" ++ (nToHex (N.of_nat i)). - Coercion indexToString : Index >-> string. - - Definition regToString {n} (r: Reg n): option string := - Some match r with + Coercion regToString {n} (r: Reg n): string := + match r with | reg32 n => "ex" ++ (nameSuffix n) | reg3232 n => "mm" ++ (nameSuffix n) | reg6464 n => "xmm" ++ (nameSuffix n) | reg80 n => "st" ++ (nameSuffix n) end. - Definition stackToString {n} (s: Stack n): option string := - Some match s with + Coercion stackToString {n} (s: Stack n): string := + match s with | stack32 n => "word" ++ (nameSuffix n) | stack64 n => "double" ++ (nameSuffix n) | stack128 n => "quad" ++ (nameSuffix n) + | stack256 n => "stack256n" ++ (nameSuffix n) + | stack512 n => "stack512n" ++ (nameSuffix n) end. + Coercion stringToSome (x: string): option string := Some x. + Definition stackLocation {n} (s: Stack n): word 32 := combine (natToWord 8 n) (natToWord 24 n). Definition assignmentToString (a: Assignment): option string := match a with - | Assign32Stack32 r s => - match (regToString r, stackToString s) with - | (Some s0, Some s1) => s0 ++ " = " ++ s1 - | _ => None - end. - | Assign32Stack16 r s i => r0 ++ " = " ++ r1 - | Assign32Stack8 r s i => - | Assign32Stack64 r s i => - | Assign32Stack128 r s i => - - | Assign32Reg32 r0 r1 => r0 ++ " = " ++ r1 - | Assign32Reg16 r0 r1 i => - | Assign32Reg8 r0 r1 i => - | Assign32Reg64 r0 r1 i => - | Assign32Reg128 r0 r1 i => - - | Assign3232Stack32 r i s => - | Assign3232Stack64 r s => - | Assign3232Stack128 r s i => - - | Assign3232Reg32 r0 i r1 => - | Assign3232Reg64 r0 r1 => - | Assign3232Reg128 r0 r1 i => - - | Assign6464Reg32 r0 i r1 => - | Assign6464Reg64 r0 i r1 => - | Assign6464Reg128 r0 r1 => - - | AssignConstant r c => + + (* r = s *) + | Assign32Stack32 r s => r ++ " = " ++ s + + | _ => None end. - Definition binOpToString (b: BinOp): string := + Coercion binOpToString (b: BinOp): string := match b with | Plus => "+" | Minus => "-" @@ -138,7 +112,7 @@ Module StringConversion <: Conversion Qhasm QhasmString. | Or => "|" end. - Definition rotOpToString (r: RotOp): string := + Coercion rotOpToString (r: RotOp): string := match r with | Shl => "<<" | Shr => ">>" @@ -146,41 +120,37 @@ Module StringConversion <: Conversion Qhasm QhasmString. | Rotr => ">>>" end. - Definition operationToString (o: Operation): string := + Definition operationToString (o: Operation): option string := match o with | OpReg32Constant b r c => - (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c) + r ++ " " ++ b ++ "= " ++ c | OpReg32Reg32 b r0 r1 => - (regToString r0) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString r1) + r0 ++ " " ++ b ++ "= " ++ r1 | RotReg32 o r i => - (regToString r) ++ " " ++ (rotOpToString o) ++ "= " ++ (constToString i) - + r ++ " " ++ o ++ "= " ++ i | OpReg64Constant b r c => - (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c) + r ++ " " ++ b ++ "= " ++ c | OpReg64Reg64 b r0 r1 => - (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c) - - | OpReg128Constant b r c => - (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c) - | OpReg128Reg128 b r0 r1 => - (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c) + r0 ++ " " ++ b ++ "= " ++ r1 + | _ => None end. - Definition testOpToString (t: TestOp): string := + Coercion testOpToString (t: TestOp): string := match t with - | TEq => - | TLt => - | TUnsignedLt => - | TGt => - | TUnsignedGt => + | TEq => "=" + | TLt => "<" + | TUnsignedLt => "unsigned<" + | TGt => ">" + | TUnsignedGt => "unsigned>" end. Definition conditionalToString (c: Conditional): string := + let f := fun (i: bool) => if i then "!" else "" in match c with - | TestTrue => - | TestFalse => - | TestReg32Reg32 o i r0 r1 => - | TestReg32Const o i r c => + | TestTrue => "" + | TestFalse => "" + | TestReg32Reg32 o i r0 r1 => (f i) ++ o ++ "?" ++ r0 ++ " " ++ r1 + | TestReg32Const o i r c =>(f i) ++ o ++ "?" ++ r ++ " " ++ c end. End Elements. @@ -188,9 +158,9 @@ Module StringConversion <: Conversion Qhasm QhasmString. Section Parsing. Inductive Entry := - | regEntry: forall n, Reg n => Entry - | stackEntry: forall n, Stack n => Entry - | constEntry: forall n, Const n => Entry. + | regEntry: forall n, Reg n -> Entry + | stackEntry: forall n, Stack n -> Entry + | constEntry: forall n, Const n -> Entry. Definition allRegs (prog: Qhasm.Program): list Entry := [(* TODO *)] |