Changeset 2316 for src/ASM/ASM.ma


Ignore:
Timestamp:
Sep 3, 2012, 9:03:24 AM (8 years ago)
Author:
boender
Message:
  • committed temporary version: true version has to wait until I recuperate my hard disk
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2143 r2316  
    10061006  | _ ⇒ False
    10071007  ].
     1008
     1009
     1010(* If instruction i is a jump, then there will be something in the policy at
     1011 * position i *)
     1012definition is_jump' ≝
     1013  λx:preinstruction Identifier.
     1014  match x with
     1015  [ JC _ ⇒ true
     1016  | JNC _ ⇒ true
     1017  | JZ _ ⇒ true
     1018  | JNZ _ ⇒ true
     1019  | JB _ _ ⇒ true
     1020  | JNB _ _ ⇒ true
     1021  | JBC _ _ ⇒ true
     1022  | CJNE _ _ ⇒ true
     1023  | DJNZ _ _ ⇒ true
     1024  | _ ⇒ false
     1025  ].
     1026
     1027definition is_relative_jump ≝
     1028  λinstr:pseudo_instruction.
     1029  match instr with
     1030  [ Instruction i ⇒ is_jump' i
     1031  | _             ⇒ false
     1032  ].
     1033   
     1034definition is_jump ≝
     1035  λinstr:pseudo_instruction.
     1036  match instr with
     1037  [ Instruction i   ⇒ is_jump' i
     1038  | Call _ ⇒ true
     1039  | Jmp _ ⇒ true
     1040  | _ ⇒ false
     1041  ].
     1042
     1043definition is_call ≝
     1044  λinstr:pseudo_instruction.
     1045  match instr with
     1046  [ Call _ ⇒ true
     1047  | _ ⇒ false
     1048  ].
     1049 
     1050definition is_jump_to ≝
     1051  λx:pseudo_instruction.λd:Identifier.
     1052  match x with
     1053  [ Instruction i ⇒ match i with
     1054    [ JC j ⇒ d = j
     1055    | JNC j ⇒ d = j
     1056    | JZ j ⇒ d = j
     1057    | JNZ j ⇒ d = j
     1058    | JB _ j ⇒ d = j
     1059    | JNB _ j ⇒ d = j
     1060    | JBC _ j ⇒ d = j
     1061    | CJNE _ j ⇒ d = j
     1062    | DJNZ _ j ⇒ d = j
     1063    | _ ⇒ False
     1064    ]
     1065  | Call c ⇒ d = c
     1066  | Jmp j ⇒ d = j
     1067  | _ ⇒ False
     1068  ].
Note: See TracChangeset for help on using the changeset viewer.