qiaokang92/P4wn

Klee doesn't work correctly, can someone give me a hand?

JeremyGuo opened this issue · 1 comments

I ran the command

python P4_to_C.py heavy-hitter.json

clang-6.0 -I /home/jeremyguo/P4wn/include/klee/ -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone heavy-hitter.c

p4wn --num-trace-pkt 10000 --real-trace 1 --program-num 1 --num-loop 3 --batch-instructions=1000 --converge-delta 1e-10 heavy-hitter.bc

and got the result below:

KLEE: the input file name is: heavy-hitter.bc

KLEE: output directory is "/home/jeremyguo/assert-p4/src/klee-out-0"
new ht handler created!
new bf handler created!
new Cmin handler created!
new MA handler created!
KLEE: WARNING: real trace enabled
[LOG] QueryHandler:68: creating query handler, prog=netwarden, profile=1, query trace enabled
KLEE: Using STP solver backend
KLEE: entry function is main.
KLEE: WARNING: undefined reference to function: klee_print_once
KLEE: WARNING: undefined reference to function: update_checksum
KLEE: else branch!
KLEE: KLEE: using no seeds
KLEE: RunInDir is empty
[LOG] runFunctionAsMain:4302: starting a new state for function main
[LOG] run:3395: it is a full PSE run
[LOG] handleMakeSymbolic:849: loop 0
[LOG] handleMakeSymbolic:849: loop 0
[LOG] handleMakeSymbolic:849: loop 0
[LOG] executeInstruction:2007: state[0]: arrived at a probabilistic branch, prob=1, line=121
[LOG] ExecutionState:164: forking a new state from 0 to 1
[LOG] queryTraceByLine:341: querying trace for netwarden line=121
[LOG] getOpsFromLine:201: prog=netwarden, getting ops from line=121
(Eq 2048
     (Extract w32 0 (LShr w64 (ReadLSB w64 8 hdr)
                              48)))
do not find, try to find in the json file!

I've done some modification on P4_to_C.py to fix the IR changed problem