From 822dbd33db307584d76fb49b300f31b606613e38 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Thu, 26 May 2016 22:18:07 -0400 Subject: Major language refactoring to support Memory and AddWithCarry --- src/Assembly/AlmostQhasm.v | 25 +++++++++- src/Assembly/Medial.v | 104 ++++++++++++++++++++++++++++++++--------- src/Assembly/Pseudo.v | 114 ++++++++++++++++++++------------------------- src/Assembly/Qhasm.v | 1 - 4 files changed, 155 insertions(+), 89 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v index 929eeaba5..d50e3a6bd 100644 --- a/src/Assembly/AlmostQhasm.v +++ b/src/Assembly/AlmostQhasm.v @@ -15,12 +15,30 @@ Module AlmostQhasm <: Language. | AAssign: Assignment -> AlmostProgram | AOp: Operation -> AlmostProgram | ACond: Conditional -> AlmostProgram -> AlmostProgram -> AlmostProgram - | AWhile: Conditional -> AlmostProgram -> AlmostProgram. + | AWhile: Conditional -> AlmostProgram -> AlmostProgram + | ADef: Label -> AlmostProgram -> AlmostProgram -> AlmostProgram + | ACall: Label -> AlmostProgram. Hint Constructors AlmostProgram. Definition Program := AlmostProgram. + Fixpoint inline (l: nat) (f prog: AlmostProgram) := + match prog with + | ASeq a b => ASeq (inline l f a) (inline l f b) + | ACond c a b => ACond c (inline l f a) (inline l f b) + | AWhile c a => AWhile c (inline l f a) + | ADef l' f' p' => + if (Nat.eq_dec l l') + then prog + else ADef l' (inline l f f') (inline l f p') + | ACall l' => + if (Nat.eq_dec l l') + then f + else prog + | _ => prog + end. + Inductive AlmostEval: AlmostProgram -> State -> State -> Prop := | AESkip: forall s, AlmostEval ASkip s s | AESeq: forall p p' s s' s'', @@ -48,7 +66,10 @@ Module AlmostQhasm <: Language. -> AlmostEval (AWhile c a) s s'' | AEWhileSkip: forall c a s, evalCond c s = Some false - -> AlmostEval (AWhile c a) s s. + -> AlmostEval (AWhile c a) s s + | AEFun: forall l f p s s', + AlmostEval (inline l f p) s s' + -> AlmostEval (ADef l f p) s s'. Definition evaluatesTo := AlmostEval. diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v index aea77932d..90f6afd73 100644 --- a/src/Assembly/Medial.v +++ b/src/Assembly/Medial.v @@ -10,15 +10,24 @@ Module Medial (M: PseudoMachine) <: Language. Definition W := word width. (* Program Types *) - Definition State := DefMap. + Definition State := (NatNMap * PairNMap * (option bool))%type. + + Definition varS (st: State) := fst (fst st). + Definition memS (st: State) := snd (fst st). + Definition carryS (st: State) := snd st. + + Definition var (i: nat) (st: State) := NatM.find i (varS st). + Definition mem (v i: nat) (st: State) := PairM.find (v, i) (memS st). Inductive MAssignment : Type := | MAVar: nat -> nat -> MAssignment + | MAMem: nat -> nat -> nat -> MAssignment | MAConst: nat -> W -> MAssignment. Inductive MOperation := | MIOpConst: IntOp -> nat -> W -> MOperation | MIOpReg: IntOp -> nat -> nat -> MOperation + | MCOpReg: CarryOp -> nat -> nat -> MOperation | MDOpReg: DualOp -> nat -> nat -> option nat -> MOperation | MOpRot: RotOp -> nat -> Index width -> MOperation. @@ -31,65 +40,112 @@ Module Medial (M: PseudoMachine) <: Language. | MAssign: MAssignment -> Medial | MOp: MOperation -> Medial | MCond: MConditional -> Medial -> Medial -> Medial - | MFunexp: nat -> Medial -> Medial. + | MFunexp: nat -> Medial -> Medial + | MDef: nat -> Medial -> Medial -> Medial + | MCall: nat -> Medial. Definition Program := Medial. + Fixpoint inline (l: nat) (f p: Medial) := + match p with + | MSeq a b => MSeq (inline l f a) (inline l f b) + | MCond c a b => MCond c (inline l f a) (inline l f b) + | MFunexp e a => MFunexp e (inline l f a) + | MDef l' f' p' => + if (Nat.eq_dec l l') + then p + else MDef l' (inline l f f') (inline l f p') + | MCall l' => + if (Nat.eq_dec l l') + then f + else p + | _ => p + end. + + Fixpoint inlineAll (p: Medial) := + match p with + | MSeq a b => MSeq (inlineAll a) (inlineAll b) + | MCond c a b => MCond c (inlineAll a) (inlineAll b) + | MFunexp e a => MFunexp e (inlineAll a) + | MDef l' f' p' => inline l' f' (inlineAll p') + | _ => p + end. + Fixpoint meval (m: Medial) (st: State): option State := let omap := fun {A B} (x: option A) (f: A -> option B) => match x with | Some y => f y | _ => None end in + match m with | MSkip => Some st + | MSeq a b => omap (meval a st) (fun s => meval b s) + | MAssign a => match a with | MAVar x y => - match (NatM.find y st) with - | (Some v) => Some (NatM.add x v st) + match (var y st) with + | Some v => Some (NatM.add x v (varS st), memS st, carryS st) | _ => None end - | MAConst x c => Some (NatM.add x (wordToN c) st) + + | MAMem x y i => + match (mem y i st) with + | Some v => Some (NatM.add x v (varS st), memS st, carryS st) + | _ => None + end + + | MAConst x c => Some (NatM.add x (wordToN c) (varS st), memS st, carryS st) end + | MOp o => match o with | MIOpConst io a c => - omap (NatM.find a st) (fun v => - let res := evalIOp io (NToWord _ v) c in - Some (NatM.add a (wordToN res) st)) + omap (var a st) (fun v => + let (res, c') := evalIntOp io (NToWord _ v) c in + Some (NatM.add a (wordToN res) (varS st), memS st, c')) | MIOpReg io a b => - omap (NatM.find a st) (fun va => - omap (NatM.find b st) (fun vb => - let res := evalIOp io (NToWord width va) (NToWord width vb) in - Some (NatM.add a (wordToN res) st))) + omap (var a st) (fun va => + omap (var b st) (fun vb => + let (res, c') := evalIntOp io (NToWord width va) (NToWord width vb) in + Some (NatM.add a (wordToN res) (varS st), memS st, c'))) + + | MCOpReg o a b => + omap (var a st) (fun va => + omap (var b st) (fun vb => + let c := match (carryS st) with | Some b => b | _ => false end in + let (res, c') := evalCarryOp o (NToWord width va) (NToWord width vb) c in + Some (NatM.add a (wordToN res) (varS st), memS st, Some c'))) | MDOpReg duo a b (Some x) => - omap (NatM.find a st) (fun va => - omap (NatM.find b st) (fun vb => + omap (var a st) (fun va => + omap (var b st) (fun vb => let res := evalDualOp duo (NToWord width va) (NToWord width vb) in Some (NatM.add a (wordToN (fst res)) - (NatM.add x (wordToN (snd res)) st)))) + (NatM.add x (wordToN (snd res)) (varS st)), memS st, carryS st))) | MDOpReg duo a b None => - omap (NatM.find a st) (fun va => - omap (NatM.find b st) (fun vb => + omap (var a st) (fun va => + omap (var b st) (fun vb => let res := evalDualOp duo (NToWord width va) (NToWord width vb) in - Some (NatM.add a (wordToN (fst res)) st))) + Some (NatM.add a (wordToN (fst res)) (varS st), memS st, carryS st))) | MOpRot ro a x => - omap (NatM.find a st) (fun v => + omap (var a st) (fun v => let res := evalRotOp ro (NToWord width v) (proj1_sig x) in - Some (NatM.add a (wordToN res) st)) + Some (NatM.add a (wordToN res) (varS st), memS st, carryS st)) end + | MCond c a b => match c with | MC t x y => - omap (NatM.find x st) (fun vx => - omap (NatM.find y st) (fun vy => + omap (var x st) (fun vx => + omap (var y st) (fun vy => if (evalTest t (NToWord width vx) (NToWord width vy)) then meval a st else meval b st)) end + | MFunexp n a => (fix fexp (m: nat) (f: State -> option State) (s: State) := match m with @@ -101,9 +157,11 @@ Module Medial (M: PseudoMachine) <: Language. end end ) n (meval a) st + + | _ => None end. - Definition evaluatesTo := fun m st0 st1 => meval m st0 = Some st1. + Definition evaluatesTo := fun m st0 st1 => meval (inlineAll m) st0 = Some st1. (* world peace *) End Medial. diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index 6bb619910..af5dd3891 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,11 +1,11 @@ -Require Import QhasmEvalCommon QhasmUtil. +Require Import QhasmEvalCommon QhasmUtil State. Require Import Language. Require Import List. Module Type PseudoMachine. Parameter width: nat. Parameter vars: nat. - Parameter width_spec: ISize width. + Parameter width_spec: Width width. End PseudoMachine. Module Pseudo (M: PseudoMachine) <: Language. @@ -14,104 +14,90 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition const: Type := word width. (* Program Types *) - Definition State := list const. + Definition State := ((list const) * (list (list const)) * (option bool))%type. + + Definition var (st: State) := fst (fst st). + Definition mem (st: State) := snd (fst st). + Definition carry (st: State) := snd st. Inductive Pseudo: nat -> nat -> Type := | PVar: forall n, Index n -> Pseudo n 1 + | PMem: forall n m, Index n -> Index m -> Pseudo n 1 | PConst: forall n, const -> Pseudo n 1 | PBin: forall n, IntOp -> Pseudo n 2 -> Pseudo n 1 | PDual: forall n, DualOp -> Pseudo n 2 -> Pseudo n 2 + | PCarry: forall n, CarryOp -> Pseudo n 2 -> Pseudo n 1 | PShift: forall n, RotOp -> Index width -> Pseudo n 1 -> Pseudo n 1 + | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m + | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n + | PLet: forall n k m, Pseudo n k -> Pseudo (n + k) m -> Pseudo n m | PComb: forall n a b, Pseudo n a -> Pseudo n b -> Pseudo n (a + b) - - | PIf: forall n m, TestOp -> Index n -> Index n -> Pseudo n m -> Pseudo n m -> Pseudo n m - | PFunExp: forall n, Pseudo n n -> nat -> Pseudo n n. + | PCall: forall n m, Pseudo n m -> Pseudo n m. Hint Constructors Pseudo. Definition Program := Pseudo vars vars. - Definition applyBin (op: IntOp) (a b: word width): const := - match op with - | IPlus => wplus a b - | IMinus => wminus a b - | IAnd => wand a b - | IXor => wxor a b - | IOr => wor a b - end. - - Definition applyDual (op: DualOp) (a b: word width): list const := - match op with - | Wmult => - let wres := natToWord (width + width) - (N.to_nat ((wordToN a) * (wordToN b))) in - [split1 _ _ wres; split2 _ _ wres] - end. - - Definition applyShift (op: RotOp) (v: const) (n: Index width): const. - refine match op with - | Shl => convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _ - | Shr => convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _ - end; abstract ( - unfold const; - destruct n; simpl; - replace (width - x + x) with width; - replace (x + (width - x)) with width; - intuition ). - Defined. - Fixpoint pseudoEval {n m} (prog: Pseudo n m) (st: State): option State := - let option_map' := fun {A B: Type} (x: option A) (f: A -> option B) => - match x with - | Some x' => - match (f x') with - | Some res => Some res - | None => None - end - | _ => None - end in - match prog with - | PVar n i => option_map' (nth_error st i) (fun x => Some [x]) - | PConst n c => Some ([c]) + | PVar n i => + omap (nth_error (var st) i) (fun x => + Some ([x], mem st, carry st)) + + | PMem n m v i => + omap (nth_error (mem st) v) (fun vec => + omap (nth_error vec i) (fun x => + Some ([x], mem st, carry st))) + + | PConst n c => Some ([c], mem st, carry st) | PBin n o p => - option_map' (pseudoEval p st) (fun sp => + omap (pseudoEval p st) (fun sp => match sp with - | [wa; wb] => Some [applyBin o wa wb] + | ([wa; wb], m', _) => + let (v, c) := evalIntOp o wa wb in Some ([v], m', c) + | _ => None + end) + + | PCarry n o p => + omap (pseudoEval p st) (fun sp => + match sp with + | ([wa; wb], m', Some c) => + let (v, c') := evalCarryOp o wa wb c in Some ([v], m', Some c') | _ => None end) | PDual n o p => - option_map' (pseudoEval p st) (fun sp => + omap (pseudoEval p st) (fun sp => match sp with - | [wa; wb] => Some (applyDual o wa wb) + | ([wa; wb], m', co) => + let (low, high) := evalDualOp o wa wb in Some ([low; high], m', co) | _ => None end) | PShift n o a x => - option_map' (pseudoEval x st) (fun sx => + omap (pseudoEval x st) (fun sx => match sx with - | [wx] => Some [applyShift o wx a] + | ([wx], m', co) => Some ([evalRotOp o wx a], m', co) | _ => None end) | PLet n k m f g => - option_map' (pseudoEval f st) (fun sf => - option_map' (pseudoEval g (st ++ sf)) + omap (pseudoEval f st) (fun sf => + omap (pseudoEval g ((var st) ++ (var sf), mem sf, carry sf)) (fun sg => Some sg)) | PComb n a b f g => - option_map' (pseudoEval f st) (fun sf => - option_map' (pseudoEval g st) (fun sg => - Some (sf ++ sg))) + omap (pseudoEval f st) (fun sf => + omap (pseudoEval g st) (fun sg => + Some ((var sf) ++ (var sg), mem sg, carry sg))) | PIf n m t i0 i1 l r => - option_map' (nth_error st i0) (fun v0 => - option_map' (nth_error st i1) (fun v1 => + omap (nth_error (var st) i0) (fun v0 => + omap (nth_error (var st) i1) (fun v1 => if (evalTest t v0 v1) then pseudoEval l st else pseudoEval r st )) @@ -121,9 +107,11 @@ Module Pseudo (M: PseudoMachine) <: Language. match e' with | O => Some st' | S e'' => - option_map' (pseudoEval p st') (fun st'' => + omap (pseudoEval p st') (fun st'' => funexpseudo e'' st'') end) e st + + | PCall n m p => pseudoEval p st end. Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st'). @@ -134,14 +122,14 @@ End Pseudo. Module PseudoUnary32 <: PseudoMachine. Definition width := 32. Definition vars := 1. - Definition width_spec := I32. + Definition width_spec := W32. Definition const: Type := word width. End PseudoUnary32. Module PseudoUnary64 <: PseudoMachine. Definition width := 64. Definition vars := 1. - Definition width_spec := I64. + Definition width_spec := W64. Definition const: Type := word width. End PseudoUnary64. \ No newline at end of file diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v index c911b00ee..193114d14 100644 --- a/src/Assembly/Qhasm.v +++ b/src/Assembly/Qhasm.v @@ -7,7 +7,6 @@ Module Qhasm <: Language. Import State. (* A constant upper-bound on the number of operations we run *) - Definition maxOps: nat := 1000. Definition State := State. (* Program Types *) -- cgit v1.2.3