*** i64.maude *** Specification of a subset of the Intel 64 instruction set: *** {MOV, ADD, SUB, TEST, XOR, AND, OR, PUSH, POP, NOP}. *** By Matt Webster, 2006-8. *** Used with Maude 2.3 built: Feb 14 2007 17:53:50 *** This module defines the syntax of a subset of I-64. mod I-64-SYNTAX is protecting INT . sorts Variable Expression Stack EInt . sorts Instruction InstructionSequence . subsort Instruction < InstructionSequence . subsorts Variable EInt < Expression . subsort Int < EInt . op dadd_,_ : Variable Expression -> Instruction [prec 20] . op dsub_,_ : Variable Expression -> Instruction [prec 20] . *** I-64 instructions op mov_,_ : Variable Expression -> Instruction [prec 20] . op add_,_ : Variable Expression -> Instruction [prec 20] . op sub_,_ : Variable Expression -> Instruction [prec 20] . op nop : -> Instruction . op push_ : Expression -> Instruction [prec 20] . op pop_ : Variable -> Instruction [prec 20] . op and_,_ : Variable Expression -> Instruction [prec 20] . op or_,_ : Variable Expression -> Instruction [prec 20] . op xor_,_ : Variable Expression -> Instruction [prec 20] . op test_,_ : Variable Expression -> Instruction [prec 20] . *** helper operations op stackPush : Expression Stack -> Stack . op stackPop : Stack -> Stack . op stackTop : Stack -> EInt . op _next_ : EInt Stack -> Stack [prec 15] . op stackBase : -> Stack . op msb : EInt -> EInt . op isZero : Expression -> EInt . op isZero : EInt -> EInt . op parity : EInt -> EInt . *** error messages op emptyStackError1 : -> Stack . op emptyStackError2 : -> EInt . *** I-64 registers ops eax ebx ecx edx ebp esp esi edi ip : -> Variable . *** I-64 EFLAGS register ops cf of sf af zf pf : -> Variable . *** equality operation op _is_ : EInt EInt -> Bool . op _is_ : Stack Stack -> Bool . *** extending the Int sort to include "undef" op undef : -> EInt . *** overloaded Boolean operations - these should be in proof scripts *** but OBJ3 v.2.0 won't allow it op _band_ : EInt EInt -> EInt [prec 35] . op _bor_ : EInt EInt -> EInt [prec 35] . endm *** This module defines the semantics of the I-64 instructions *** whose syntax is defined in I-64-SYNTAX. mod I-64-SEMANTICS is protecting I-64-SYNTAX . sort Store . *** stores ops s : -> Store . op initial : -> Store . *** operators for defining the semantics of I-64 op _[[_]] : Store Expression -> EInt [prec 30] . op _[[stack]] : Store -> Stack [prec 30] . op _;_ : Store Instruction -> Store [prec 25] . op _;_ : InstructionSequence InstructionSequence -> InstructionSequence [gather (E e) prec 26] . *** variables for rewriting rules vars S S1 S2 S3 : Store . vars I I1 I2 I3 : EInt . vars INT INT1 INT2 : Int . vars V V1 V2 V3 : Variable . vars E E1 E2 E3 : Expression . vars ST ST1 ST2 : Stack . vars P1 P2 : InstructionSequence . *** evaluation of instruction sequences eq S ; (P1 ; P2 ) = (S ; P1) ; P2 . *** _is_ semantics eq I1 is I2 = (I1 == I2) . eq ST1 is ST2 = (ST1 == ST2) . *** the value of any integer in a store is the integer itself eq S[[I]] = I . *** initial values of variables and the stack eq initial[[stack]] = stackBase . ceq initial[[V]] = undef if V =/= ip . eq initial[[ip]] = 0 . *** Axioms to deal with static analysis of primitive *** operators such as +, -, |, &, xor . eq I | I = I . eq I & I = I . eq (I1 + I2) is (I3 + I2) = I1 is I3 . eq (I1 + I2) is (I1 + I2) = true . eq (I1 - I2) is (I1 - I2) = true . eq (I1 | I2) is (I1 | I2) = true . eq (I & S1[[V1]]) is (I & S2[[V2]]) = S1[[V1]] is S2[[V2]] . eq isZero(I1 & I2) is isZero(I1 & I2) = true . eq parity(I1 & I2) is parity(I1 & I2) = true . eq msb(I1 & I2) is msb(I1 & I2) = true . eq isZero(I1 | I2) is isZero(I1 | I2) = true . eq parity(I1 | I2) is parity(I1 | I2) = true . eq msb(I1 xor I2) is msb(I1 xor I2) = true . eq isZero(I1 xor I2) is isZero(I1 xor I2) = true . eq parity(I1 xor I2) is parity(I1 xor I2) = true . eq msb(I1 | I2) is msb(I1 | I2) = true . eq (I1 xor I2) is (I1 xor I2) = true . *** I-64 instruction semantics eq S ; and V,E [[V]] = S[[V]] & S[[E]] . ceq S ; and V1,E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip and V2 =/= sf and V2 =/= zf and V2 =/= pf and V2 =/= cf and V2 =/= of . eq S ; and V,E [[stack]] = S[[stack]] . eq S ; and V,E [[ip]] = S[[ip]] + 1 . eq S ; and V,E [[sf]] = msb( S[[V]] & S[[E]] ) . eq S ; and V,E [[zf]] = isZero( S[[V]] & S[[E]] ) . eq S ; and V,E [[pf]] = parity( S[[V]] & S[[E]] ) . eq S ; and V,E [[cf]] = 0 . eq S ; and V,E [[of]] = 0 . eq S ; or V,E [[V]] = S[[V]] | S[[E]] . ceq S ; or V1,E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip and V2 =/= sf and V2 =/= zf and V2 =/= pf and V2 =/= cf and V2 =/= of . eq S ; or V,E [[stack]] = S[[stack]] . eq S ; or V,E [[ip]] = S[[ip]] + 1 . eq S ; or V,E [[sf]] = msb( S[[V]] | S[[E]] ) . eq S ; or V,E [[zf]] = isZero( S[[V]] | S[[E]] ) . eq S ; or V,E [[pf]] = parity( S[[V]] | S[[E]] ) . eq S ; or V,E [[cf]] = 0 . eq S ; or V,E [[of]] = 0 . eq S ; xor V,E [[V]] = S[[V]] xor S[[E]] . ceq S ; xor V1,E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip and V2 =/= sf and V2 =/= zf and V2 =/= pf and V2 =/= cf and V2 =/= of . eq S ; xor V,E [[stack]] = S[[stack]] . eq S ; xor V,E [[ip]] = S[[ip]] + 1 . eq S ; xor V,E [[sf]] = msb( S[[V]] xor S[[E]] ) . eq S ; xor V,E [[zf]] = isZero( S[[V]] xor S[[E]] ) . eq S ; xor V,E [[pf]] = parity( S[[V]] xor S[[E]] ) . eq S ; xor V,E [[cf]] = 0 . eq S ; xor V,E [[of]] = 0 . eq S ; test V,E [[V]] = S[[V]] . ceq S ; test V1,E [[V2]] = S[[V2]] if V2 =/= ip and V2 =/= sf and V2 =/= zf and V2 =/= pf and V2 =/= cf and V2 =/= of . eq S ; test V,E [[stack]] = S[[stack]] . eq S ; test V,E [[ip]] = S[[ip]] + 1 . eq S ; test V,E [[sf]] = msb( S[[V]] & S[[E]] ) . eq S ; test V,E [[zf]] = isZero( S[[V]] & S[[E]] ) . eq S ; test V,E [[pf]] = parity( S[[V]] & S[[E]] ) . eq S ; test V,E [[cf]] = 0 . eq S ; test V,E [[of]] = 0 . eq S ; mov V,E [[V]] = S[[E]] . ceq S ; mov V1,E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; mov V,E [[stack]] = S[[stack]] . eq S ; mov V,E [[ip]] = S[[ip]] + 1 . eq S ; add V,E [[V]] = (S[[V]] + S[[E]]) . ceq S ; add V1, E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; add V,E [[stack]] = S[[stack]] . eq S ; add V,E [[ip]] = S[[ip]] + 1 . *** special version of add ("dynamic add") that keeps *** results of additions within I-64 limits (2^32-1). eq S ; dadd V,E [[V]] = (S[[V]] + S[[E]]) & 4294967295 . ceq S ; dadd V1, E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; dadd V,E [[stack]] = S[[stack]] . eq S ; dadd V,E [[ip]] = S[[ip]] + 1 . eq S ; sub V,E [[V]] = (S[[V]] - S[[E]]) . ceq S ; sub V1, E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; sub V,E [[stack]] = S[[stack]] . eq S ; sub V,E [[ip]] = S[[ip]] + 1 . *** special version of add ("dynamic sub") that keeps *** results of additions within I-64 limits (2^32-1). eq S ; dsub V,E [[V]] = (S[[V]] - S[[E]]) & 4294967295 . ceq S ; dsub V1, E [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; dsub V,E [[stack]] = S[[stack]] . eq S ; dsub V,E [[ip]] = S[[ip]] + 1 . eq S ; push E [[stack]] = stackPush(S[[E]],S[[stack]]) . ceq S ; push E [[V]] = S[[V]] if V =/= ip . eq S ; push E [[ip]] = S[[ip]] + 1 . eq S ; pop V [[stack]] = stackPop(S[[stack]]) . eq S ; pop V [[V]] = stackTop(S[[stack]]) . ceq S ; pop V1 [[V2]] = S[[V2]] if V1 =/= V2 and V2 =/= ip . eq S ; pop V [[ip]] = S[[ip]] + 1 . ceq S ; nop [[V]] = S[[V]] if V =/= ip . eq S ; nop [[stack]] = S[[stack]] . eq S ; nop [[ip]] = S[[ip]] + 1 . *** Stack helper operations semantics eq stackPush(I,ST) = I next ST . eq stackPop(I next ST) = ST . eq stackPop(stackBase) = emptyStackError1 . eq stackTop(I next ST) = I . eq stackTop(stackBase) = emptyStackError2 . endm mod METAMORPHIC is pr I-64-SEMANTICS . op "sidt" : -> EInt . *** "sidt" is a special integer op s : -> Store . var S : Store . rl [1] : S => S ; mov ebx, "sidt" . rl [2] : S => S ; mov eax, ebx . rl [3] : S => S ; mov ecx, ebx . rl [4] : S => S ; mov eax, ecx . endm search [1000] in METAMORPHIC : S =>+ S such that S[[eax]] is "sidt" .