Skip to content

Instantly share code, notes, and snippets.

View DieracDelta's full-sized avatar
💭
2565 7B91 AD2D 02C6 1B7F 9819 E682 81EB 2ABC E9B8

Justin Restivo DieracDelta

💭
2565 7B91 AD2D 02C6 1B7F 9819 E682 81EB 2ABC E9B8
83 followers · 75 following
View GitHub Profile
@DieracDelta
DieracDelta / model
Created July 22, 2020 18:11
Model:
ZF |-> 0x0
SF |-> 0x0
RSP |-> 0x0000000040000000
RBX |-> 0x000000003fffffed
RAX |-> 0x0000000000000000
PF |-> 0x0
OF |-> 0x0
CF |-> 0x0
AF |-> 0x0
@DieracDelta
DieracDelta / main_1.cfg
Created July 22, 2020 18:15
digraph {
node[shape=box];
subgraph "cluster__start" {
label="_start"
"\%0000001c"[label="\%0000001c
0000002f: RSP := RSP - 8\l00000032: mem := mem with [RSP, el]:u64 <- 0x4000E5\l00000035: call @main with noreturn\l"]
}
"\%0000001c" -> "\%0000002b";
@DieracDelta
DieracDelta / main_2.cfg
Created July 22, 2020 18:16
digraph {
node[shape=box];
subgraph "cluster__start" {
label="_start"
"\%0000002b"[label="\%0000002b
0000003e: RSP := RSP - 8\l00000041: mem := mem with [RSP, el]:u64 <- 0x4000E6\l00000044: call @main with noreturn\l"]
}
"\%0000002b" -> "\%0000003a";
@DieracDelta
DieracDelta / tmp
Created July 27, 2020 21:37
rm -f main
gcc-8 -O2 -Wall -o main main.c
#gcc -O0 -Wall -o main main.c
#clang -O3 -o main main.c
Evaluating precondition.
Checking precondition with Z3.
Z3 :
(declare-fun RDI0 () (_ BitVec 64))
(declare-fun RSP0 () (_ BitVec 64))
(declare-fun RBX0 () (_ BitVec 64))
@DieracDelta
DieracDelta / is_dumpdir
Created July 28, 2020 13:09
real 0m31.930s
user 0m28.753s
sys 0m3.158s
dir_result)
0012a6c7: is_dumpdir_result :: out u32 = RAX
000ccd2c:
000ccd31: RAX := pad:64[pad:32[mem[RDI + 0x188]]]
000ccd3e: #27613 := low:8[RAX]
000ccd41: OF := 0
@DieracDelta
DieracDelta / mb_copy
Created July 28, 2020 13:13
real 1m3.383s
user 1m0.163s
sys 0m3.191s
result)
0012a704: mb_copy_result :: out u32 = RAX
0000196e:
00001975: #259 := RBP
00001978: RSP := RSP - 8
0000197b: mem := mem with [RSP, el]:u64 <- #259
@DieracDelta
DieracDelta / mb_copy
Created July 28, 2020 13:19
real 1m3.016s
user 0m59.842s
sys 0m3.154s
esult)
0012a704: mb_copy_result :: out u32 = RAX
0000196e:
00001975: #259 := RBP
00001978: RSP := RSP - 8
0000197b: mem := mem with [RSP, el]:u64 <- #259
@DieracDelta
DieracDelta / is_dumpdir
Created July 28, 2020 13:19
real 0m31.460s
user 0m28.338s
sys 0m3.103s
dir_result)
0012a6c7: is_dumpdir_result :: out u32 = RAX
000ccd2c:
000ccd31: RAX := pad:64[pad:32[mem[RDI + 0x188]]]
000ccd3e: #27613 := low:8[RAX]
000ccd41: OF := 0
@DieracDelta
DieracDelta / main.c
Created July 29, 2020 15:29
#include <assert.h>
#include <stdint.h>
#include <stdbool.h>
#include <stdio.h>
#define GET_ELEMENT(index, input) (( (input) >> (2 * (index))) & 0x3)
void print_board(uint32_t board){
for(int row = 0; row < 4; row++){
for(int col = 0; col < 4; col++){
@DieracDelta
DieracDelta / perf_nums
Created September 23, 2020 16:51
Evaluating precondition.
Call graph 'bap wp --func=encode_nqueens_net --trip-asserts --num-unroll=0 -- bin/main_4':
------------------------------------------------------------------------------------------
[ 198.32G cycles in 1 calls ] - 98.89% : Src/precondition.check
[ 198.32G cycles in 1 calls ] | - 100.00% : Src/constraint.eval
[ 198.32G cycles in 1 calls ] | | - 100.00% : Src/constraint.eval_aux
[ 13.50G cycles in 20546138 calls ] | | | - 6.81% : Src/constraint.update_stats
Note: Nodes accounting for less than 1.00% of their parent have been ignored.