gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

Figure out why sometimes paths are sometimes not preserved #2

Open gernst opened 2 years ago

gernst commented 2 years ago

For example sv-benchmarks/c/seq-pthread/cs_sync.i fails to preserve some path (see below). Probably something wrong with the generated path constraints. Two places we should check are the simplifications performed for extract and concat in runtime/Runtime.cpp

?                                  input: 
partial trace:  abort
< 0
+ 0
? 0                                input: 623b8c595106208141fb3ea17c43ac957bc886bb261b7c942ca226aeb9a0af7588340cc72639c2516cd81fa5f90d47
partial trace:  abort
< 0
? 1                                input: db6afcf0d5c1ff5cd4d3b775d0256483ffee002723f75056bbe23dbc70302f404483121816bdaae900593132634000
partial trace:  abort
< 111010
+ 111010
e 11100                           
? 10                               input: af97adf6e61989e90061fbc082ecd5b65d16b4026552b491c30b0d84679fb5764c2735df2f08bc39990276d058f501f67ead4fe6
partial trace:  abort
< 110
! 110

current tree
      local      subtree
   win  try     win  try    path
*    1    1       2    5    
?    0    1       0    1    0
?    0    1       0    1    10
?    0    0       0    0    110
e    0    1       0    1    11100
?    0    0       0    0    111010
?    0    0       0    0    111011
?    0    0       0    0    1111
Traceback (most recent call last):
  File "Legion.py", line 711, in <module>
    raise e
  File "Legion.py", line 705, in <module>
    raise Exception("failed to preserve prefix (naive sampler is precise)")
Exception: failed to preserve prefix (naive sampler is precise)