| The X86 machine language |
Require Import Arith Bvector ZArith.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Maps.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.Specif.
Require Import Asm.Bitvector.Bitvector.
Set Implicit Arguments.
Register sets |
| General-purpose 8-bit registers |
Inductive reg8 : Set :=
AL
| CL
| DL
| BL
| AH
| CH
| DH
| BH.
| General-purpose 32-bit registers |
Inductive reg32 : Set :=
EAX
| ECX
| EDX
| EBX
| ESP
| EBP
| ESI
| EDI.
Flags |
Inductive flag : Set :=
ID
| VIP
| VIF
| AC
| VM
| RF
| NT
| IOPL
| OF
| DF
| IF_flag
| TF
| SF
| ZF
| AF
| PF
| CF.
Conditions |
| Condition codes |
Inductive condition : Set :=
O
| B
| Z
| BE
| S
| P
| L
| LE.
Definition cc := (bool * condition)%type.
Addresses |
Inductive scale : Set :=
Scale1
| Scale2
| Scale4
| Scale8.
Record address : Set :=
{addrDisp : int32;
addrBase : option reg32;
addrIndex : option (scale * reg32)}.
Operands |
Inductive genop (R : Set) : Set :=
Imm : int32 -> genop R
| Reg : R -> genop R
| Address : address -> genop R.
Definition genop32 := genop reg32.
Definition genop8 := genop reg8.
Operations |
Inductive arith_op : Set :=
Add
| And
| Or
| Sub.
Inductive shift_op : Set :=
Shl
| Shr.
Instructions |
Inductive instr : Set :=
Arith : arith_op -> genop32 -> genop32 -> instr
| Arithb : arith_op -> genop8 -> genop8 -> instr
| Call : genop32 -> instr
| Cmp : genop32 -> genop32 -> instr
| Inc : genop32 -> instr
| Jcc : cc -> int32 -> instr
| Jmp : int32 -> instr
| Lea : reg32 -> address -> instr
| Leave : instr
| Mov : genop32 -> genop32 -> instr
| Movb : genop8 -> genop8 -> instr
| Pop : genop32 -> instr
| Push : genop32 -> instr
| Ret : instr
| Shift : shift_op -> genop32 -> genop8 -> instr.
Maps to be used in concrete states |
Definition reg32_eq_dec : forall (r1 r2 : reg32), {r1 = r2} + {r1 <> r2}.
Module Reg32Indexed <: INDEXED_TYPE.
Definition t := reg32.
Definition index r :=
(match r with
| EAX => 1
| ECX => 2
| EDX => 3
| EBX => 4
| ESP => 5
| EBP => 6
| ESI => 7
| EDI => 8
end)%positive.
Theorem index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := reg32_eq_dec.
Definition invert p :=
(match p with
| 1 => EAX
| 2 => ECX
| 3 => EDX
| 4 => EBX
| 5 => ESP
| 6 => EBP
| 7 => ESI
| _ => EDI
end)%positive.
Theorem invert_index : forall x, invert (index x) = x.
End Reg32Indexed.
Module Reg32Map := IMap(Reg32Indexed).
Definition regs32 := Reg32Map.t int32.
Definition flag_eq_dec : forall (r1 r2 : flag), {r1 = r2} + {r1 <> r2}.
Module FlagIndexed <: INDEXED_TYPE.
Definition t := flag.
Definition index f :=
(match f with
| ID => 1
| VIP => 2
| VIF => 3
| AC => 4
| VM => 5
| RF => 6
| NT => 7
| IOPL => 8
| OF => 9
| DF => 10
| IF_flag => 11
| TF => 12
| SF => 13
| ZF => 14
| AF => 15
| PF => 16
| CF => 17
end)%positive.
Theorem index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := flag_eq_dec.
Definition invert f :=
(match f with
| 1 => ID
| 2 => VIP
| 3 => VIF
| 4 => AC
| 5 => VM
| 6 => RF
| 7 => NT
| 8 => IOPL
| 9 => OF
| 10 => DF
| 11 => IF_flag
| 12 => TF
| 13 => SF
| 14 => ZF
| 15 => AF
| 16 => PF
| _ => CF
end)%positive.
Theorem invert_index : forall x, invert (index x) = x.
End FlagIndexed.
Module FlagMap := IMap(FlagIndexed).
Definition flags := FlagMap.t bool.
Module Int32Indexed <: INDEXED_TYPE.
Definition t := int32.
Definition index (n : t) := P_of_succ_nat (bvec_to_nat n).
Lemma P_of_succ_nat_inj : forall n1 n2,
P_of_succ_nat n1 = P_of_succ_nat n2
-> n1 = n2.
Theorem index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := int32_eq_dec.
Definition invert n := nat_to_bvec 32 (pred (nat_of_P n)).
Theorem invert_index : forall x, invert (index x) = x.
End Int32Indexed.
Module Int32Map := IMap(Int32Indexed).
Definition mem := Int32Map.t int8.
Concrete states |
Record state : Set := {
stRegs32 : regs32;
stFlags : flags;
stMem : mem;
stPc : int32
}.
Accessors and mutators |
Definition get_reg32 (st : state) (r : reg32) :=
Reg32Map.get r (stRegs32 st).
Definition set_reg32 (st : state) (r : reg32) (n : int32) :=
Build_state (Reg32Map.set r n (stRegs32 st)) (stFlags st) (stMem st) (stPc st).
Definition get_flag st f := FlagMap.get f (stFlags st).
Definition set_flag st f b := Build_state (stRegs32 st)
(FlagMap.set f b (stFlags st)) (stMem st) (stPc st).
Definition get_mem (st : state) (a : int32) :=
Int32Map.get a (stMem st).
Definition set_mem (st : state) (a : int32) (n : int8) :=
Build_state (stRegs32 st) (stFlags st) (Int32Map.set a n (stMem st)) (stPc st).
Definition set_pc (st : state) (pc : int32) :=
Build_state (stRegs32 st) (stFlags st) (stMem st) pc.
Address evaluation |
Definition scale_shift sc :=
match sc with
| Scale1 => 0
| Scale2 => 1
| Scale4 => 2
| Scale8 => 3
end.
Definition eval_addr (addr : address) (st : state) : int32 :=
let n := addrDisp addr in
let n := match addrBase addr with
| None => n
| Some base => badd32 n (get_reg32 st base)
end in
match addrIndex addr with
| None => n
| Some (sc, index) =>
badd32 n (bshl32 (get_reg32 st index) (scale_shift sc))
end.
Combined 32-bit memory accessor/mutator |
Definition get_mem32' (m : Int32Map.t int8) (a : int32) : int32 :=
nat_to_bvec 32
(bvec_to_nat (Int32Map.get a m)
+ pow2 8 * bvec_to_nat (Int32Map.get (binc a) m)
+ pow2 16 * bvec_to_nat (Int32Map.get (binc (binc a)) m)
+ pow2 24 * bvec_to_nat (Int32Map.get (binc (binc (binc a))) m)).
Definition get_mem32 (st : state) (a : int32) := get_mem32' (stMem st) a.
Definition set_mem32' (m : Int32Map.t int8) (a v : int32) :=
Int32Map.set (binc3 a) (byte4 v)
(Int32Map.set (binc2 a) (byte3 v)
(Int32Map.set (binc a) (byte2 v)
(Int32Map.set a (byte1 v) m))).
Definition set_mem32 (st : state) (a v : int32) :=
Build_state (stRegs32 st) (stFlags st) (set_mem32' (stMem st) a v) (stPc st).
Evaluating operands |
Definition eval_genop32 (gop : genop32) (st : state) : int32 :=
match gop with
| Imm n => n
| Reg r => get_reg32 st r
| Address a => get_mem32 st (eval_addr a st)
end.
Writing to an operand |
Inductive write_genop32 : genop32 -> int32 -> state -> state -> Prop :=
| WriteReg : forall r n st,
write_genop32 (Reg r) n st (set_reg32 st r n)
| WriteMem : forall a n st,
write_genop32 (Address reg32 a) n st (set_mem32 st (eval_addr a st) n).
Evaluating arithmetic |
Definition eval_arith aop n1 n2 :=
match aop with
| Add => badd32 n1 n2
| And => band32 n1 n2
| Or => bor32 n1 n2
| Sub => bsub32 n1 n2
end.
Definition parity : forall n len (v : Bvector (len + n)), bool.
Definition sign : forall len (v : Bvector (Datatypes.S len)), bool.
Definition eval_CF aop (n1 n2 : int32) :=
match aop with
| Add => sum_to_bool (le_lt_dec (pow2 32) (bvec_to_nat n1 + bvec_to_nat n2))
| And => false
| Or => false
| _ => negb (sum_to_bool (le_lt_dec (bvec_to_nat n2) (bvec_to_nat n1)))
end.
Definition eval_PF aop n1 n2 := negb (parity 8 24 (eval_arith aop n1 n2)).
Parameter eval_AF : arith_op -> int32 -> int32 -> bool.
Definition eval_ZF aop n1 n2 := bvec_eq (eval_arith aop n1 n2) bzero32.
Definition eval_SF aop n1 n2 := sign (eval_arith aop n1 n2).
Definition eval_OF aop (n1 n2 : int32) :=
match aop with
| Add =>
eqb (sign n1) (sign n2)
&& (negb (eqb (sign n1) (sign (badd32 n1 n2)))
|| (bvec_eq (badd32 n1 n2) bzero32
&& negb (bvec_eq n1 bzero32 && bvec_eq n2 bzero32)))
| And => false
| Or => false
| _ =>
negb (eqb (sign n1) (sign n2))
&& (negb (eqb (sign n1) (sign (bsub32 n1 n2)))
|| (bvec_eq (bsub32 n1 n2) bzero32
&& negb (bvec_eq n1 bzero32 && bvec_eq n2 bzero32)))
end.
Definition arith_flags' m aop n1 n2 :=
FlagMap.set OF (eval_OF aop n1 n2)
(FlagMap.set SF (eval_SF aop n1 n2)
(FlagMap.set ZF (eval_ZF aop n1 n2)
(FlagMap.set AF (eval_AF aop n1 n2)
(FlagMap.set PF (eval_PF aop n1 n2)
(FlagMap.set CF (eval_CF aop n1 n2)
m))))).
Definition arith_flags st aop n1 n2 :=
Build_state (stRegs32 st) (arith_flags' (stFlags st) aop n1 n2)
(stMem st) (stPc st).
Definition arith_flags_no_CF' m aop n1 n2 :=
FlagMap.set OF (eval_OF aop n1 n2)
(FlagMap.set SF (eval_SF aop n1 n2)
(FlagMap.set ZF (eval_ZF aop n1 n2)
(FlagMap.set AF (eval_AF aop n1 n2)
(FlagMap.set PF (eval_PF aop n1 n2)
m)))).
Definition arith_flags_no_CF st aop n1 n2 :=
Build_state (stRegs32 st) (arith_flags_no_CF' (stFlags st) aop n1 n2)
(stMem st) (stPc st).
Evaluating conditions |
Definition check_condition' m c :=
match c with
O => FlagMap.get OF m
| B => FlagMap.get CF m
| Z => FlagMap.get ZF m
| BE => FlagMap.get CF m || FlagMap.get ZF m
| S => FlagMap.get SF m
| P => FlagMap.get PF m
| L => negb (eqb (FlagMap.get SF m) (FlagMap.get OF m))
| LE => FlagMap.get ZF m || negb (eqb (FlagMap.get SF m) (FlagMap.get OF m))
end.
Definition check_cc' m cb := eqb (check_condition' m (snd cb)) (fst cb).
Definition check_cc st cb := check_cc' (stFlags st) cb.
Executing instructions |
Definition one := nat_to_bvec 32 1.
Definition four := nat_to_bvec 32 4.
Definition neg_four := bneg four.
Inductive exec : (instr * int32) -> state -> state -> Prop :=
| XArith : forall nextPc st aop dst src st',
write_genop32 dst (eval_arith aop (eval_genop32 dst st) (eval_genop32 src st)) st st'
-> exec (Arith aop dst src, nextPc) st
(set_pc (arith_flags st' aop (eval_genop32 dst st) (eval_genop32 src st)) nextPc)
| XCall : forall nextPc st dst st' st'',
write_genop32 (Address reg32 (Build_address neg_four (Some ESP) None)) nextPc st st'
-> write_genop32 (Reg ESP) (eval_arith Sub (eval_genop32 (Reg ESP) st) four) st' st''
-> exec (Call dst, nextPc) st (set_pc st'' (eval_genop32 dst st''))
| XCmp : forall nextPc st dst src,
exec (Cmp dst src, nextPc) st
(set_pc (arith_flags st Sub (eval_genop32 dst st) (eval_genop32 src st)) nextPc)
| XInc : forall nextPc st src st',
write_genop32 src (eval_arith Add (eval_genop32 src st) one) st st'
-> exec (Inc src, nextPc) st
(set_pc (arith_flags_no_CF st' Add (eval_genop32 src st) one) nextPc)
| XJcc_true : forall nextPc st co pc,
check_cc st co = true
-> exec (Jcc co pc, nextPc) st (set_pc st pc)
| XJcc_false : forall nextPc st co pc,
check_cc st co = false
-> exec (Jcc co pc, nextPc) st (set_pc st nextPc)
| XJmp : forall nextPc st pc,
exec (Jmp pc, nextPc) st (set_pc st pc)
| XLea : forall nextPc st r a,
exec (Lea r a, nextPc) st (set_pc (set_reg32 st r (eval_addr a st)) nextPc)
| XLeave : forall nextPc st st' st'',
write_genop32 (Reg EBP) (eval_genop32 (Address reg32 (Build_address bzero32 (Some EBP) None)) st) st st'
-> write_genop32 (Reg ESP) (eval_arith Add four (eval_genop32 (Reg EBP) st)) st' st''
-> exec (Leave, nextPc) st (set_pc st'' nextPc)
| XMov : forall nextPc st dst src st',
write_genop32 dst (eval_genop32 src st) st st'
-> exec (Mov dst src, nextPc) st (set_pc st' nextPc)
| XPop : forall nextPc st dst st' st'',
write_genop32 dst (eval_genop32 (Address reg32 (Build_address bzero32 (Some ESP) None)) st) st st'
-> write_genop32 (Reg ESP) (eval_arith Add four (eval_genop32 (Reg ESP) st')) st' st''
-> exec (Pop dst, nextPc) st (set_pc st'' nextPc)
| XPush : forall nextPc st src st' st'',
write_genop32 (Address reg32 (Build_address neg_four (Some ESP) None)) (eval_genop32 src st) st st'
-> write_genop32 (Reg ESP) (eval_arith Add neg_four (eval_genop32 (Reg ESP) st)) st' st''
-> exec (Push src, nextPc) st (set_pc st'' nextPc)
| XRet : forall nextPc st st',
write_genop32 (Reg ESP) (eval_arith Add four (eval_genop32 (Reg ESP) st)) st st'
-> exec (Ret, nextPc) st (set_pc st'
(eval_genop32 (Address reg32 (Build_address bzero32 (Some ESP) None)) st)).
Decoding instructions |
Definition longestInstr := 15.
| The longest encoding of any x86 instruction |
Parameter decode_instr : mem -> int32 -> instr * int32.
| For a given memory and PC, figure out which instruction we execute and to which next PC we fall-through if no special control flow occurs. This function is implemented in OCaml. |
Definition get_instr st := decode_instr (stMem st) (stPc st).
Reasoning about parts of memory that remain unchanged |
Definition agree_range (mem1 mem2 : mem) (addr1 : int32) (len : nat) :=
forall addr', bvec_to_nat addr1 <= bvec_to_nat addr' < bvec_to_nat addr1 + len
-> Int32Map.get addr' mem1 = Int32Map.get addr' mem2.
Axiom decode_same : forall mem1 mem2 addr,
agree_range mem1 mem2 addr longestInstr
-> decode_instr mem1 addr = decode_instr mem2 addr.