diff options
Diffstat (limited to 'src/Assembly/Medial.v')
| -rw-r--r-- | src/Assembly/Medial.v | 175 |
1 files changed, 0 insertions, 175 deletions
diff --git a/src/Assembly/Medial.v b/src/Assembly/Medial.v deleted file mode 100644 index 5f082aa12..000000000 --- a/src/Assembly/Medial.v +++ /dev/null @@ -1,175 +0,0 @@ -Require Import QhasmEvalCommon Pseudo. -Require Import Language. -Require Import List. - -Module Medial (Arch: PseudoMachine) <: Language. - Import MedState EvalUtil Arch. - - Definition W := word width. - - (* Program Types *) - Definition State := MedState width. - Transparent State. - - Inductive MAssignment : Type := - | MAVar: nat -> nat -> MAssignment - | MAMem: forall m, nat -> nat -> Index m -> 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. - - Inductive MConditional := - | MZ: nat -> MConditional - | MCReg: TestOp -> nat -> nat -> MConditional - | MCConst: TestOp -> nat -> W -> MConditional. - - Inductive Medial: Set := - | MSkip: Medial - | MSeq: Medial -> Medial -> Medial - | MAssign: MAssignment -> Medial - | MOp: MOperation -> Medial - | MCond: MConditional -> Medial -> 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 (getVar y st) with - | Some v => Some (setVar x v st) - | _ => None - end - - | MAMem _ x y i => - match (getMem y i st) with - | Some v => Some (setVar x v st) - | _ => None - end - - | MAConst x c => Some (setVar x c st) - end - - | MOp o => - match o with - | MIOpConst io a c => - omap (getVar a st) (fun v => - let (res, c') := evalIntOp io v c in - Some (setVar a res (setCarryOpt c' st))) - - | MIOpReg io a b => - omap (getVar a st) (fun va => - omap (getVar b st) (fun vb => - let (res, c') := evalIntOp io va vb in - Some (setVar a res (setCarryOpt c' st)))) - - | MCOpReg o a b => - omap (getVar a st) (fun va => - omap (getVar b st) (fun vb => - let c := match (snd st) with | Some b => b | _ => false end in - let (res, c') := evalCarryOp o va vb c in - Some (setVar a res (setCarry c' st)))) - - | MDOpReg duo a b (Some x) => - omap (getVar a st) (fun va => - omap (getVar b st) (fun vb => - let (low, high) := evalDualOp duo va vb in - Some (setVar a low (setVar x high st)))) - - | MDOpReg duo a b None => - omap (getVar a st) (fun va => - omap (getVar b st) (fun vb => - let (low, high) := evalDualOp duo va vb in - Some (setVar a low st))) - - | MOpRot ro a x => - omap (getVar a st) (fun v => - let res := evalRotOp ro v (proj1_sig x) in - Some (setVar a res st)) - end - - | MCond c a b => - match c with - | MCConst t x y => - omap (getVar x st) (fun vx => - if (evalTest t vx y) - then meval a st - else meval b st) - - | MCReg t x y => - omap (getVar x st) (fun vx => - - (* TODO: why can't we infer width here? *) - omap (@getVar width y st) (fun vy => - if (evalTest t vx vy) - then meval a st - else meval b st)) - - | MZ x => - omap (getVar x st) (fun vx => - if (evalTest TEq vx (wzero width)) - 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 - | O => Some s - | S m' => - match f s with - | None => None - | Some s' => fexp m' f s' - end - end - ) n (meval a) st - - | _ => None - end. - - Definition evaluatesTo := fun m st0 st1 => meval (inlineAll m) st0 = Some st1. - - (* world peace *) -End Medial. |