Symbolic Execution with Algebrite

by Josh Pullen

HTML

<script src="https://unpkg.com/[email protected]/dist/algebrite.bundle-for-browser.js"></script>

JavaScript

/*

function test(x) {
	if (x < 3) {
  	return 3;
  } else {
  	return x;
  }
}

*/

const myFunc = {
  inputs: ["x"],
  statements: [{
      type: "if",
      condition: "x < 5",
      caseA: [{
        type: "if",
        condition: "x < 3",
        caseA: [{
          type: "return",
          value: "3"
        }],
        caseB: [{
          type: "return",
          value: "x < 3"
        }]
      }],
      caseB: [{
        type: "return",
        value: "100"
      }]
    }

  ]
}

function symbolicExecute(inputs, statements) {
  const statement = statements[0];
  switch (statement.type) {
    case "if": {
      const caseAResult = symbolicExecute(inputs, statement.caseA);
      const caseBResult = symbolicExecute(inputs, statement.caseB);
      return [
        ...caseAResult.map(({
          condition,
          value
        }) => ({
          condition: Algebrite.run(`simplify(and(${condition}, ${statement.condition}))`),
          value
        })),
        ...caseBResult.map(({
          condition,
          value
        }) => ({
          condition: Algebrite.run(`simplify(and(${condition}, not(${statement.condition})))`),
          value
        }))
      ];
    }
    case "return": {
      return [{
        condition: "1",
        value: Algebrite.run(statement.value)
      }]
    }
    default:
      throw new Error(`I don't recognize statement type ${statement.type}`)
  }
}

function symoblicExecuteFunction(func) {
  return symbolicExecute(func.inputs, func.statements);
}

console.log(symoblicExecuteFunction(myFunc));

// console.log(Algebrite.run("x < 3"));