my simple concolic execution demo

this is a concolic executor on minimal C, currently only support:

• int (with no bound)
• bool
• + operator of int
• == operator of int

this project is a (bad and minimal) re-implementation in C++ of the cs6.858's symbolic lab

try it!

git clone https://github.com/chujDK/concolic-cpp.git
cd concolic-cpp && mkdir build && cd build
cmake ..
make
./concolic-cpp-test

this will concolic execute this function

int testf(int a, int b) {
  if (a == b) {
    return a + b;
  } else {
    if (a == 1) {
      return a + 4;
    } else {
      return b;
    }
  }
}

and produce out put like

{"input:" {a:{symbolic: a; concrete: 0},b:{symbolic: b; concrete: 0}} } 
[+] returned:  {symbolic: (+ a b); concrete: 0} 
explored:  [(= a b)] 
[+] setting  a  =  1 
[+] setting  b  =  0 
{"input:" {a:{symbolic: a; concrete: 1},b:{symbolic: b; concrete: 0}} } 
[+] returned:  {symbolic: (+ a 4); concrete: 5} 
explored:  [(not (= a b)),(= a 1)] 
[+] setting  a  =  2 
[+] setting  b  =  3 
{"input:" {a:{symbolic: a; concrete: 2},b:{symbolic: b; concrete: 3}} } 
[+] returned:  {symbolic: b; concrete: 3} 
explored:  [(not (= a b)),(not (= a 1))]

you can see it explored all the paths