smt errors when using solve_one with a symbolic buffer

murmus commented 7 years ago

python script: https://gist.github.com/murmus/22084226c52db4048056ad95d696a49a c source: https://gist.github.com/murmus/03b615047c2ce93395d4cd5c4540eedf traceback: https://gist.github.com/murmus/deede2d6a0c2b0ecbe1cc67dff120bd7

Summary of the problem

Calling solve_one with a buffer that has been created with new_symbolic_buffer appears to cause an SMT error

Expected behavior

According to mark, this solve_one should return a concrete buffer that fits the constraints, so at line 21 of the python script, I would get a concrete buffer that fits my constraints.

Actual behavior

I get an smt error (shown in the traceback) since I added the buffer_2 declaration multiple times.

offlinemark commented 7 years ago

saelo also triggered issue with:

for _ in range(80):
        flag.append(state.new_symbolic_value(8))

offlinemark commented 7 years ago

I believe this is something related to how ConstraintSet declarations are computed, if you examine the declarations of temp_cs before and after this line, you can see the SMTLIB variable is double declared after that line

feliam commented 6 years ago

You are saving the symbolic buffer of such state in manticore global context. m.context Maybe what you want is to save that in the local state.context.

Also for using the global shared context you need to lock. As it may be accessed from several workers.

with m.locked_context('some_global_list', list) as some_global_list:
    some_global_list.append(123213)

offlinemark commented 6 years ago

this script doesn't crash now due to the hack introduced in #653. (https://github.com/trailofbits/manticore/pull/653/files#diff-33538f83c04c8488c98e7948bf060fbdR153) related #663

offlinemark commented 6 years ago

i wasn't immediately able to get the script to work correctly, to produce input that makes the crc return 0xff. however, i when i change main to look like below, it works. this means the issue is at the api layer, and not in the core engine.

int main(int argc, char **argv){
    char *argv1 = argv[1];

    if (argv1[3] == 0) {
        unsigned ret = crc8(0, argv1, 3);
        if (ret == 0xff) {
            return 33;
        }
    }

    return 1;
}

2018-01-09 12:38:58,857: [76190] m.manticore:INFO: Loading program murmus2
2018-01-09 12:39:31,394: [76190] m.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 1
2018-01-09 12:39:32,720: [76190] m.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 33
2018-01-09 12:39:33,393: [76190] m.manticore:INFO: Generated testcase No. 2 - Program finished with exit status: 1
2018-01-09 12:39:33,398: [76190] m.manticore:INFO: Results in /mnt/hgfs/code/tmp/murmuss189/mcore_9cCv63
2018-01-09 12:39:33,399: [76190] m.manticore:INFO: Total time: 33.6162781715

ehennenfent commented 4 years ago

As it's been over two years, and it looks like the smtlib API issue has been resolved, I'm going to close this.

trailofbits / manticore