Concolic driver

[butterunderflow]

No description provided.

[butterunderflow]

This PR is still a work in progress. I’d like to discuss something about path exploration in today’s meeting.

[ahuoguo]

might be worth trying to call 2 in the x^2 + y^2 = 25 branch since it's easier to check the results. (also concolic execution allegedly tries to deal with this kinda of non-linear constraint (eg: https://faculty.sist.shanghaitech.edu.cn/faculty/songfu/cav/CT-slides.pdf)

PS: they seem to take the example from CACM https://dl.acm.org/doi/fullHtml/10.1145/2408776.2408795

[ahuoguo]

Also, in the logs, I saw the following output:

solving constrains: (declare-fun sym_0 () Int)
(assert (= 1 0))
(assert (not (= (ite (<= sym_0 0) 1 0) 0)))

Where does the (assert (= 1 0)) come from?

[butterunderflow]

Also, in the logs, I saw the following output:

solving constrains: (declare-fun sym_0 () Int)
(assert (= 1 0))
(assert (not (= (ite (<= sym_0 0) 1 0) 0)))

Where does the (assert (= 1 0)) come from?

It comes from the second if instruction when the first if's condition is true. In this case, when the first if condition evaluates to true, the second if's condition will always be 1. Reverting its path condition (not (= 1 0)) yields (= 1 0).

[ahuoguo]

Also, in the logs, I saw the following output:

solving constrains: (declare-fun sym_0 () Int)
(assert (= 1 0))
(assert (not (= (ite (<= sym_0 0) 1 0) 0)))

Where does the (assert (= 1 0)) come from?

It comes from the second if instruction when the first if's condition is true. In this case, when the first if condition evaluates to true, the second if's condition will always be 1. Reverting its path condition (not (= 1 0)) yields (= 1 0).

I see in a sense the exploration tree is different from the original branch.c program:

int f(int x, int y) {
  if (x <= 0 || y <= 0) return -1;
  if (x * x + y * y == 25) {
    // x = 3, y = 4
    return 1;
  }
  return 0;
}

changes to something like

int f(int x, int y) {
  int cond;
  if (x <= 0) {
    cond = 1;
  } else {
    cond = (y <= 0);
  }

  if (cond) {
    return 1;
  }

  if (x * x + y * y == 25) {
    // x = 3, y = 4
    return 1;
  }
  return 0;
}

TBH I might fall back to using i32.or just for a simpler exploration tree

[Kraks]

I see in a sense the exploration tree is different from the original branch.c program:

int f(int x, int y) {
  if (x <= 0 || y <= 0) return -1;
  if (x * x + y * y == 25) {
    // x = 3, y = 4
    return 1;
  }
  return 0;
}

changes to something like

int f(int x, int y) {
  int cond;
  if (x <= 0) {
    cond = 1;
  } else {
    cond = (y <= 0);
  }

  if (cond) {
    return 1;
  }

  if (x * x + y * y == 25) {
    // x = 3, y = 4
    return 1;
  }
  return 0;
}

That just looks like because compiling to webassembly changes the control-flow structure?

[ahuoguo]

That just looks like because compiling to webassembly changes the control-flow structure?

But in the previous program I can hardly imagine something like assert (0 == 1) will happen