Abstract interpretation

c go java js lua py vbs rkt scm pro

Abstract interpretation is a programming language technique whereby the running of code (e.g., a program) is simulated.

One purpose is to transform the code to a different (e.g., more efficient in some way) form.

The Adobe PDF (Portable Document Format) is, in part, an abstract interpretation of the page description language PostScript such that loops and conditionals are removed (and certain other transformations are made). Then, some additional features are added such as meta information, font embedding support, etc.

In a C program, for example, the only statements that do anything are input, assignment, and output - primitive statements.

The other statements such as while and if effect control flow. Functions are abstractions.

An abstract interpretation of a C program with the data for that program would record just the primitive statements. The resulting program would run and just do one and only one thing - ever. That is what is done with PDF.

Let us return to the example of a stack-based expression code. Details are at Stack-based code execution .

In those example, the goal was evaluation given values for variables.

Here, only the generated code is of interest.

Consider the following example code. Here is the JavaScript code.

var codeList1 = [
	["var", "x"],
	["var", "y"],
	["op2", "and"],
	["var", "x"],
	["op1", "not"],
	["var", "y"],
	["op1", "not"],
	["op2", "and"],
	["op2", "or"]
	];
function execute(codeList1) {
	var n1 = codeList1.length;
	var stackPos1 = 0;
	for (var i1=0; i1 < n1; i1++) {
		var code1 = codeList1[i1];
		var type1 = code1[0];
		if (type1 == "var") {
			var name1 = code1[1];
			console.log("VAR "+name1+" \n");
			console.log("\tPUSH at "+stackPos1+"\n");
			stackPos1++;
			}
		else if (type1 == "op1") {
			var op1 = code1[1];
			console.log("OP1 "+op1+"\n");
			stackPos1--;
			console.log("\tPOP at "+stackPos1+"\n");
			console.log("\tPUSH at "+stackPos1+"\n");
			stackPos1++;
			}
		else if (type1 == "op2") {
			var op2 = code1[1];
			console.log("OP2 "+op2+"\n");
			stackPos1--;
			console.log("\tPOP at "+stackPos1+"\n");
			stackPos1--;
			console.log("\tPOP at "+stackPos1+"\n");
			console.log("\tPUSH at "+stackPos1+"\n");
			stackPos1++;
			}
		}
	console.log("RESULT\n");
	console.log("\tPOP at "+stackPos1+"\n");
	stackPos1--;
	}

execute(codeList1);

Here is the output of the JavaScript code.

VAR x 

	PUSH at 0

VAR y 

	PUSH at 1

OP2 and

	POP at 1

	POP at 0

	PUSH at 0

VAR x 

	PUSH at 1

OP1 not

	POP at 1

	PUSH at 1

VAR y 

	PUSH at 2

OP1 not

	POP at 2

	PUSH at 2

OP2 and

	POP at 2

	POP at 1

	PUSH at 1

OP2 or

	POP at 1

	POP at 0

	PUSH at 0

RESULT

	POP at 1

Notice that the needed stack size can be determined from the code. In this case, the stack will have exactly 3 elements on it.

The push and pop instructions do a lot of work (even without error checking). Instead of push and pop, which takes time to increment/decrement the stack pointer and then load and store from the (dynamic) stack, a fixed number of variables (variable locations) can be used, such as the following. These could be on the run-time stack or registers on a processor. Here they are variables prefixed with temp for "temporary" (expression) variables.

temp0 temp1 temp2

The above code can then be converted the the following - which can be pre-processed and part of the generated code.

Note that these temporary variables are automatically reused as they would have been on an actual stack.

In a beginning course in programming, students learn variables and then later how to replace a sequence of similar variable names with an array reference and index.

Here, the opposite is happening. An array and index references are being replaced with individual variable names (memory locations). Here is the JavaScript code.

var codeList1 = [
	["var", "x"],
	["var", "y"],
	["op2", "and"],
	["var", "x"],
	["op1", "not"],
	["var", "y"],
	["op1", "not"],
	["op2", "and"],
	["op2", "or"]
	];
function execute(codeList1) {
	var n1 = codeList1.length;
	var stackPos1 = 0;
	var stackList1 = [];
	for (var i1=0; i1 < n1; i1++) {
		var code1 = codeList1[i1];
		var type1 = code1[0];
		if (type1 == "var") {
			var name1 = code1[1];
			console.log("VAR "+name1+" \n");
			stackList1.push(name1);
			stackPos1++;
			}
		else if (type1 == "op1") {
			var op1 = code1[1];
			console.log("OP1 "+op1+"\n");
			stackPos1--;
			var right1 = stackList1.pop();
			console.log("\ttemp"+stackPos1+" == "+op1+" "+right1+";\n");
			stackList1.push("temp" + stackPos1)
			stackPos1++;
			}
		else if (type1 == "op2") {
			var op2 = code1[1];
			console.log("OP2 "+op2+"\n");
			var right1 = stackList1.pop();
			var left1 = stackList1.pop();
			stackPos1--;
			stackPos1--;
			console.log("\ttemp"+stackPos1+" == "+left1+" "+op2+" "+right1+";\n");
			stackList1.push("temp" + stackPos1)
			stackPos1++;
			}
		}
	stackPos1--;
	console.log("RESULT\n");
	console.log("\tresult == temp"+stackPos1+";\n");
	}

execute(codeList1);

Here is the output of the JavaScript code.

VAR x 

VAR y 

OP2 and

	temp0 == x and y;

VAR x 

OP1 not

	temp1 == not x;

VAR y 

OP1 not

	temp2 == not y;

OP2 and

	temp1 == temp1 and temp2;

OP2 or

	temp0 == temp0 or temp1;

RESULT

	result == temp0;

Instead of an explicit stack, the code can be generated to use the original variables or to use (and reuse) temporary variables.

This results in more compact code that runs faster.

There is still room for improvement, but the example shows how abstract interpretation of the generated postfix code can be used to create more compact and faster running code.

We will return to abstract interpretation when we get to Alan Turing and the Halting Problem and what is and what is not computable.

11. Acronyms and/or initialisms for this page

1