Symbolic Execution with Algebrite

by Josh Pullen

HTML

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

JavaScript

const initialState = { a: "α", b: "β" };

/*
const program = [
  { type: "assign", var: "a", value: "3" },
  { type: "assert", condition: "a == 3" },
  {
  	type: "if",
    condition: "b < 0",
    branchA: [{ type: "assert", condition: "b < a" }],
    branchB: [{ type: "assert", condition: "b > a" }]
  }
];
*/

const program = [
	{
  	type: "if",
    condition: "a < 5",
    branchA: [{ type: "assign", var: "a", value: "5" }],
    branchB: []
  },
  {
  	type: "if",
    condition: "b < a",
    branchA: [{ type: "assign", var: "b", value: "a" }],
    branchB: []
  },
  {
  	type: "if",
    condition: "a + b > 15",
    branchA: [{ type: "assign", var: "b", value: "b - a" }],
    branchB: []
  },
  { type: "assert", condition: "a + b >= 10" }
];

function substitute(expression, state) {
	for (const [varName, value] of Object.entries(state)) {
  	expression = expression.replaceAll(varName, value);
  }
  return expression;
}

function getSymbolicAssertions(program, state, pathCondition = "true") {
	let assertions = [];

	for (let index = 0; index < program.length; index++) {
    const statement = program[index];
    switch (statement.type) {
      case "assign":
        state = { ...state, [statement.var]: substitute(statement.value, state) };
        break;
      case "assert":
        assertions.push({
        	condition: substitute(statement.condition, state),
          given: substitute(pathCondition, state)
        });
        break;
      case "if":
      	return [
        	...getSymbolicAssertions(
          	[...statement.branchA, ...program.slice(index + 1)],
            state,
            `${pathCondition} && ${statement.condition}`
          ),
          ...getSymbolicAssertions(
          	[...statement.branchB, ...program.slice(index + 1)],
            state,
            `${pathCondition} && !(${statement.condition})`
          ),
        ];
    }
  }
  
  return assertions;
}

console.log(getSymbolicAssertions(program, initialState));