Andrew Kent pnwamk
pnwamk
/ eqrange_ex_2.smt2
Created
June 29, 2020 17:15
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; main.block_0_201070.1 (0x201084). jump precondition: (= (mcstack (bvsub stack_high (_ bv8 64)) (_ BitVec 64)) (fnstart rbp)) | |
| (set-logic ALL_SUPPORTED) | |
| (set-option :produce-models true) | |
| (define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0)) | |
| (define-fun mem_readbv8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 8) (select m a)) | |
| (define-fun mem_readbv16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 16) (concat (select m (bvadd a (_ bv1 64))) (select m a))) | |
| (define-fun mem_readbv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 32) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a))))) | |
| (define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select |
pnwamk
/ eqrange_ex_1.smt2
Created
June 29, 2020 17:12
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; main.block_0_201340.1 (0x201354). jump precondition: (= (mcstack (bvsub stack_high (_ bv8 64)) (_ BitVec 64)) (fnstart rbp)) | |
| (set-logic ALL) | |
| (set-option :produce-models true) | |
| (define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0)) | |
| (define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select m (bvadd a (_ bv7 64))) (concat (select m (bvadd a (_ bv6 64))) (concat (select m (bvadd a (_ bv5 64))) (concat (select m (bvadd a (_ bv4 64))) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a))))))))) | |
| (define-fun mem_writebv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64)) (v (_ BitVec 32))) (Array (_ BitVec 64) (_ BitVec 8)) (store (store (store (store m a ((_ extract 7 0) v)) (bvadd a (_ bv1 64)) ((_ extract |
pnwamk
/ actual.add_block_0_201320_0.smt2
Created
June 24, 2020 23:20
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; 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 |
pnwamk
/ expected.add_block_0_201320_0.smt2
Created
June 24, 2020 22:59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; add.block_0_201320.1 (0x201320). Machine code write at 0x201320 is in unreserved stack space. | |
| (set-logic ALL_SUPPORTED) | |
| (set-option :produce-models true) | |
| (define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0)) | |
| (define-fun mem_readbv8 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 8) (select m a)) | |
| (define-fun mem_readbv16 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 16) (concat (select m (bvadd a (_ bv1 64))) (select m a))) | |
| (define-fun mem_readbv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 32) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a))))) | |
| (define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select m (bvadd a (_ bv7 64))) (concat |
pnwamk
/ rewritten-jump-table.diss
Created
March 25, 2020 15:51
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| test-switch-jump-table.clang.nostdlib.x86_64.re.exe: file format elf64-x86-64 | |
| Disassembly of section .text: | |
| 00000000004000f0 <mod_5>: | |
| 4000f0: e9 0b ff 20 00 jmpq 610000 <__renovate_mod_5> | |
| 4000f5: cc int3 | |
| 4000f6: cc int3 | |
| 4000f7: cc int3 |
pnwamk
/ orig-jump-table.diss
Created
March 25, 2020 15:50
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| test-switch-jump-table.clang.nostdlib.x86_64.exe: file format elf64-x86-64 | |
| Disassembly of section .text: | |
| 00000000004000f0 <mod_5>: | |
| 4000f0: 55 push %rbp | |
| 4000f1: 48 89 e5 mov %rsp,%rbp | |
| 4000f4: 48 89 7d f0 mov %rdi,-0x10(%rbp) | |
| 4000f8: 48 89 75 e8 mov %rsi,-0x18(%rbp) |
pnwamk
/ kw-opt-strategy.txt
Last active
May 25, 2018 17:28
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| For _annotated_ kw/optional-argument functions: | |
| 1. Partition the arguments into the following categories: | |
| a. mandatory | |
| b. optional, non-immediate, reachable | |
| c. optional, non-immediate, unreachable | |
| d. optional, immediate, reachable | |
| e. optional, immediate, unreachable | |
| 2. Check the body at a function type where: | |
| a. Each mandatory argument has it's annotated type |
pnwamk
/ env-printing.rkt
Created
May 22, 2018 18:59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #lang racket/base | |
| (require (for-syntax racket/base)) | |
| (begin-for-syntax | |
| (struct env (types props aliases) #:transparent) | |
| (define lexical-env (make-parameter (env '() '() '())))) | |
| (define-syntax (LET stx) |
pnwamk
/ Typed Racket HEAD instructions
Created
May 22, 2018 17:57
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 0. download and set up a racket snapshot (https://pre.racket-lang.org/) | |
| 1. cd to the root racket folder for that snapshot install | |
| 2. mkdir extra-pkgs && cd extra-pkgs | |
| 3. git clone https://github.com/racket/typed-racket.git | |
| 4. cd typed-racket | |
| 5. raco pkg install --auto -i --no-setup --skip-installed typed-racket-test | |
| 6. raco pkg update -i --auto --no-setup source-syntax/ typed-racket-lib/ typed-racket-more/ typed-racket-compatibility/ typed-racket-doc/ typed-racket/ typed-racket-test/ | |
| 7. raco setup typed typed-racket typed-racket-test typed-scheme |
pnwamk
/ plot2d_rkt.zo.diff
Created
May 22, 2018 15:38
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 51c51 | |
| < (lambda (arg0-69 arg1-70 arg2-71) | |
| --- | |
| > (lambda (arg0-65 arg1-66 arg2-67) | |
| 53c53 | |
| < #<path:/home/pnwamk/Repos/plt/snap-22may/share/pkgs/plot-gui-lib/plot/private/gui/compiled/plot2d.rkt> | |
| --- | |
| > #<path:/home/pnwamk/Repos/plt/reduce-expansion/racket/share/pkgs/plot-gui-lib/plot/private/gui/compiled/plot2d.rkt> | |
| 129,142c129,142 | |
| < (let ((local72 |