package herdtools7

This module produces an map like interface to model memory storage.

Introduction to scopes, mutability and blocks

The usual implementation and semantics of variables is based on "maps", i.e. functions from variables to values with a finite domain. We note env such a map.

As in ASL, to evaluate a program, we distinguish between expressions and statements:

1. function eval_expr takes as argument an environment and an expression and returns a value. For instance, here is the evaluation of a variable:

   eval_expr env = function
     | E_Var x -> Map.find x env

2. function eval_stmt takes as argument an environment and a statement and returns an environment. For instance here is the execution of a variable declaration:

   eval_stmt env = function
     | S_Decl (x, e) ->
       let v = eval_expr x e in
       Map.add x v env

In a simplified setting, the above scheme suffices to implement mutable variables, mostly because the eval_stmt returns the environment, as illustrated by the rule for assignment, which is the same as the declaration rule.

eval_stmt env = function
  | S_Assign (x, e) ->
    let v = eval_expr env e in
    Map.add x v env

Notice that the new binding overwrites the old one, which is no longer accessible.

The scheme still works in case all variables are global and when expression can perform side effects. Function eval_expr will now return a pair of a value and of an environment, For instance, assume expression E_Incr x that increments the contents of x and return the new value:

eval_expr env = function
  | E_Incr x ->
    let v = Map.find x env in
    let v = v + 1 in
    (v, Map.add x v env)

Things get more complicated in the presence of scopes. The root reason is what happens to bindings at scope end. Consider the following ASL code:

 var s = 0;
 var i = 0;
 while i < n do
   var c = i*i ;
   s = s + c;
   i = i + 1;
 end
 // 'c' is mo longer available, 's' is.

According to ASL semantics the variable c exists from its declaration to the end of its enclosing block. One simple implementation for executing a block is as follows:

let eval_stmt env = function
  | S_Block stmt ->
    ignore (eval_stmt env stmt);
    env

All extensions performed by the statement stmt from inside the block are discarded.

However, some variable defined before the block can be assigned inside the block (this is the case of s above), and those modifications have to survive the end of the block... This would lead to the following contradictory implementation:

let eval_stmt env = function
  | S_Block stmt -> eval_stmt env stmt

One solution is adding an indirection in environments. En environment is now made of two maps: one for bindings from variables to pointers and another for the "heap" from pointers to values.

type env = { bds : pointer VarMap.t; heap : value PointerMap.t; }

The rule for blocks can now discard the bindings and retain the heap:

let eval_stmt old_env = function
  | S_Block stmt ->
    let new_env =  eval_stmt env stmt in
    { bds = old_env.bds; heap = new_env.heap; }

One may notice that the heap can be purged of the slots associated to the discarded bindings, some kind of garbage collection. This can be done easily by an additional field in environment 'declared' that records the variables declared in a block - this technique is used in the interpreter.

The rule for evaluating a variable now performs two successive searches, one for retrieving the pointer and then the value:

let eval_expr env = function
  | E_Var x ->
    let pointer = VarMap.find x env.bds in
    PointerMap.find pointer env.heap

The rules for declarations and assignments also change, there are now different:

1. The declaration allocates a fresh pointer. That way if a binding for the same variable exists the underlying heap slot is preserved.
2. The assignment retrieve the pointer associated to the variable, which must exist.

Storage module

This module implements the storage type presented above, and present a simple interface to this.