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 < 3",
      caseA: [
      	{ type: "return", value: "3" }
      ],
      caseB: [
      	{ type: "return", value: "x < 3" }
      ]
    }
  ]
}

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"));