Skip to content

Instantly share code, notes, and snippets.

@pnwamk

pnwamk/actual.add_block_0_201320_0.smt2

Created June 24, 2020 23:20
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save pnwamk/97d52ace5664a4ad217922b303b402b5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save pnwamk/97d52ace5664a4ad217922b303b402b5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
actual.add_block_0_201320_0.smt2
; Machine code write at 0x201320 is in unreserved stack space.
(set-logic ALL)
(set-option :produce-modules true)
(define-fun |mem_read8-0| ((|arg-1| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-2| (_ BitVec 64))) (_ BitVec 8) (select |arg-1| (bvadd |arg-2| #x0000000000000000)))
(define-fun |mem_write8-3| ((|arg-4| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-5| (_ BitVec 64)) (|arg-6| (_ BitVec 8))) (Array (_ BitVec 64) (_ BitVec 8)) (store |arg-4| |arg-5| ((_ extract 7 0) |arg-6|)))
(define-fun |mem_read16-7| ((|arg-8| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-9| (_ BitVec 64))) (_ BitVec 16) (concat (select |arg-8| (bvadd |arg-9| #x0000000000000000)) (select |arg-8| (bvadd |arg-9| #x0000000000000001))))
(define-fun |mem_write16-10| ((|arg-11| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-12| (_ BitVec 64)) (|arg-13| (_ BitVec 16))) (Array (_ BitVec 64) (_ BitVec 8)) (store |arg-11| (bvadd |arg-12| #x0000000000000001) ((_ extract 15 8) |arg-13|)))
(define-fun |mem_read32-14| ((|arg-15| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-16| (_ BitVec 64))) (_ BitVec 32) (concat (concat (concat (select |arg-15| (bvadd |arg-16| #x0000000000000000)) (select |arg-15| (bvadd |arg-16| #x0000000000000001))) (select |arg-15| (bvadd |arg-16| #x0000000000000002))) (select |arg-15| (bvadd |arg-16| #x0000000000000003))))
(define-fun |mem_write32-17| ((|arg-18| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-19| (_ BitVec 64)) (|arg-20| (_ BitVec 32))) (Array (_ BitVec 64) (_ BitVec 8)) (store |arg-18| (bvadd (bvadd (bvadd |arg-19| #x0000000000000001) #x0000000000000001) #x0000000000000001) ((_ extract 31 24) |arg-20|)))
(define-fun |mem_read64-21| ((|arg-22| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-23| (_ BitVec 64))) (_ BitVec 64) (concat (concat (concat (concat (concat (concat (concat (select |arg-22| (bvadd |arg-23| #x0000000000000000)) (select |arg-22| (bvadd |arg-23| #x0000000000000001))) (select |arg-22| (bvadd |arg-23| #x0000000000000002))) (select |arg-22| (bvadd |arg-23| #x0000000000000003))) (select |arg-22| (bvadd |arg-23| #x0000000000000004))) (select |arg-22| (bvadd |arg-23| #x0000000000000005))) (select |arg-22| (bvadd |arg-23| #x0000000000000006))) (select |arg-22| (bvadd |arg-23| #x0000000000000007))))
(define-fun |mem_write64-24| ((|arg-25| (Array (_ BitVec 64) (_ BitVec 8))) (|arg-26| (_ BitVec 64)) (|arg-27| (_ BitVec 64))) (Array (_ BitVec 64) (_ BitVec 8)) (store |arg-25| (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd |arg-26| #x0000000000000001) #x0000000000000001) #x0000000000000001) #x0000000000000001) #x0000000000000001) #x0000000000000001) #x0000000000000001) ((_ extract 63 56) |arg-27|)))
(declare-fun |rax-28| () (_ BitVec 64))
(declare-fun |rcx-29| () (_ BitVec 64))
(declare-fun |rdx-30| () (_ BitVec 64))
(declare-fun |rbx-31| () (_ BitVec 64))
(declare-fun |rsp-32| () (_ BitVec 64))
(declare-fun |rbp-33| () (_ BitVec 64))
(declare-fun |rsi-34| () (_ BitVec 64))
(declare-fun |rdi-35| () (_ BitVec 64))
(declare-fun |r8-36| () (_ BitVec 64))
(declare-fun |r9-37| () (_ BitVec 64))
(declare-fun |r10-38| () (_ BitVec 64))
(declare-fun |r11-39| () (_ BitVec 64))
(declare-fun |r12-40| () (_ BitVec 64))
(declare-fun |r13-41| () (_ BitVec 64))
(declare-fun |r14-42| () (_ BitVec 64))
(declare-fun |r15-43| () (_ BitVec 64))
(declare-fun |cf-44| () Bool)
(declare-fun |RESERVED_1-45| () Bool)
(declare-fun |pf-46| () Bool)
(declare-fun |RESERVED_3-47| () Bool)
(declare-fun |af-48| () Bool)
(declare-fun |RESERVED_5-49| () Bool)
(declare-fun |zf-50| () Bool)
(declare-fun |sf-51| () Bool)
(declare-fun |tf-52| () Bool)
(declare-fun |if-53| () Bool)
(declare-fun |df-54| () Bool)
(declare-fun |of-55| () Bool)
(declare-fun |iopl1-56| () Bool)
(declare-fun |iopl2-57| () Bool)
(declare-fun |nt-58| () Bool)
(declare-fun |RESERVED_15-59| () Bool)
(declare-fun |rf-60| () Bool)
(declare-fun |vm-61| () Bool)
(declare-fun |ac-62| () Bool)
(declare-fun |vif-63| () Bool)
(declare-fun |vip-64| () Bool)
(declare-fun |id-65| () Bool)
(declare-fun |el-66| () Bool)
(declare-fun |el-67| () Bool)
(declare-fun |el-68| () Bool)
(declare-fun |el-69| () Bool)
(declare-fun |el-70| () Bool)
(declare-fun |el-71| () Bool)
(declare-fun |el-72| () Bool)
(declare-fun |el-73| () Bool)
(declare-fun |el-74| () Bool)
(declare-fun |el-75| () Bool)
(declare-fun |init_mem-76| () (Array (_ BitVec 64) (_ BitVec 8)))
(declare-fun |stack_alloc_min-77| () (_ BitVec 64))
(assert (= (bvand |stack_alloc_min-77| #x0000000000000fff) #x0000000000000000))
(assert (bvult #x0000000000001000 |stack_alloc_min-77|))
(define-fun |stack_guard_min-78| () (_ BitVec 64) (bvsub |stack_alloc_min-77| #x0000000000001000))
(assert (bvult |stack_guard_min-78| |stack_alloc_min-77|))
(declare-fun |stack_max-79| () (_ BitVec 64))
(assert (= (bvand |stack_max-79| #x0000000000000fff) #x0000000000000000))
(assert (bvult |stack_alloc_min-77| |stack_max-79|))
(assert (bvule |stack_alloc_min-77| |rsp-32|))
(assert (bvule |rsp-32| (bvsub |stack_max-79| #x0000000000000008)))
(define-fun |on_stack-81| ((|arg-82| (_ BitVec 64)) (|arg-83| (_ BitVec 64))) Bool (let ((|e-80| (bvadd |arg-82| |arg-83|))) (and (bvule |stack_guard_min-78| |arg-82|) (and (bvule |arg-82| |e-80|) (bvule |e-80| |stack_max-79|)))))
(define-fun |not_in_stack_range-85| ((|arg-86| (_ BitVec 64)) (|arg-87| (_ BitVec 64))) Bool (let ((|e-84| (bvadd |arg-86| |arg-87|))) (and (bvule |arg-86| |e-84|) (or (bvule |e-84| |stack_alloc_min-77|) (bvule |stack_max-79| |arg-86|)))))
(assert (bvult |rsp-32| (bvsub |stack_max-79| #x0000000000000008)))
(assert (= (bvand (bvadd |rsp-32| #x0000000000000008) #x000000000000000f) #x0000000000000000))
(define-fun |%arg0-88| () (_ BitVec 64) |rdi-35|)
(assert (= |rbx-31| |rbx-31|))
(assert (= |rsp-32| |rsp-32|))
(assert (= |rbp-33| |rbp-33|))
(assert (= |r12-40| |r12-40|))
(assert (= |r13-41| |r13-41|))
(assert (= |r14-42| |r14-42|))
(assert (= |r15-43| |r15-43|))
; LLVM: %t0 = add i64 %arg0, 1
(define-fun |%t0-89| () (_ BitVec 64) (bvadd |%arg0-88| #x0000000000000001))
; LLVM: ret i64 %t0
(define-fun |rsp-90| () (_ BitVec 64) (bvsub |rsp-32| #x0000000000000008))
(define-fun |addr-91| () (_ BitVec 64) |rsp-90|)
(check-sat-assuming ((not (|on_stack-81| |addr-91| #x0000000000000008))))
(exit)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment