Hi,
Is there a tool to encode a constraint solver query (e.g., from
queries.pc) into C code that, when compiled to LLVM and run in KLEE,
would generate the exact same query as in the log? This may help me
speed up debugging the attached query that is reported as invalid by
KLEE but valid by kleaver.
Thanks,
Vitaly
# Query 23909 -- Type: Truth, Instructions: 7015991
array v_NdisReadConfigurationRet_success20[4] : w32 -> w8 = symbolic
array v_MediumArraySize17[4] : w32 -> w8 = symbolic
array v_MediumArray_02[4] : w32 -> w8 = symbolic
array v_NdisReadConfigurationRet_CardType_value19[4] : w32 -> w8 = symbolic
array v_NdisAllocateMemoryRet18[4] : w32 -> w8 = symbolic
array v_NdisMRegisterMiniportRet1[4] : w32 -> w8 = symbolic
array v_NdisReadConfigurationRet_success248[4] : w32 -> w8 = symbolic
array v_NdisReadConfigurationRet_success55[4] : w32 -> w8 = symbolic
array arr125inb0000c107_806f68be[1] : w32 -> w8 = symbolic
array v_NdisReadNetworkAddressRet_success86[4] : w32 -> w8 = symbolic
array v_regadapter5c554[4] : w32 -> w8 = symbolic
array v_QuerySetInfoBufferSize1239[4] : w32 -> w8 = symbolic
array arr445inb0000c103_806f68be[1] : w32 -> w8 = symbolic
array v_QuerySetInformationHandler_OID1237[4] : w32 -> w8 = symbolic
array const_arr2[128] : w32 -> w8 = [85 139 69 8 139 128 244 1 0 0 235 28 139
69 8 139 128 240 1 0 0 235 17 139 69 8 139 128 248 1 0 0 235 6 139 69 8 139 64
108 137 69 8 59
85 20 118 14 139 69 28 199 69 252 20 0 1 192 137 16 235 24 139 125 16 139 202
139 193 193 233 2 243 165 139 200 139 69 24 131 225 3 243 164 1 16 139 69 252
95 94 201 194 24 0 65 211 131 252 80 211 131 252 91 211 131 252 91 211 131 252
99 211 131 252 111 211 131 252 123 211 131 252 135 211 131 252 149]
array arr219inb0000c106_806f68be[1] : w32 -> w8 = symbolic
array arr218inb0000c100_806f68be[1] : w32 -> w8 = symbolic
array arr220inb0000c105_806f68be[1] : w32 -> w8 = symbolic
array const_arr3[128] : w32 -> w8 = [211 131 252 173 211 131 252 173 211 131
252 185 211 131 252 212 211 131 252 248 212 131 252 237 211 131 252 251 211 131
252 9 212 131 252 248 212 131 252 21 212 131 252 67 212 131 252 81 212 131 252
225 211 131 252 204 85 139 236 139 77 12 83 86 51 246 51 192 129 233 14 1 1 0
87 15 132 131 0 0 0 73 116 91
129 233 244 255 255 0 116 7 184 23 0 1 192 235 126 139 77 20 106 6 139 193 51
210 95 247 247 133 210 117 105 139 93 8 139 117 16 139 193 106 6 141 187 24]
array v_IsFakeOid1238[1] : w32 -> w8 = symbolic
array arr221inb0000c10e_806f68be[1] : w32 -> w8 = symbolic
array arr122inb0000c100_806f68be[1] : w32 -> w8 = symbolic
array v_NdisMRegisterIoPortRangeRet903[4] : w32 -> w8 = symbolic
array v_NdisReadConfigurationRet_success490[4] : w32 -> w8 = symbolic
(query [(Eq false
(Slt (And w32 (Sub w32 (w32 0)
(ZExt w32 (Ult (w32 0)
(ReadLSB w32 0
v_NdisMRegisterMiniportRet1))))
(w32 3221225473))
(w32 0)))
(Ule N0:(ReadLSB w32 0 v_MediumArraySize17)
(w32 15))
(Ult (w32 0) N0)
(Eq (w32 0)
(ReadLSB w32 0 v_MediumArray_02))
(Eq (w32 0)
(ReadLSB w32 0 v_NdisAllocateMemoryRet18))
(Eq (w32 0)
(ReadLSB w32 0 v_NdisReadConfigurationRet_success20))
(Eq false
(Eq (w32 0)
(ReadLSB w32 0 v_NdisReadConfigurationRet_success55)))
(Eq false
(Eq (w32 0)
(ReadLSB w32 0 v_NdisReadNetworkAddressRet_success86)))
(Eq false
(Eq (w32 0)
(ReadLSB w32 0 v_NdisReadConfigurationRet_success248)))
(Eq false
(Eq (w32 0)
(ReadLSB w32 0 v_NdisReadConfigurationRet_success490)))
(Eq false
(Ult (w32 12)
N1:(ReadLSB w32 0 v_regadapter5c554)))
(Eq (w32 0)
(ReadLSB w32 0 v_NdisMRegisterIoPortRangeRet903))
(Eq false
(Eq (w32 0)
(And w32 (ZExt w32 (Read w8 0 arr122inb0000c100_806f68be))
(w32 1))))
(Eq (w32 1)
(ReadLSB w32 0 v_NdisReadConfigurationRet_CardType_value19))
(Eq false
(Eq (w32 0)
(And w32 (ZExt w32 (Read w8 0 arr125inb0000c107_806f68be))
(w32 128))))
(Eq false (Ult (w32 0) N1))
(Eq (w32 0)
(And w32 (Add w32 (w32 4294967263)
(And w32 (And w32 (ZExt w32 (Read w8 0
arr218inb0000c100_806f68be))
(w32 255))
(w32 4294967073)))
(w32 255)))
(Eq false
(Eq (w32 0)
(And w32 (Add w32 (w32 4294967255)
(And w32 (ZExt w32 (Read w8 0
arr221inb0000c10e_806f68be))
(w32 255)))
(w32 255))))
(Eq false
(Eq (w32 0)
(And w32 (Or w32 (And w32 (ZExt w32 (Read w8 0
arr219inb0000c106_806f68be))
(w32 64))
(And w32 (ZExt w32 (Read w8 0
arr220inb0000c105_806f68be))
(w32 128)))
(w32 192))))
(Eq (w32 0)
(And w32 (ZExt w32 (Read w8 0 arr445inb0000c103_806f68be))
(w32 4)))
(Eq (w8 1) (Read w8 0 v_IsFakeOid1238))
(Ule (ReadLSB w32 0 v_QuerySetInfoBufferSize1239)
(w32 64))
(Eq false
(Ult (w32 131329)
N2:(ReadLSB w32 0 v_QuerySetInformationHandler_OID1237)))
(Eq (w32 0)
(And w32 (Select w32 (Eq (w32 131329) N2) (w32 64) (w32 0))
(w32 64)))
(Eq false
(Ult (w32 21) N3:(Add w32 (w32 4294901503) N2)))
(Eq (w32 33097642)
(LShr w32 N4:(Add w32 (w32 4236498271) (Shl w32 N3 (w32 2)))
(w32 7)))
(Ult (w32 127)
(Add w32 (w32 3) (And w32 N4 (w32 127))))
(Eq (w32 33097643)
(LShr w32 N5:(Add w32 (w32 4) N6:(And w32 N4 (w32 4294967292)))
(w32 7)))]
(Eq false
(Eq (w32 1)
(Or w32 (Shl w32 (ReadLSB w32 N7:(Extract w32 0 (Add w64 (w64
18446744069473053312) (ZExt w64 N5))) const_arr3)
(Sub w32 (w32 32)
N8:(And w32 (Shl w32 N4 (w32 3)) (w32 24))))
(LShr w32 (ReadLSB w32 N9:(Extract w32 0 (Add w64 (w64
18446744069473053440) (ZExt w64 N6))) const_arr2)
N8)))))
# OK -- Elapsed: 0.0367539
# Is Valid: false
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
