(*  Title:       X86 instruction semantics and basic block symbolic execution
    Authors:     Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran
    Year:        2020
    Maintainer:  Freek Verbeek (freek@vt.edu)
*)

section "

theory Exmple
  imports SymbolicExecution
java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0

context unknowns
begin
  
  text ‹
  A simple hand-crafted example showing some basic instructions.
\<close>


schematic_goal example1:
  assumes[simp]: "  0x0 = PUSH (Reg ''rbp'') 1"
 and[simp]: "fetch 0x1 = SUB (Reg ''rsp'') (Imm 30) 2"
 and[simp]: "fetch 0x2 = MOV (QWORD PTR [22 + ''rsp'']₂) (Imm 42) 3"
 and[simp]: "fetch 0x3 = MOV (QWORD PTR [30 + ''rsp'']₂) (Imm 43) 4"
 and[simp]: "fetch 0x4 = ADD (Reg ''rsp'') (Imm 30) 5"
 and[simp]: "fetch 0x5 = POP (Reg ''rbp'') 6"
 and[simp]: "fetch 0x6 = RET 1"
 shows "run 0x6 fetch (σ with [setRip 0x0]) ?σ'"
 apply se_step+
 apply (subst eq_def,simp)
 done

  example1




  ‹Demonstrates little-endian memory and register-aliasing›

 ‹
 begin{verbatim}
 RAX + 0 1 2 3 4 5 6 7
 | FF | EE | DD | CC | BB | AA | 00 | 00 |
 
 EDI := 0xCCDDEEFF
 EBX := 0xAABB
 RCX := 0xAABBCCDDAABB
 end{verbatim}
 ›

  example2:
 assumes[simp]: "fetch 0x0 = MOV (QWORD PTR [''rax'']₁) (Imm 0xAABBCCDDEEFF) 1"
 and[simp]: "fetch 0x1 = MOV (Reg ''edi'') (DWORD PTR [''rax'']₁) 2"
 and[simp]: "fetch 0x2 = MOV (Reg ''ebx'') (DWORD PTR [4 + ''rax'']₂) 3"
 and[simp]: "fetch 0x3 = MOV (Reg ''rcx'') (QWORD PTR [''rax'']₁) 4"
 and[simp]: "fetch 0x4 = MOV (Reg ''cx'') (WORD PTR [4 + ''rax'']₂) 5"
 shows "run 0x4 fetch (σ with [setRip 0x0]) ?σ'"
 apply se_step+
 apply (subst eq_def,simp)
 done

  example2

  ‹
 This example show how assumptions over regions are generated.
 Since no relation over rax and rbx is known in the initial state, they will be assumed to be
 separate by default.
 ›
  example3:
 assumes[simp]: "fetch 0x0 = MOV (QWORD PTR [''rax'']₁) (Imm 0xAABBCCDDEEFF) 1"
 and[simp]: "fetch 0x1 = MOV (QWORD PTR [''rbx'']₁) (Imm 0x112233445566) 2"
 and[simp]: "fetch 0x2 = MOV (Reg ''rcx'') (DWORD PTR [2 + ''rax'']₂) 3"
 and[simp]: "fetch 0x3 = MOV (Reg ''cx'') (WORD PTR [4 + ''rbx'']₂) 4"
 and[simp]: "fetch 0x4 = MOV (Reg ''cl'') (BYTE PTR [''rax'']₁) 5"
 shows "assumptions ?A ==> run 0x4 fetch (σ with [setRip 0x0]) ?σ'"
 apply se_step+
 apply (subst eq_def,simp)
 done

  example3