eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
781 stars 137 forks source link

The question about std::cin #96

Open liushengahn opened 2 years ago

liushengahn commented 2 years ago

hello, I build an instrumented C++ standard library to track data. When I use syd::cin in my program, the result appears as shown in the figure.

#include <iostream>
int nested_checking(const char *buff_array)
{
    if(buff_array[0] == 'A'){
        if(buff_array[1] == 'B'){
            if(buff_array[2] == 'M'){
                return 4;
            }
            if(buff_array[2] == 'N'){
                return 5;
            }
        }
        else if(buff_array[1] == 'C'){
            if(buff_array[2] == 'D'){
                if(buff_array[3] == 'E'){
                    return 5;
                }
                if(buff_array[3] == 'F'){
                    return 6;
                }
            }
            else{
                return 1;
            }
        }
    }
    return 3;
}

int main(int argc,char** argv){
    std::string n;
    std::cin>>n;
    return nested_checking(n.c_str());
}

图片1 After symbolic execution, I got a result that starts with A, but there are a lot of redundant results. This would not have happened without std::cin. Also, there are some strategies for string symbolization (Exponential back-off as I saw in Qsym's paper, It only executes blocks whose frequency number is a power of two.)I suspect it may have introduced a loop that produced redundant results.But I'm not sure. I was hoping you could explain why. Thank you very much. I look forward to your reply.