Symbolic Execution with Algebrite

by Josh Pullen

HTML

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

JavaScript

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 substitute(expression, vars) {
  // For now, do nothing
  for (const [name, value] of Object.entries(vars)) {
  	expression = expression.replaceAll(name, value);
  }
	return expression;
}

class Scope {
	constructor(vars = {}, conditions = []) {
  	this.vars = vars;
    this.conditions = conditions;
    this.returnValue = null;
  }
  
  execute(statement) {
  	switch (statement.type) {
    	case "set":
      	this.vars[statement.var] = substitute(statement.value, this.vars);
        break;
    	case "return":
        this.returnValue = substitute(statement.value, this.vars);
    }
  }
}

const scope = new Scope({ x: "đť’ł" });
scope.execute({ type: "set", var: "y", value: "2*x" });
scope.execute({ type: "return", value: "y" });
console.log(scope.vars, scope.returnValue);


/*
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...