Theory SymbolicExecution

(*  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 "A symbolic execution engine"


theory SymbolicExecution
  imports X86_InstructionSemantics StateCleanUp
begin



definition eq (infixl "≜" 50)
  where "(≜) ≡ (=)"

context unknowns
begin 


inductive run :: "64 word ⇒ (64 word ⇒ I) ⇒ state ⇒ state ⇒ bool"
  where 
    "rip σ = a⇩f ⟹ fetch (rip σ) = i ⟹ σ' ≜ step i σ ⟹ run a⇩f fetch σ σ'"
  | "rip σ ≠ a⇩f ⟹ fetch (rip σ) = i ⟹ run a⇩f fetch (step i σ) σ' ⟹ run a⇩f fetch σ σ'"


method fetch_and_execute = (
   ((rule run.intros(2),(simp (no_asm) add: state_simps;fail))
    | (rule run.intros(1),(simp (no_asm) add: state_simps;fail))),
   (simp (no_asm) add: state_simps),                                             ― ‹fetch instruction›
   (simp (no_asm_simp) add: step_def semantics_simps state_simps BitByte_simps), ― ‹simplification›
   (subst clean_state_updates[symmetric],simp (no_asm))                          ― ‹cleaning up›
 )

method resolve_mem_reads = (
  subst mem_read_mem_write_separate,
  ((simp (no_asm_simp) add: separate_simps state_simps; fail) 
   | (rule assumptions_impI,simp (no_asm_simp),subst (asm) assumptions_conjE, erule conjE)),
  (simp (no_asm_simp) add: semantics_simps state_simps BitByte_simps separate_simps)?
 )

method se_step = 
  fetch_and_execute,
  ((resolve_mem_reads)+;(subst clean_state_updates[symmetric],simp (no_asm)))?,
  clean_up

method se_step_no_clean = 
  fetch_and_execute,
  ((resolve_mem_reads)+;(subst clean_state_updates[symmetric],simp (no_asm)))?

end


abbreviation RSP0 
  where "RSP0 σ ≡ regs σ ''rsp''"
abbreviation RBP0 
  where "RBP0 σ ≡ regs σ ''rbp''"
abbreviation RAX0 
  where "RAX0 σ ≡ regs σ ''rax''"
abbreviation RBX0 
  where "RBX0 σ ≡ regs σ ''rbx''"
abbreviation RCX0 
  where "RCX0 σ ≡ regs σ ''rcx''"
abbreviation RDX0 
  where "RDX0 σ ≡ regs σ ''rdx''"
abbreviation RDI0 
  where "RDI0 σ ≡ regs σ ''rdi''"
abbreviation RSI0 
  where "RSI0 σ ≡ regs σ ''rsi''"
abbreviation R150 
  where "R150 σ ≡ regs σ ''r15''"
abbreviation R140
  where "R140 σ ≡ regs σ ''r14''"
abbreviation R130 
  where "R130 σ ≡ regs σ ''r13''"
abbreviation R120 
  where "R120 σ ≡ regs σ ''r12''"
abbreviation R110 
  where "R110 σ ≡ regs σ ''r11''"
abbreviation R100 
  where "R100 σ ≡ regs σ ''r10''"
abbreviation R90 
  where "R90 σ ≡ regs σ ''r9''"
abbreviation R80 
  where "R80 σ ≡ regs σ ''r8''"



text ‹Repeat a command up to n times, in deterministic fashion (a la the REPEAT\_DETERM tactic).›

method_setup repeat_n = ‹
  Scan.lift Parse.nat -- Method.text_closure >>
    (fn (n,text) => fn ctxt => fn using => 
      let
        val ctxt_tac = Method.evaluate_runtime text ctxt using;
        fun repeat_n 0 ctxt_st = Seq.make_results (Seq.succeed ctxt_st)
          | repeat_n i ctxt_st = case Seq.pull (ctxt_tac ctxt_st) of
                            SOME (Seq.Result ctxt_st', _) => repeat_n (i-1) ctxt_st'
                          | _ => Seq.make_results (Seq.succeed ctxt_st)
      in
        repeat_n n
      end)
›

end