diff options
-rw-r--r-- | src/Assembly/AlmostConversion.v | 51 | ||||
-rw-r--r-- | src/Assembly/AlmostQhasm.v | 57 | ||||
-rw-r--r-- | src/Assembly/Conversion.v | 19 | ||||
-rw-r--r-- | src/Assembly/GallinaConversion.v | 60 | ||||
-rw-r--r-- | src/Assembly/HighLevel.v | 9 | ||||
-rw-r--r-- | src/Assembly/Language.v | 7 | ||||
-rw-r--r-- | src/Assembly/Qhasm.v | 745 | ||||
-rw-r--r-- | src/Assembly/QhasmCommon.v | 157 | ||||
-rw-r--r-- | src/Assembly/QhasmEvalCommon.v | 334 | ||||
-rw-r--r-- | src/Assembly/QhasmExtraction.v | 24 | ||||
-rw-r--r-- | src/Assembly/QhasmUtil.v | 44 | ||||
-rw-r--r-- | src/Assembly/StringConversion.v | 30 |
12 files changed, 831 insertions, 706 deletions
diff --git a/src/Assembly/AlmostConversion.v b/src/Assembly/AlmostConversion.v new file mode 100644 index 000000000..16638af78 --- /dev/null +++ b/src/Assembly/AlmostConversion.v @@ -0,0 +1,51 @@ + +Require Import NArith. +Require Export Qhasm AlmostQhasm Conversion. + +Module AlmostConversion <: Conversion AlmostQhasm Qhasm. + Import QhasmCommon AlmostQhasm Qhasm. + Import ListNotations. + + Fixpoint almostToQhasm' (prog: AlmostProgram) (startLabel: N): Qhasm.Program := + let label0 := N.shiftl 1 startLabel in + let label1 := N.succ label0 in + + match prog with + | ASkip => [] + | ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1) + | AAssign a => [ QAssign a ] + | AOp a => [ QOp a ] + | ACond c a b => + let els := N.to_nat (N.shiftl 1 label0) in + let finish := S els in + [QJmp (invertConditional c) els] ++ + (almostToQhasm' a label1) ++ + [QJmp TestTrue finish] ++ + [QLabel els] ++ + (almostToQhasm' b label1) ++ + [QLabel finish] + | AWhile c a => + let start := N.to_nat (N.shiftl 1 label0) in + let finish := S start in + [ QJmp (invertConditional c) finish ; + QLabel start ] ++ + (almostToQhasm' a label1) ++ + [ QJmp c start; + QLabel finish ] + end. + + Definition convertProgram (prog: AlmostQhasm.Program) := Some (almostToQhasm' prog 0%N). + Definition convertState (st: Qhasm.State): option AlmostQhasm.State := Some st. + + Lemma convert_spec: forall st' prog, + match ((convertProgram prog), (convertState st')) with + | (Some prog', Some st) => + match (Qhasm.eval prog' st') with + | Some st'' => AlmostQhasm.eval prog st = (convertState st'') + | _ => True + end + | _ => True + end. + Admitted. + +End AlmostConversion. diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v new file mode 100644 index 000000000..31128fbfb --- /dev/null +++ b/src/Assembly/AlmostQhasm.v @@ -0,0 +1,57 @@ +Require Import QhasmEvalCommon. +Require Import Language. +Require Import List. + +Module AlmostQhasm <: Language. + Import ListNotations. + + (* A constant upper-bound on the number of operations we run *) + Definition maxOps: nat := 1000. + + (* Program Types *) + Definition State := State. + + Inductive AlmostProgram: Set := + | ASkip: AlmostProgram + | ASeq: AlmostProgram -> AlmostProgram -> AlmostProgram + | AAssign: Assignment -> AlmostProgram + | AOp: Operation -> AlmostProgram + | ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram + | AWhile: Conditional -> AlmostProgram -> AlmostProgram. + + Hint Constructors AlmostProgram. + + Definition Program := AlmostProgram. + + (* Only execute while loops a fixed number of times. + TODO (rsloan): can we do any better? *) + + (* TODO: make this inductive *) + Fixpoint almostEvalWhile (cond: Conditional) (prog: Program) (state: State) (horizon: nat): option State := + match horizon with + | (S m) => + if (evalCond cond state) + then almostEvalWhile cond prog state m + else Some state + | O => None + end. + + Fixpoint eval (prog: Program) (state: State): option State := + match prog with + | ASkip => Some state + | ASeq a b => + match (eval a state) with + | (Some st') => eval b st' + | _ => None + end + | AAssign a => Some (evalAssignment a state) + | AOp a => Some (evalOperation a state) + | ACond c a b => + if (evalCond c state) + then eval a state + else eval b state + | AWhile c a => almostEvalWhile c a state maxOps + end. + + (* world peace *) +End AlmostQhasm. diff --git a/src/Assembly/Conversion.v b/src/Assembly/Conversion.v new file mode 100644 index 000000000..eb378d437 --- /dev/null +++ b/src/Assembly/Conversion.v @@ -0,0 +1,19 @@ + +Require Export Language. + +Module Type Conversion (A B: Language). + + Parameter convertProgram: A.Program -> option B.Program. + Parameter convertState: B.State -> option A.State. + + Axiom convert_spec: forall st' prog, + match ((convertProgram prog), (convertState st')) with + | (Some prog', Some st) => + match (B.eval prog' st') with + | Some st'' => A.eval prog st = (convertState st'') + | _ => True + end + | _ => True + end. + +End Conversion. diff --git a/src/Assembly/GallinaConversion.v b/src/Assembly/GallinaConversion.v new file mode 100644 index 000000000..0419ec3e1 --- /dev/null +++ b/src/Assembly/GallinaConversion.v @@ -0,0 +1,60 @@ + +Require Export Language Conversion. +Require Export AlmostQhasm QhasmCommon. +Require Export Bedrock.Word. +Require Export List. +Require Vector. + +Module Type GallinaFunction <: Language. + Parameter len: nat. + Definition Vec := Vector.t (word 32) len. + + Definition Program := Vec -> Vec. + Definition State := Vec. + + Definition eval (p: Program) (s: Vec) := Some (p s). +End GallinaFunction. + +Module GallinaConversion (S: GallinaFunction) <: Conversion S AlmostQhasm. + Import QhasmCommon AlmostQhasm. + Import ListNotations. + Import S. + + Fixpoint convertState' (st: AlmostQhasm.State) (rem: nat): list (word 32) := + match rem with + | O => [] + | S m => + match (getStack (stack32 rem) st) with + | Some e => e + | None => (wzero 32) + end :: (convertState' st m) + end. + + Lemma convertState'_len: forall st rem, length (convertState' st rem) = rem. + Proof. + intros; induction rem; simpl; intuition. + Qed. + + Definition convertState (st: AlmostQhasm.State): option S.State. + unfold State, Vec. + replace len with (length (convertState' st len)) + by abstract (apply convertState'_len). + refine (Some (Vector.of_list (convertState' st len))). + Defined. + + (* TODO (rsloan): implement conversion *) + Definition convertProgram (prog: S.Program): option AlmostQhasm.Program := + Some ASkip. + + Lemma convert_spec: forall st' prog, + match ((convertProgram prog), (convertState st')) with + | (Some prog', Some st) => + match (AlmostQhasm.eval prog' st') with + | Some st'' => S.eval prog st = (convertState st'') + | _ => True + end + | _ => True + end. + Admitted. + +End GallinaConversion. diff --git a/src/Assembly/HighLevel.v b/src/Assembly/HighLevel.v deleted file mode 100644 index bae67f312..000000000 --- a/src/Assembly/HighLevel.v +++ /dev/null @@ -1,9 +0,0 @@ - -Inductive Const32 : Set = | const32: word 32 -> Const32. - -Inductive HL := - | Input: Const32 -> HL - | Variable: Const32 -> HL - | Let: forall m, nat -> HL -> HL -> HL - | Lift1: (Const32 -> Const32) -> HL -> HL - | Lift2: (Const32 -> Const32 -> Const32) -> HL -> HL -> HL. diff --git a/src/Assembly/Language.v b/src/Assembly/Language.v new file mode 100644 index 000000000..d04393b51 --- /dev/null +++ b/src/Assembly/Language.v @@ -0,0 +1,7 @@ + +Module Type Language. + Parameter Program: Type. + Parameter State: Type. + + Parameter eval: Program -> State -> option State. +End Language. diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v index 901554b19..05e607462 100644 --- a/src/Assembly/Qhasm.v +++ b/src/Assembly/Qhasm.v @@ -1,674 +1,73 @@ +Require Import QhasmEvalCommon. +Require Import Language. +Require Import List NPeano. + +Module Qhasm <: Language. + Import ListNotations. + + (* A constant upper-bound on the number of operations we run *) + Definition maxOps: nat := 1000. + Definition State := State. + + (* Program Types *) + Inductive QhasmStatement := + | QAssign: Assignment -> QhasmStatement + | QOp: Operation -> QhasmStatement + | QJmp: Conditional -> Label -> QhasmStatement + | QLabel: Label -> QhasmStatement. + + Hint Constructors QhasmStatement. + + Definition Program := list QhasmStatement. + + (* Only execute while loops a fixed number of times. + TODO (rsloan): can we do any better? *) + + Fixpoint getLabelMap' (prog: Program) (cur: LabelMap) (index: nat): LabelMap := + match prog with + | p :: ps => + match p with + | QLabel label => getLabelMap' ps (NatM.add label index cur) (S index) + | _ => getLabelMap' ps cur (S index) + end + | [] => cur + end. + + Definition getLabelMap (prog: Program): LabelMap := + getLabelMap' prog (NatM.empty nat) O. + + Fixpoint eval' (prog: Program) (state: State) (loc: nat) (horizon: nat) (labelMap: LabelMap) (maxLoc: nat): option State := + match horizon with + | (S h) => + match (nth_error prog loc) with + | Some stmt => + let (nextState, jmp) := + match stmt with + | QAssign a => (evalAssignment a state, None) + | QOp o => (evalOperation o state, None) + | QLabel l => (state, None) + | QJmp c l => + if (evalCond c state) + then (state, Some l) + else (state, None) + end + in + match jmp with + | None => + if (Nat.eq_dec loc maxLoc) + then Some nextState + else eval' prog nextState (S loc) h labelMap maxLoc + | Some nextLoc => + eval' prog nextState nextLoc h labelMap nextLoc + end + | None => None + end + | O => None + end. + + Definition eval (prog: Program) (state: State): option State := + eval' prog state O maxOps (getLabelMap prog) ((length prog) - 1). + + (* world peace *) +End Qhasm. -Require Import String List. -Require Import Bedrock.Word. -Require Import ZArith NArith NPeano. -Require Import Coq.Structures.OrderedTypeEx. - -Require Export FMapAVL FMapList. - -Module NatM := FMapAVL.Make(Nat_as_OT). -Definition DefMap: Type := NatM.t N. -Definition StateMap: Type := NatM.t DefMap. -Definition LabelMap: Type := NatM.t nat. - -(* A formalization of x86 qhasm *) - -(* Basic Types *) -Definition Label := nat. -Definition Index (limit: nat) := {x: nat | (x < limit)%nat}. -Definition Invert := bool. - -Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. -Coercion indexToNat : Index >-> nat. - -(* 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. - -Inductive Reg: nat -> Set := - | reg32: nat -> Reg 32 - | reg3232: nat -> Reg 64 - | reg6464: nat -> Reg 128 - | reg80: nat -> Reg 80. - -Inductive Stack: nat -> Set := - | stack32: nat -> Stack 32 - | stack64: nat -> Stack 64 - | stack128: nat -> Stack 128. - -(* Assignments *) -Inductive Assignment : Set := - | Assign32Stack32: Reg 32 -> Stack 32 -> Assignment - | Assign32Stack16: Reg 32 -> Stack 32 -> Index 2 -> Assignment - | Assign32Stack8: Reg 32 -> Stack 32 -> Index 4 -> Assignment - | Assign32Stack64: Reg 32 -> Stack 64 -> Index 2 -> Assignment - | Assign32Stack128: Reg 32 -> Stack 128 -> Index 2 -> Assignment - - | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment - | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment - | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment - | Assign32Reg64: Reg 32 -> Reg 64 -> Index 2 -> Assignment - | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment - - | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment - | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment - | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment - - | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment - | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment - | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment - - | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment - | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment - | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment - - | AssignConstant: Reg 32 -> Const 32 -> Assignment. - -Hint Constructors Assignment. - -(* Operations *) - -Inductive BinOp := - | Plus: BinOp | Minus: BinOp | Mult: BinOp - | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp. - -Inductive RotOp := - | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp. - -Inductive Operation := - | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation - | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation - | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation - - | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation - | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation - - | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation - | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation. - -Hint Constructors Operation. - -(* Control Flow *) - -Inductive TestOp := - | TEq: TestOp - | TLt: TestOp - | TUnsignedLt: TestOp - | TGt: TestOp - | TUnsignedGt: 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 => TestFalse - | TestReg32Reg32 o i r0 r1 => TestReg32Reg32 o (negb i) r0 r1 - | TestReg32Const o i r c => TestReg32Const o (negb i) r c - end. - -Hint Constructors Conditional. - -(* Program Types *) - -Inductive AlmostQhasm := - | ASeq: AlmostQhasm -> AlmostQhasm -> AlmostQhasm - | AAssign: Assignment -> AlmostQhasm - | AOp: Operation -> AlmostQhasm - | ACond: Conditional -> AlmostQhasm -> AlmostQhasm - | AWhile: Conditional -> AlmostQhasm -> AlmostQhasm. - -Hint Constructors AlmostQhasm. - -Inductive QhasmStatement := - | QAssign: Assignment -> QhasmStatement - | QOp: Operation -> QhasmStatement - | QJmp: Conditional -> Label -> QhasmStatement - | QLabel: Label -> QhasmStatement. - -Hint Constructors QhasmStatement. - -Definition Qhasm := list QhasmStatement. - -Import ListNotations. - -(* AlmostQhasm -> Qhasm Conversion *) - -Fixpoint almostToQhasm' (prog: AlmostQhasm) (startLabel: N): Qhasm := - let label0 := N.shiftl 1 startLabel in - let label1 := N.succ label0 in - - match prog with - | ASeq a b => (almostToQhasm' a label0) ++ (almostToQhasm' b label1) - | AAssign a => [ QAssign a ] - | AOp a => [ QOp a ] - | ACond c a => - [QJmp (invertConditional c) (N.to_nat label0)] ++ - (almostToQhasm' a label1) ++ - [QLabel (N.to_nat label0)] - | AWhile c a => - let start := N.to_nat (N.shiftl 1 label0) in - let finish := S start in - [ QJmp (invertConditional c) finish ; - QLabel start ] ++ - (almostToQhasm' a label1) ++ - [ QJmp c start; - QLabel finish ] - end. - -Definition almostToQhasm (prog: AlmostQhasm) := almostToQhasm' prog 0%N. - -(* Machine State *) - -Inductive State := -| fullState (regState: StateMap) (stackState: StateMap): State. - -Definition getReg {n} (reg: Reg n) (state: State): option (word n). - destruct state; inversion reg as [L H | L H | L H | L H]; - destruct (NatM.find n regState) as [map |]; - first [ destruct (NatM.find L map) as [n0 |] | exact None ]; - first [ rewrite H; exact (Some (NToWord n n0)) | exact None ]. -Defined. - -Definition setReg {n} (reg: Reg n) (value: word n) (state: State): State. - inversion state; inversion reg as [L H | L H | L H | L H]; - destruct (NatM.find n regState) as [map |]; - first [ - exact - (fullState - (NatM.add n - (NatM.add L (wordToN value) map) regState) - stackState) - | exact state ]. -Defined. - -Definition getStack {n} (entry: Stack n) (state: State): option (word n). - destruct state; inversion entry as [L H | L H | L H]; - destruct (NatM.find n stackState) as [map |]; - first [ destruct (NatM.find L map) as [n0 |] | exact None ]; - first [ rewrite H; exact (Some (NToWord n n0)) | exact None ]. -Defined. - -Definition setStack {n} (entry: Stack n) (value: word n) (state: State): State. - inversion state; inversion entry as [L H | L H | L H]; - destruct (NatM.find n stackState) as [map |]; - first [ - exact - (fullState regState - (NatM.add n - (NatM.add L (wordToN value) map) regState)) - | exact state ]. -Defined. - -Definition emptyState: State := - fullState (NatM.empty DefMap) (NatM.empty DefMap). - -(* Magical Bitwise Manipulations *) - -(* Force w to be m bits long, by truncation or zero-extension *) -Definition trunc {n} (m: nat) (w: word n): word m. - destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. - - - replace m with (n + (m - n)) by abstract intuition. - refine (zext w (m - n)). - - - rewrite <- s; assumption. - - - replace n with (m + (n - m)) in w by abstract intuition. - refine (split1 m (n-m) w). -Defined. - -(* Get the index-th m-bit block of w *) -Definition getIndex {n} (w: word n) (m index: nat): word m. - replace n with - ((min n (m * index)) + (n - (min n (m * index))))%nat - in w by abstract ( - assert ((min n (m * index)) <= n)%nat - by apply Nat.le_min_l; - intuition). - - refine - (trunc m - (split2 (min n (m * index)) (n - min n (m * index)) w)). -Defined. - -(* set the index-th m-bit block of w to s *) -Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n := - w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))) - ^| (trunc n (combine s (wzero (index * m)%nat))). - -(* State Evaluation *) - -Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool := - xorb invert - match o with - | TEq => weqb a b - | TLt => - match (Z.compare (wordToZ a) (wordToZ b)) with - | Lt => true - | _ => false - end - | TUnsignedLt => - match (N.compare (wordToN a) (wordToN b)) with - | Lt => true - | _ => false - end - | TGt => - match (Z.compare (wordToZ a) (wordToZ b)) with - | Gt => true - | _ => false - end - | TUnsignedGt => - match (N.compare (wordToN a) (wordToN b)) with - | Gt => true - | _ => false - end - end. - - -Definition evalCond (c: Conditional) (state: State): option bool := - match c with - | TestTrue => Some true - | TestFalse => Some false - | TestReg32Reg32 o i r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r0 state) with - | Some v1 => Some (evalTest o i v0 v1) - | _ => None - end - | _ => None - end - | TestReg32Const o i r x => - match (getReg r state) with - | Some v0 => - match x with - | const32 v1 => Some (evalTest o i v0 v1) - end - | _ => None - end - end. - -Definition evalBinOp {n} (o: BinOp) (a b: word n): word n := - match o with - | Plus => wplus a b - | Minus => wminus a b - | Mult => wmult a b - | Div => NToWord n ((wordToN a) / (wordToN b))%N - | Or => wor a b - | Xor => wxor a b - | And => wand a b - end. - -Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n := - match o with - | Shl => NToWord n (N.shiftl_nat (wordToN a) m) - | Shr => NToWord n (N.shiftr_nat (wordToN a) m) - - (* TODO (rsloan): not actually rotate operations *) - | Rotl => NToWord n (N.shiftl_nat (wordToN a) m) - | Rotr => NToWord n (N.shiftr_nat (wordToN a) m) - end. - -Definition evalOperation (o: Operation) (state: State): State := - match o with - | OpReg32Constant b r c => - match (getReg r state) with - | Some v0 => - match c with - | const32 v1 => setReg r (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - | OpReg32Reg32 b r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - | RotReg32 b r m => - match (getReg r state) with - | Some v0 => setReg r (evalRotOp b v0 m) state - | None => state - end - - | OpReg64Constant b r c => - match (getReg r state) with - | Some v0 => - match c with - | const64 v1 => setReg r (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - | OpReg64Reg64 b r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - - | OpReg128Constant b r c => - match (getReg r state) with - | Some v0 => - match c with - | const128 v1 => setReg r (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - | OpReg128Reg128 b r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (evalBinOp b v0 v1) state - | _ => state - end - | None => state - end - end. - -Definition evalAssignment (a: Assignment) (state: State): State := - match a with - | Assign32Stack32 r s => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r v1 state - | _ => state - end - | None => state - end - | Assign32Stack16 r s i => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r (trunc 32 (getIndex v1 16 i)) state - | _ => state - end - | None => state - end - | Assign32Stack8 r s i => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r (trunc 32 (getIndex v1 8 i)) state - | _ => state - end - | None => state - end - | Assign32Stack64 r s i => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r (getIndex v1 32 i) state - | _ => state - end - | None => state - end - | Assign32Stack128 r s i => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r (getIndex v1 32 i) state - | _ => state - end - | None => state - end - - | Assign32Reg32 r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 v1 state - | _ => state - end - | None => state - end - | Assign32Reg16 r0 r1 i => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (trunc 32 (getIndex v1 16 i)) state - | _ => state - end - | None => state - end - | Assign32Reg8 r0 r1 i => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (trunc 32 (getIndex v1 8 i)) state - | _ => state - end - | None => state - end - | Assign32Reg64 r0 r1 i => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (getIndex v1 32 i) state - | _ => state - end - | None => state - end - | Assign32Reg128 r0 r1 i => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (getIndex v1 32 i) state - | _ => state - end - | None => state - end - - | Assign3232Stack32 r0 i s => - match (getReg r0 state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r0 (setInPlace v0 v1 i) state - | _ => state - end - | None => state - end - - | Assign3232Stack64 r s => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r v1 state - | _ => state - end - | None => state - end - - | Assign3232Stack128 r s i => - match (getReg r state) with - | Some v0 => - match (getStack s state) with - | Some v1 => setReg r (getIndex v1 64 i) state - | _ => state - end - | None => state - end - - | Assign3232Reg32 r0 i r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (setInPlace v0 v1 i) state - | _ => state - end - | None => state - end - - | Assign3232Reg64 r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 v1 state - | _ => state - end - | None => state - end - - | Assign3232Reg128 r0 r1 i => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (getIndex v1 64 i) state - | _ => state - end - | None => state - end - - | Assign6464Reg32 r0 i r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (setInPlace v0 v1 i) state - | _ => state - end - | None => state - end - - | Assign6464Reg64 r0 i r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 (setInPlace v0 v1 i) state - | _ => state - end - | None => state - end - - | Assign6464Reg128 r0 r1 => - match (getReg r0 state) with - | Some v0 => - match (getReg r1 state) with - | Some v1 => setReg r0 v1 state - | _ => state - end - | None => state - end - - | AssignConstant r c => - match (getReg r state) with - | Some v0 => - match c with - | const32 v1 => setReg r v1 state - | _ => state - end - | None => state - end - end. - -(* AlmostQhasm Evaluation *) - - -(* Only execute while loops a fixed number of times. - TODO (rsloan): can we do any better? *) - -Fixpoint almostEvalWhile (cond: Conditional) (prog: AlmostQhasm) (state: State) (horizon: nat): State := - match horizon with - | (S m) => - if (evalCond cond state) - then almostEvalWhile cond prog state m - else state - | O => state - end. - -Fixpoint almostEval (prog: AlmostQhasm) (state: State): State := - match prog with - | ASeq a b => almostEval b (almostEval a state) - | AAssign a => evalAssignment a state - | AOp a => evalOperation a state - | ACond c a => - if (evalCond c state) - then almostEval a state - else state - | AWhile c a => almostEvalWhile c a state maxOps - end. - -Definition almostEvalReg {n} (prog: AlmostQhasm) (reg: Reg n): option (word n) := - getReg reg (almostEval prog emptyState). - -Definition almostEvalStack {n} (prog: AlmostQhasm) (stack: Stack n): option (word n) := - getStack stack (almostEval prog emptyState). - -(* Qhasm Evaluation *) - -Fixpoint getLabelMap' (prog: Qhasm) (cur: LabelMap) (index: nat): LabelMap := - match prog with - | p :: ps => - match p with - | QLabel label => getLabelMap' ps (NatM.add label index cur) (S index) - | _ => getLabelMap' ps cur (S index) - end - | [] => cur - end. - -Definition getLabelMap (prog: Qhasm): LabelMap := - getLabelMap' prog (NatM.empty nat) O. - -Fixpoint eval' (prog: Qhasm) (state: State) (loc: nat) (horizon: nat) (labelMap: LabelMap) (maxLoc: nat): option State := - match horizon with - | (S h) => - match (nth_error prog loc) with - | Some stmt => - let (nextState, jmp) := - match stmt with - | QAssign a => (evalAssignment a state, None) - | QOp o => (evalOperation o state, None) - | QLabel l => (state, None) - | QJmp c l => - if (evalCond c state) - then (state, Some l) - else (state, None) - end - in - match jmp with - | None => - if (Nat.eq_dec loc maxLoc) - then Some nextState - else eval' prog nextState (S loc) h labelMap maxLoc - | Some nextLoc => - eval' prog nextState nextLoc h labelMap nextLoc - end - | None => None - end - | O => None - end. - -Definition eval (prog: Qhasm) (state: State): option State := - eval' prog state O maxOps (getLabelMap prog) ((length prog) - 1). - -Definition evalReg {n} (prog: Qhasm) (reg: Reg n): option (word n) := - match (eval prog emptyState) with - | Some st => getReg reg st - | None => None - end. - -Definition evalStack {n} (prog: Qhasm) (stack: Stack n): option (word n) := - match (eval prog emptyState) with - | Some st => getStack stack st - | None => None - end. - -(* world peace *) diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v new file mode 100644 index 000000000..2d3567a44 --- /dev/null +++ b/src/Assembly/QhasmCommon.v @@ -0,0 +1,157 @@ +Require Export String List. +Require Export Bedrock.Word. + +Require Import ZArith NArith NPeano. +Require Import Coq.Structures.OrderedTypeEx. +Require Import FMapAVL FMapList. + +Require Import QhasmUtil. + +Module NatM := FMapAVL.Make(Nat_as_OT). +Definition DefMap: Type := NatM.t N. +Definition StateMap: Type := NatM.t DefMap. +Definition LabelMap: Type := NatM.t nat. + +(* A formalization of x86 qhasm *) + +(* 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. + +Inductive Reg: nat -> Set := + | reg32: nat -> Reg 32 + | reg3232: nat -> Reg 64 + | reg6464: nat -> Reg 128 + | reg80: nat -> Reg 80. + +Inductive Stack: nat -> Set := + | stack32: nat -> Stack 32 + | stack64: nat -> Stack 64 + | stack128: nat -> Stack 128. + +(* Assignments *) +Inductive Assignment : Set := + | Assign32Stack32: Reg 32 -> Stack 32 -> Assignment + | Assign32Stack16: Reg 32 -> Stack 32 -> Index 2 -> Assignment + | Assign32Stack8: Reg 32 -> Stack 32 -> Index 4 -> Assignment + | Assign32Stack64: Reg 32 -> Stack 64 -> Index 2 -> Assignment + | Assign32Stack128: Reg 32 -> Stack 128 -> Index 2 -> Assignment + + | Assign32Reg32: Reg 32 -> Reg 32 -> Assignment + | Assign32Reg16: Reg 32 -> Reg 32 -> Index 2 -> Assignment + | Assign32Reg8: Reg 32 -> Reg 32 -> Index 4 -> Assignment + | Assign32Reg64: Reg 32 -> Reg 64 -> Index 2 -> Assignment + | Assign32Reg128: Reg 32 -> Reg 128 -> Index 4 -> Assignment + + | Assign3232Stack32: Reg 64 -> Index 2 -> Stack 32 -> Assignment + | Assign3232Stack64: Reg 64 -> Stack 64 -> Assignment + | Assign3232Stack128: Reg 64 -> Stack 128 -> Index 2 -> Assignment + + | Assign3232Reg32: Reg 64 -> Index 2 -> Reg 32 -> Assignment + | Assign3232Reg64: Reg 64 -> Reg 64 -> Assignment + | Assign3232Reg128: Reg 64 -> Reg 128 -> Index 2 -> Assignment + + | Assign6464Reg32: Reg 128 -> Index 4 -> Reg 32 -> Assignment + | Assign6464Reg64: Reg 128 -> Index 2 -> Reg 64 -> Assignment + | Assign6464Reg128: Reg 128 -> Reg 128 -> Assignment + + | AssignConstant: Reg 32 -> Const 32 -> Assignment. + +Hint Constructors Assignment. + +(* Operations *) + +Inductive BinOp := + | Plus: BinOp | Minus: BinOp | Mult: BinOp + | Div: BinOp | Xor: BinOp | And: BinOp | Or: BinOp. + +Inductive RotOp := + | Shl: RotOp | Shr: RotOp | Rotl: RotOp | Rotr: RotOp. + +Inductive Operation := + | OpReg32Constant: BinOp -> Reg 32 -> Const 32 -> Operation + | OpReg32Reg32: BinOp -> Reg 32 -> Reg 32 -> Operation + | RotReg32: RotOp -> Reg 32 -> Index 32 -> Operation + + | OpReg64Constant: BinOp -> Reg 64 -> Const 64 -> Operation + | OpReg64Reg64: BinOp -> Reg 64 -> Reg 64 -> Operation + + | OpReg128Constant: BinOp -> Reg 128 -> Const 32 -> Operation + | OpReg128Reg128: BinOp -> Reg 128 -> Reg 128 -> Operation. + +Hint Constructors Operation. + +(* Control Flow *) + +Inductive TestOp := + | TEq: TestOp + | TLt: TestOp + | TUnsignedLt: TestOp + | TGt: TestOp + | TUnsignedGt: 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. + +Hint Constructors Conditional. + +(* Machine State *) + +Inductive State := +| fullState (regState: StateMap) (stackState: StateMap): State. + +Definition getReg {n} (reg: Reg n) (state: State): option (word n). + destruct state; inversion reg as [L H | L H | L H | L H]; + destruct (NatM.find n regState) as [map |]; + first [ destruct (NatM.find L map) as [n0 |] | exact None ]; + first [ rewrite H; exact (Some (NToWord n n0)) | exact None ]. +Defined. + +Definition setReg {n} (reg: Reg n) (value: word n) (state: State): State. + inversion state; inversion reg as [L H | L H | L H | L H]; + destruct (NatM.find n regState) as [map |]; + first [ + exact + (fullState + (NatM.add n + (NatM.add L (wordToN value) map) regState) + stackState) + | exact state ]. +Defined. + +Definition getStack {n} (entry: Stack n) (state: State): option (word n). + destruct state; inversion entry as [L H | L H | L H]; + destruct (NatM.find n stackState) as [map |]; + first [ destruct (NatM.find L map) as [n0 |] | exact None ]; + first [ rewrite H; exact (Some (NToWord n n0)) | exact None ]. +Defined. + +Definition setStack {n} (entry: Stack n) (value: word n) (state: State): State. + inversion state; inversion entry as [L H | L H | L H]; + destruct (NatM.find n stackState) as [map |]; + first [ + exact + (fullState regState + (NatM.add n + (NatM.add L (wordToN value) map) regState)) + | exact state ]. +Defined. + +Definition emptyState: State := + fullState (NatM.empty DefMap) (NatM.empty DefMap). diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v new file mode 100644 index 000000000..312f30e03 --- /dev/null +++ b/src/Assembly/QhasmEvalCommon.v @@ -0,0 +1,334 @@ +Require Export QhasmCommon. +Require Export QhasmUtil. + +Require Export ZArith. + +Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool := + xorb invert + match o with + | TEq => weqb a b + | TLt => + match (Z.compare (wordToZ a) (wordToZ b)) with + | Lt => true + | _ => false + end + | TUnsignedLt => + match (N.compare (wordToN a) (wordToN b)) with + | Lt => true + | _ => false + end + | TGt => + match (Z.compare (wordToZ a) (wordToZ b)) with + | Gt => true + | _ => false + end + | TUnsignedGt => + match (N.compare (wordToN a) (wordToN b)) with + | Gt => true + | _ => false + end + end. + +Definition evalCond (c: Conditional) (state: State): option bool := + match c with + | TestTrue => Some true + | TestFalse => Some false + | TestReg32Reg32 o i r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r0 state) with + | Some v1 => Some (evalTest o i v0 v1) + | _ => None + end + | _ => None + end + | TestReg32Const o i r x => + match (getReg r state) with + | Some v0 => + match x with + | const32 v1 => Some (evalTest o i v0 v1) + end + | _ => None + end + end. + +Definition evalBinOp {n} (o: BinOp) (a b: word n): word n := + match o with + | Plus => wplus a b + | Minus => wminus a b + | Mult => wmult a b + | Div => NToWord n ((wordToN a) / (wordToN b))%N + | Or => wor a b + | Xor => wxor a b + | And => wand a b + end. + +Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n := + match o with + | Shl => NToWord n (N.shiftl_nat (wordToN a) m) + | Shr => NToWord n (N.shiftr_nat (wordToN a) m) + + (* TODO (rsloan): not actually rotate operations *) + | Rotl => NToWord n (N.shiftl_nat (wordToN a) m) + | Rotr => NToWord n (N.shiftr_nat (wordToN a) m) + end. + +Definition evalOperation (o: Operation) (state: State): State := + match o with + | OpReg32Constant b r c => + match (getReg r state) with + | Some v0 => + match c with + | const32 v1 => setReg r (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + | OpReg32Reg32 b r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + | RotReg32 b r m => + match (getReg r state) with + | Some v0 => setReg r (evalRotOp b v0 m) state + | None => state + end + + | OpReg64Constant b r c => + match (getReg r state) with + | Some v0 => + match c with + | const64 v1 => setReg r (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + | OpReg64Reg64 b r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + + | OpReg128Constant b r c => + match (getReg r state) with + | Some v0 => + match c with + | const128 v1 => setReg r (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + | OpReg128Reg128 b r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (evalBinOp b v0 v1) state + | _ => state + end + | None => state + end + end. + +Definition evalAssignment (a: Assignment) (state: State): State := + match a with + | Assign32Stack32 r s => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r v1 state + | _ => state + end + | None => state + end + | Assign32Stack16 r s i => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r (trunc 32 (getIndex v1 16 i)) state + | _ => state + end + | None => state + end + | Assign32Stack8 r s i => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r (trunc 32 (getIndex v1 8 i)) state + | _ => state + end + | None => state + end + | Assign32Stack64 r s i => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r (getIndex v1 32 i) state + | _ => state + end + | None => state + end + | Assign32Stack128 r s i => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r (getIndex v1 32 i) state + | _ => state + end + | None => state + end + + | Assign32Reg32 r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 v1 state + | _ => state + end + | None => state + end + | Assign32Reg16 r0 r1 i => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (trunc 32 (getIndex v1 16 i)) state + | _ => state + end + | None => state + end + | Assign32Reg8 r0 r1 i => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (trunc 32 (getIndex v1 8 i)) state + | _ => state + end + | None => state + end + | Assign32Reg64 r0 r1 i => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (getIndex v1 32 i) state + | _ => state + end + | None => state + end + | Assign32Reg128 r0 r1 i => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (getIndex v1 32 i) state + | _ => state + end + | None => state + end + + | Assign3232Stack32 r0 i s => + match (getReg r0 state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r0 (setInPlace v0 v1 i) state + | _ => state + end + | None => state + end + + | Assign3232Stack64 r s => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r v1 state + | _ => state + end + | None => state + end + + | Assign3232Stack128 r s i => + match (getReg r state) with + | Some v0 => + match (getStack s state) with + | Some v1 => setReg r (getIndex v1 64 i) state + | _ => state + end + | None => state + end + + | Assign3232Reg32 r0 i r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (setInPlace v0 v1 i) state + | _ => state + end + | None => state + end + + | Assign3232Reg64 r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 v1 state + | _ => state + end + | None => state + end + + | Assign3232Reg128 r0 r1 i => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (getIndex v1 64 i) state + | _ => state + end + | None => state + end + + | Assign6464Reg32 r0 i r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (setInPlace v0 v1 i) state + | _ => state + end + | None => state + end + + | Assign6464Reg64 r0 i r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 (setInPlace v0 v1 i) state + | _ => state + end + | None => state + end + + | Assign6464Reg128 r0 r1 => + match (getReg r0 state) with + | Some v0 => + match (getReg r1 state) with + | Some v1 => setReg r0 v1 state + | _ => state + end + | None => state + end + + | AssignConstant r c => + match (getReg r state) with + | Some v0 => + match c with + | const32 v1 => setReg r v1 state + | _ => state + end + | None => state + end + end. diff --git a/src/Assembly/QhasmExtraction.v b/src/Assembly/QhasmExtraction.v deleted file mode 100644 index 0584553fc..000000000 --- a/src/Assembly/QhasmExtraction.v +++ /dev/null @@ -1,24 +0,0 @@ - - -(* -- Define an evaluation function over the QH type, which can be terribly inefficient. This function will be parametrized in the following way: - - evalReg x InputRegs OutputRegs - evalStack x InputStack OutputStack - -Then, produce a lemma which shows that evaluating a given QH will perform an appropriate register operation. This will not check side-effects, which should be okay since we’re synthesizing in a very controlled manner. - -- Work on {x: QH | eval x _ _ = AST}, like the bounding code - -- Introduce all Inputs as StackX - -- Replace upward as: - - + Lifted functions by lemma (as above) - + Conditionals as QCond, by lemma - -- Then we can convert to string: - - + We can introduce stack inputs, etc. by traversing the AST - + QSeq, QStatement, QAssign are convertible directly - + QCond, QWhile are fixed assembly wrappers *)
\ No newline at end of file diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v new file mode 100644 index 000000000..0528d0738 --- /dev/null +++ b/src/Assembly/QhasmUtil.v @@ -0,0 +1,44 @@ + +Require Import ZArith NArith NPeano. +Require Export Bedrock.Word. + +Definition Label := nat. +Definition Index (limit: nat) := {x: nat | (x < limit)%nat}. +Definition Invert := bool. + +Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. +Coercion indexToNat : Index >-> nat. + +(* Magical Bitwise Manipulations *) + +(* Force w to be m bits long, by truncation or zero-extension *) +Definition trunc {n} (m: nat) (w: word n): word m. + destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. + + - replace m with (n + (m - n)) by abstract intuition. + refine (zext w (m - n)). + + - rewrite <- s; assumption. + + - replace n with (m + (n - m)) in w by abstract intuition. + refine (split1 m (n-m) w). +Defined. + +(* Get the index-th m-bit block of w *) +Definition getIndex {n} (w: word n) (m index: nat): word m. + replace n with + ((min n (m * index)) + (n - (min n (m * index))))%nat + in w by abstract ( + assert ((min n (m * index)) <= n)%nat + by apply Nat.le_min_l; + intuition). + + refine + (trunc m + (split2 (min n (m * index)) (n - min n (m * index)) w)). +Defined. + +(* set the index-th m-bit block of w to s *) +Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n := + w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))) + ^| (trunc n (combine s (wzero (index * m)%nat))). diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v new file mode 100644 index 000000000..0504ed3a6 --- /dev/null +++ b/src/Assembly/StringConversion.v @@ -0,0 +1,30 @@ +Require Export Qhasm Language Conversion. +Require Export String. + +Module QhasmString <: Language. + Definition Program := string. + Definition State := unit. + + Definition eval (p: Program) (s: State): option State := Some tt. +End QhasmString. + +Module StringConversion <: Conversion Qhasm QhasmString. + + Definition convertState (st: QhasmString.State): option Qhasm.State := None. + + (* TODO (rsloan): Actually implement string conversion *) + Definition convertProgram (prog: Qhasm.Program): option string := + Some EmptyString. + + Lemma convert_spec: forall st' prog, + match ((convertProgram prog), (convertState st')) with + | (Some prog', Some st) => + match (QhasmString.eval prog' st') with + | Some st'' => Qhasm.eval prog st = (convertState st'') + | _ => True + end + | _ => True + end. + Admitted. + +End StringConversion. |