[klee-dev] How to Interpret Klee Path Predicate
Azizul Hakim
azizulfahim2002 at gmail.com
Mon Mar 21 05:36:47 GMT 2016
How do we interpret the path predicates generated by KLEE. I've the
following path predicates generated by S2E tool which uses KLEE. This
predicate is generated from one branch of an IF-ELSE statement.
__tmpInt8 : BITVECTOR(8);
__tmpInt16 : BITVECTOR(16);
__tmpInt32 : BITVECTOR(32);
__tmpInt64 : BITVECTOR(64);
v0_pos_0_0x7ff554dfc4a0 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
const_arr1_0x7ff55532c2d0 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
%----------------------------------------------------
ASSERT( ( NOT( (0x00000403 = (0x00020403 & ((0x000000 @
v0_pos_0_0x7ff554dfc4a0[0x00000000]
)[23:0] @ 0x00
)
)
))) );
ASSERT( ( NOT( SBVGT(0x00000000,IF((0b1 =
v0_pos_0_0x7ff554dfc4a0[0x00000003][7:7]
))
THEN 0xFFFFFFFF
ELSE 0x00000000
ENDIF)
)) );
ASSERT( ( NOT( SBVGT(IF((0b1 = v0_pos_0_0x7ff554dfc4a0[0x00000003][7:7]
))
THEN 0xFFFFFFFF
ELSE 0x00000000
ENDIF,0x000007FF)
)) );
ASSERT( (LET let_k_0 = IF((0b1 = v0_pos_0_0x7ff554dfc4a0[0x00000003][7:7]
))
THEN 0xFFFFFFFF
ELSE 0x00000000
ENDIF,
let_k_1 = BVPLUS(32,
0xFFFFF801,
let_k_0)
IN
( NOT( (0b0 = BVXOR((0b00000000000 @ (0x00000 @ (BVXOR(0x000007FF,let_k_0)
& BVXOR(let_k_0,let_k_1)
)[31:20]
)[31:11]
),(0b0000000 @ ((0x000000 @ let_k_1[31:24]
) | (0x000000 @
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((const_arr1_0x7ff55532c2d0
WITH [0x00000000] := 0x04)
WITH [0x00000001] := 0x00)
WITH [0x00000002] := 0x00)
WITH [0x00000003] := 0x04)
WITH [0x00000004] := 0x00)
WITH [0x00000005] := 0x04)
WITH [0x00000006] := 0x04)
WITH [0x00000007] := 0x00)
WITH [0x00000008] := 0x00)
WITH [0x00000009] := 0x04)
WITH [0x0000000A] := 0x04)
WITH [0x0000000B] := 0x00)
WITH [0x0000000C] := 0x04)
WITH [0x0000000D] := 0x00)
WITH [0x0000000E] := 0x00)
WITH [0x0000000F] := 0x04)
WITH [0x00000010] := 0x00)
WITH [0x00000011] := 0x04)
WITH [0x00000012] := 0x04)
WITH [0x00000013] := 0x00)
WITH [0x00000014] := 0x04)
WITH [0x00000015] := 0x00)
WITH [0x00000016] := 0x00)
WITH [0x00000017] := 0x04)
WITH [0x00000018] := 0x04)
WITH [0x00000019] := 0x00)
WITH [0x0000001A] := 0x00)
WITH [0x0000001B] := 0x04)
WITH [0x0000001C] := 0x00)
WITH [0x0000001D] := 0x04)
WITH [0x0000001E] := 0x04)
WITH [0x0000001F] := 0x00)
WITH [0x00000020] := 0x00)
WITH [0x00000021] := 0x04)
WITH [0x00000022] := 0x04)
WITH [0x00000023] := 0x00)
WITH [0x00000024] := 0x04)
WITH [0x00000025] := 0x00)
WITH [0x00000026] := 0x00)
WITH [0x00000027] := 0x04)
WITH [0x00000028] := 0x04)
WITH [0x00000029] := 0x00)
WITH [0x0000002A] := 0x00)
WITH [0x0000002B] := 0x04)
WITH [0x0000002C] := 0x00)
WITH [0x0000002D] := 0x04)
WITH [0x0000002E] := 0x04)
WITH [0x0000002F] := 0x00)
WITH [0x00000030] := 0x04)
WITH [0x00000031] := 0x00)
WITH [0x00000032] := 0x00)
WITH [0x00000033] := 0x04)
WITH [0x00000034] := 0x00)
WITH [0x00000035] := 0x04)
WITH [0x00000036] := 0x04)
WITH [0x00000037] := 0x00)
WITH [0x00000038] := 0x00)
WITH [0x00000039] := 0x04)
WITH [0x0000003A] := 0x04)
WITH [0x0000003B] := 0x00)
WITH [0x0000003C] := 0x04)
WITH [0x0000003D] := 0x00)
WITH [0x0000003E] := 0x00)
WITH [0x0000003F] := 0x04)
WITH [0x00000040] := 0x00)
WITH [0x00000041] := 0x04)
WITH [0x00000042] := 0x04)
WITH [0x00000043] := 0x00)
WITH [0x00000044] := 0x04)
WITH [0x00000045] := 0x00)
WITH [0x00000046] := 0x00)
WITH [0x00000047] := 0x04)
WITH [0x00000048] := 0x04)
WITH [0x00000049] := 0x00)
WITH [0x0000004A] := 0x00)
WITH [0x0000004B] := 0x04)
WITH [0x0000004C] := 0x00)
WITH [0x0000004D] := 0x04)
WITH [0x0000004E] := 0x04)
WITH [0x0000004F] := 0x00)
WITH [0x00000050] := 0x04)
WITH [0x00000051] := 0x00)
WITH [0x00000052] := 0x00)
WITH [0x00000053] := 0x04)
WITH [0x00000054] := 0x00)
WITH [0x00000055] := 0x04)
WITH [0x00000056] := 0x04)
WITH [0x00000057] := 0x00)
WITH [0x00000058] := 0x00)
WITH [0x00000059] := 0x04)
WITH [0x0000005A] := 0x04)
WITH [0x0000005B] := 0x00)
WITH [0x0000005C] := 0x04)
WITH [0x0000005D] := 0x00)
WITH [0x0000005E] := 0x00)
WITH [0x0000005F] := 0x04)
WITH [0x00000060] := 0x04)
WITH [0x00000061] := 0x00)
WITH [0x00000062] := 0x00)
WITH [0x00000063] := 0x04)
WITH [0x00000064] := 0x00)
WITH [0x00000065] := 0x04)
WITH [0x00000066] := 0x04)
WITH [0x00000067] := 0x00)
WITH [0x00000068] := 0x00)
WITH [0x00000069] := 0x04)
WITH [0x0000006A] := 0x04)
WITH [0x0000006B] := 0x00)
WITH [0x0000006C] := 0x04)
WITH [0x0000006D] := 0x00)
WITH [0x0000006E] := 0x00)
WITH [0x0000006F] := 0x04)
WITH [0x00000070] := 0x00)
WITH [0x00000071] := 0x04)
WITH [0x00000072] := 0x04)
WITH [0x00000073] := 0x00)
WITH [0x00000074] := 0x04)
WITH [0x00000075] := 0x00)
WITH [0x00000076] := 0x00)
WITH [0x00000077] := 0x04)
WITH [0x00000078] := 0x04)
WITH [0x00000079] := 0x00)
WITH [0x0000007A] := 0x00)
WITH [0x0000007B] := 0x04)
WITH [0x0000007C] := 0x00)
WITH [0x0000007D] := 0x04)
WITH [0x0000007E] := 0x04)
WITH [0x0000007F] := 0x00)
WITH [0x00000080] := 0x00)
WITH [0x00000081] := 0x04)
WITH [0x00000082] := 0x04)
WITH [0x00000083] := 0x00)
WITH [0x00000084] := 0x04)
WITH [0x00000085] := 0x00)
WITH [0x00000086] := 0x00)
WITH [0x00000087] := 0x04)
WITH [0x00000088] := 0x04)
WITH [0x00000089] := 0x00)
WITH [0x0000008A] := 0x00)
WITH [0x0000008B] := 0x04)
WITH [0x0000008C] := 0x00)
WITH [0x0000008D] := 0x04)
WITH [0x0000008E] := 0x04)
WITH [0x0000008F] := 0x00)
WITH [0x00000090] := 0x04)
WITH [0x00000091] := 0x00)
WITH [0x00000092] := 0x00)
WITH [0x00000093] := 0x04)
WITH [0x00000094] := 0x00)
WITH [0x00000095] := 0x04)
WITH [0x00000096] := 0x04)
WITH [0x00000097] := 0x00)
WITH [0x00000098] := 0x00)
WITH [0x00000099] := 0x04)
WITH [0x0000009A] := 0x04)
WITH [0x0000009B] := 0x00)
WITH [0x0000009C] := 0x04)
WITH [0x0000009D] := 0x00)
WITH [0x0000009E] := 0x00)
WITH [0x0000009F] := 0x04)
WITH [0x000000A0] := 0x04)
WITH [0x000000A1] := 0x00)
WITH [0x000000A2] := 0x00)
WITH [0x000000A3] := 0x04)
WITH [0x000000A4] := 0x00)
WITH [0x000000A5] := 0x04)
WITH [0x000000A6] := 0x04)
WITH [0x000000A7] := 0x00)
WITH [0x000000A8] := 0x00)
WITH [0x000000A9] := 0x04)
WITH [0x000000AA] := 0x04)
WITH [0x000000AB] := 0x00)
WITH [0x000000AC] := 0x04)
WITH [0x000000AD] := 0x00)
WITH [0x000000AE] := 0x00)
WITH [0x000000AF] := 0x04)
WITH [0x000000B0] := 0x00)
WITH [0x000000B1] := 0x04)
WITH [0x000000B2] := 0x04)
WITH [0x000000B3] := 0x00)
WITH [0x000000B4] := 0x04)
WITH [0x000000B5] := 0x00)
WITH [0x000000B6] := 0x00)
WITH [0x000000B7] := 0x04)
WITH [0x000000B8] := 0x04)
WITH [0x000000B9] := 0x00)
WITH [0x000000BA] := 0x00)
WITH [0x000000BB] := 0x04)
WITH [0x000000BC] := 0x00)
WITH [0x000000BD] := 0x04)
WITH [0x000000BE] := 0x04)
WITH [0x000000BF] := 0x00)
WITH [0x000000C0] := 0x04)
WITH [0x000000C1] := 0x00)
WITH [0x000000C2] := 0x00)
WITH [0x000000C3] := 0x04)
WITH [0x000000C4] := 0x00)
WITH [0x000000C5] := 0x04)
WITH [0x000000C6] := 0x04)
WITH [0x000000C7] := 0x00)
WITH [0x000000C8] := 0x00)
WITH [0x000000C9] := 0x04)
WITH [0x000000CA] := 0x04)
WITH [0x000000CB] := 0x00)
WITH [0x000000CC] := 0x04)
WITH [0x000000CD] := 0x00)
WITH [0x000000CE] := 0x00)
WITH [0x000000CF] := 0x04)
WITH [0x000000D0] := 0x00)
WITH [0x000000D1] := 0x04)
WITH [0x000000D2] := 0x04)
WITH [0x000000D3] := 0x00)
WITH [0x000000D4] := 0x04)
WITH [0x000000D5] := 0x00)
WITH [0x000000D6] := 0x00)
WITH [0x000000D7] := 0x04)
WITH [0x000000D8] := 0x04)
WITH [0x000000D9] := 0x00)
WITH [0x000000DA] := 0x00)
WITH [0x000000DB] := 0x04)
WITH [0x000000DC] := 0x00)
WITH [0x000000DD] := 0x04)
WITH [0x000000DE] := 0x04)
WITH [0x000000DF] := 0x00)
WITH [0x000000E0] := 0x00)
WITH [0x000000E1] := 0x04)
WITH [0x000000E2] := 0x04)
WITH [0x000000E3] := 0x00)
WITH [0x000000E4] := 0x04)
WITH [0x000000E5] := 0x00)
WITH [0x000000E6] := 0x00)
WITH [0x000000E7] := 0x04)
WITH [0x000000E8] := 0x04)
WITH [0x000000E9] := 0x00)
WITH [0x000000EA] := 0x00)
WITH [0x000000EB] := 0x04)
WITH [0x000000EC] := 0x00)
WITH [0x000000ED] := 0x04)
WITH [0x000000EE] := 0x04)
WITH [0x000000EF] := 0x00)
WITH [0x000000F0] := 0x04)
WITH [0x000000F1] := 0x00)
WITH [0x000000F2] := 0x00)
WITH [0x000000F3] := 0x04)
WITH [0x000000F4] := 0x00)
WITH [0x000000F5] := 0x04)
WITH [0x000000F6] := 0x04)
WITH [0x000000F7] := 0x00)
WITH [0x000000F8] := 0x00)
WITH [0x000000F9] := 0x04)
WITH [0x000000FA] := 0x04)
WITH [0x000000FB] := 0x00)
WITH [0x000000FC] := 0x04)
WITH [0x000000FD] := 0x00)
WITH [0x000000FE] := 0x00)
WITH [0x000000FF] := 0x04)
[(0x00000000000000 @ let_k_1[7:0]
)[31:0]]
)
)[31:7]
))
[0:0]
)))) );
ASSERT( (LET let_k_0 = v0_pos_0_0x7ff554dfc4a0[0x00000003] IN
(0x00000000 = (IF((0b1 = let_k_0[7:7]
))
THEN 0xFFFFFFFF
ELSE 0x00000000
ENDIF | BVXOR(0x00000014,(let_k_0 @ (v0_pos_0_0x7ff554dfc4a0[0x00000002] @
(v0_pos_0_0x7ff554dfc4a0[0x00000001] @ v0_pos_0_0x7ff554dfc4a0[0x00000000]
)
)
))
)
)) );
ASSERT( ( NOT( BVGT((v0_pos_0_0x7ff554dfc4a0[0x00000003] @
(v0_pos_0_0x7ff554dfc4a0[0x00000002] @ (v0_pos_0_0x7ff554dfc4a0[0x00000001]
@ v0_pos_0_0x7ff554dfc4a0[0x00000000]
)
)
),0xFFFFF000)
)) );
%----------------------------------------------------
QUERY( FALSE );
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list