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" }]
    }
  ]
};

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

const scope = new Scope({ x: "x" });
scope.execute({ type: "set", var: "" })
scope.execute({ type: "return", value: "x" });
console.log(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 ${statement.type}`)
  }
}

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

console.log(symoblicExecuteFunction(myFunc));

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