In the previous several posts, I’ve formalized the notion of lattices, which are an essential ingredient to formalizing the analyses in Anders Møller’s lecture notes. However, there can be no program analysis without a program to analyze! In this post, I will define the (very simple) language that we will be analyzing. An essential aspect of the language is its semantics, which simply speaking explains what each feature of the language does. At the end of the previous article, I gave the following inference rule which defined (partially) how the if-else statement in the language works.

ρ1,ez¬(z=0)ρ1,s1ρ2ρ1,if e then s1 else s2  ρ2 \frac{\rho_1, e \Downarrow z \quad \neg (z = 0) \quad \rho_1,s_1 \Downarrow \rho_2} {\rho_1, \textbf{if}\ e\ \textbf{then}\ s_1\ \textbf{else}\ s_2\ \Downarrow\ \rho_2}

Like I mentioned then, this rule reads as follows:

If the condition of an if-else statement evaluates to a nonzero value, then to evaluate the statement, you evaluate its then branch.

Another similar — but crucially, not equivlalent – rule is the following:

ρ1,ezz=1ρ1,s1ρ2ρ1,if e then s1 else s2  ρ2 \frac{\rho_1, e \Downarrow z \quad z = 1 \quad \rho_1,s_1 \Downarrow \rho_2} {\rho_1, \textbf{if}\ e\ \textbf{then}\ s_1\ \textbf{else}\ s_2\ \Downarrow\ \rho_2}

This time, the English interpretation of the rule is as follows:

If the condition of an if-else statement evaluates to one, then to evaluate the statement, you evaluate its then branch.

These rules are certainly not equivalent. For instance, the former allows the “then” branch to be executed when the condition is 2; however, in the latter, the value of the conditional must be 1. If our analysis were intelligent (our first few will not be), then this difference would change its output when determining the signs of the following program:

x = 2
if x {
  y = - 1
} else {
  y = 1
}

Using the first, more “relaxed” rule, the condition would be considered “true”, and the sign of y would be -. On the other hand, using the second, “stricter” rule, the sign of y would be +. I stress that in this case, I am showing a flow-sensitive analysis (one that can understand control flow and make more specific predictions); for our simplest analyses, we will not be aiming for flow-sensitivity. There is plenty of work to do even then.

The point of showing these two distinct rules is that we need to be very precise about how the language will behave, because our analyses depend on that behavior.

Let’s not get ahead of ourselves, though. I’ve motivated the need for semantics, but there is much groundwork to be laid before we delve into the precise rules of our language. After all, to define the language’s semantics, we need to have a language.

The Syntax of Our Simple Language

I’ve shown a couple of examples our our language now, and there won’t be that much more to it. We can start with expressions: things that evaluate to something. Some examples of expressions are 1, x, and 2-(x+y). For our specific language, the precise set of possible expressions can be given by the following Context-Free Grammar:

e::=x(variables)z(integer literals)e+e(addition)ee(subtraction) \begin{array}{rcll} e & ::= & x & \text{(variables)} \\ & | & z & \text{(integer literals)} \\ & | & e + e & \text{(addition)} \\ & | & e - e & \text{(subtraction)} \end{array}

The above can be read as follows:

An expression ee is one of the following things:

  1. Some variable xx [importantly xx is a placeholder for any variable, which could be x or y in our program code; specifically, xx is a metavariable.]
  2. Some integer zz [once again, zz can be any integer, like 1, -42, etc.].
  3. The addition of two other expressions [which could themselves be additions etc.].
  4. The subtraction of two other expressions [which could also themselves be additions, subtractions, etc.].

Since expressions can be nested within other expressions — which is necessary to allow complicated code like 2-(x+y) above — they form a tree. Each node is one of the elements of the grammar above (variable, addition, etc.). If a node contains sub-expressions (like addition and subtraction do), then these sub-expressions form sub-trees of the given node. This data structure is called an Abstract Syntax Tree.

Notably, though 2-(x+y) has parentheses, our grammar above does not include include them as a case. The reason for this is that the structure of an abstract syntax tree is sufficient to encode the order in which the operations should be evaluated. Since I lack a nice way of drawing ASTs, I will use an ASCII drawing to show an example.

Expression: 2 - (x+y)
    (-)
   /   \
  2    (+)
      /   \
     x     y


Expression: (2-x) + y
       (+)
      /   \
    (-)    y
   /   \
  2     x

Above, in the first AST, (+) is a child of the (-) node, which means that it’s a sub-expression. As a result, that subexpression is evaluated first, before evaluating (-), and so, the AST expresents 2-(x+y). In the other example, (-) is a child of (+), and is therefore evaluated first. The resulting association encoded by that AST is (2-x)+y.

To an Agda programmer, the one-of-four-things definition above should read quite similarly to the definition of an algebraic data type. Indeed, this is how we can encode the abstract syntax tree of expressions:

From Base.agda, lines 12 through 16
12
13
14
15
16
data Expr : Set where
    _+_ : Expr  Expr  Expr
    _-_ : Expr  Expr  Expr
    `_ : String  Expr
    #_ :   Expr

The only departure from the grammar above is that I had to invent constructors for the variable and integer cases, since Agda doesn’t support implicit coercions. This adds a little bit of extra overhead, requiring, for example, that we write numbers as # 42 instead of 42.

Having defined expressions, the next thing on the menu is statements. Unlike expressions, which just produce values, statements “do something”; an example of a statement might be the following Python line:

print("Hello, world!")

The print function doesn’t produce any value, but it does perform an action; it prints its argument to the console!

For the formalization, it turns out to be convenient to separate “simple” statements from “complex” ones. Pragmatically speaking, the difference is that between the “simple” and the “complex” is control flow; simple statements will be guaranteed to always execute without any decisions or jumps. The reason for this will become clearer in subsequent posts; I will foreshadow a bit by saying that consecutive simple statements can be placed into a single basic block.

The following is a group of three simple statements:

x = 1
y = x + 2
noop

These will always be executed in the same order, exactly once. Here, noop is a convenient type of statement that simply does nothing.

On the other hand, the following statement is not simple:

while x {
  x = x - 1
}

It’s not simple because it makes decisions about how the code should be executed; if x is nonzero, it will try executing the statement in the body of the loop (x = x - 1). Otherwise, it would skip evaluating that statement, and carry on with subsequent code.

I first define simple statements using the BasicStmt type:

From Base.agda, lines 18 through 20
18
19
20
data BasicStmt : Set where
    _←_ : String  Expr  BasicStmt
    noop : BasicStmt

Complex statements are just called Stmt; they include loops, conditionals and sequences — [note: The standard notation for sequencing in imperative languages is s1;s2s_1; s_2. However, Agda gives special meaning to the semicolon, and I couldn't find any passable symbolic alternatives. ] is a sequence where s2s_2 is evaluated after s1s_1. Complex statements subsume simple statements, which I model using the constructor ⟨_⟩.

From Base.agda, lines 25 through 29
25
26
27
28
29
data Stmt : Set where
    ⟨_⟩ : BasicStmt  Stmt
    _then_ : Stmt  Stmt  Stmt
    if_then_else_ : Expr  Stmt  Stmt  Stmt
    while_repeat_ : Expr  Stmt  Stmt

For an example of using this encoding, take the following simple program:

var = 1
if var {
  x = 1
}

The Agda version is:

From Main.agda, lines 27 through 34
27
28
29
30
31
32
33
34
testCodeCond₂ : Stmt
testCodeCond₂ =
     "var"  (# 1)  then
    if (` "var") then (
         "x"  (# 1) 
    ) else (
         noop 
    )

Notice how we used noop to express the fact that the else branch of the conditional does nothing.

The Semantics of Our Language

We now have all the language constructs that I’ll be showing off — because those are all the concepts that I’ve formalized. What’s left is to define how they behave. We will do this using a logical tool called inference rules. I’ve written about them a number of times; they’re ubiquitous, particularly in the sorts of things I like explore on this site. The section on inference rules from my Advent of Code series is pretty relevant, and the notation section from a post in my compiler series says much the same thing; I won’t be re-describing them here.

There are three pieces which demand semantics: expressions, simple statements, and non-simple statements. The semantics of each of the three requires the semantics of the items that precede it. We will therefore start with expressions.

Expressions

The trickiest thing about expression is that the value of an expression depends on the “context”: x+1 can evaluate to 43 if x is 42, or it can evaluate to 0 if x is -1. To evaluate an expression, we will therefore need to assign values to all of the variables in that expression. A mapping that assigns values to variables is typically called an environment. We will write \varnothing for “empty environment”, and {x42,y1}\{\texttt{x} \mapsto 42, \texttt{y} \mapsto -1 \} for an environment that maps the variable x\texttt{x} to 42, and the variable y\texttt{y} to -1.

Now, a bit of notation. We will use the letter ρ\rho to represent environments (and if several environments are involved, we will occasionally number them as ρ1\rho_1, ρ2\rho_2, etc.) We will use the letter ee to stand for expressions, and the letter vv to stand for values. Finally, we’ll write ρ,ev\rho, e \Downarrow v to say that “in an environment ρ\rho, expression ee evaluates to value vv”. Our two previous examples of evaluating x+1 can thus be written as follows:

{x42},x+143{x1},x+10 \{ \texttt{x} \mapsto 42 \}, \texttt{x}+1 \Downarrow 43 \\ \{ \texttt{x} \mapsto -1 \}, \texttt{x}+1 \Downarrow 0 \\

Now, on to the actual rules for how to evaluate expressions. Most simply, integer literals like 1 just evaluate to themselves.

nIntρ,nn \frac{n \in \text{Int}}{\rho, n \Downarrow n}

Note that the letter ρ\rho is completely unused in the above rule. That’s because no matter what values variables have, a number still evaluates to the same value. As we’ve already established, the same is not true for a variable like x\texttt{x}. To evaluate such a variable, we need to retrieve the value it’s mapped to in the current environment, which we will write as ρ(x)\rho(\texttt{x}). This gives the following inference rule:

ρ(x)=vρ,xv \frac{\rho(x) = v}{\rho, x \Downarrow v}

All that’s left is to define addition and subtraction. For an expression in the form e1+e2e_1+e_2, we first need to evaluate the two subexpressions e1e_1 and e2e_2, and then add the two resulting numbers. As a result, the addition rule includes two additional premises, one for evaluating each summand.

ρ,e1v1ρ,e2v2v1+v2=vρ,e1+e2v \frac {\rho, e_1 \Downarrow v_1 \quad \rho, e_2 \Downarrow v_2 \quad v_1 + v_2 = v} {\rho, e_1+e_2 \Downarrow v}

The subtraction rule is similar. Below, I’ve configured an instance of Bergamot to interpret these exact rules. Try typing various expressions like 1, 1+1, etc. into the input box below to see them evaluate. If you click the “Full Proof Tree” button, you can also view the exact rules that were used in computing a particular value. The variables x, y, and z are pre-defined for your convenience.

The Agda equivalent of this looks very similar to the rules themselves. I use ⇒ᵉ instead of \Downarrow, and there’s a little bit of tedium with wrapping integers into a new Value type. I also used a (partial) relation (x, v) ∈ ρ instead of explicitly defining accessing an environment, since it is conceivable for a user to attempt accessing a variable that has not been assigned to. Aside from these notational changes, the structure of each of the constructors of the evaluation data type matches the inference rules I showed above.

From Semantics.agda, lines 27 through 35
27
28
29
30
31
32
33
34
35
data _,_⇒ᵉ_ : Env  Expr  Value  Set where
    ⇒ᵉ-ℕ :  (ρ : Env) (n : )  ρ , (# n) ⇒ᵉ (↑ᶻ (+ n))
    ⇒ᵉ-Var :  (ρ : Env) (x : String) (v : Value)  (x , v)  ρ  ρ , (` x) ⇒ᵉ v
    ⇒ᵉ-+ :  (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ) 
           ρ , e₁ ⇒ᵉ (↑ᶻ z₁)  ρ , e₂ ⇒ᵉ (↑ᶻ z₂) 
           ρ , (e₁ + e₂) ⇒ᵉ (↑ᶻ (z₁ +ᶻ z₂))
    ⇒ᵉ-- :  (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ) 
           ρ , e₁ ⇒ᵉ (↑ᶻ z₁)  ρ , e₂ ⇒ᵉ (↑ᶻ z₂) 
           ρ , (e₁ - e₂) ⇒ᵉ (↑ᶻ (z₁ -ᶻ z₂))

Simple Statements

The main difference between formalizing (simple and “normal”) statements is that they modify the environment. If x has one value, writing x = x + 1 will certainly change that value. On the other hand, statements don’t produce values. So, we will be writing claims like ρ1,bsρ2\rho_1 , \textit{bs} \Rightarrow \rho_2 to say that the basic statement bs\textit{bs}, when starting in environment ρ1\rho_1, will produce environment ρ2\rho_2. Here’s an example:

{x42,y17}, x = x - 1{x41,y17} \{ \texttt{x} \mapsto 42, \texttt{y} \mapsto 17 \}, \ \texttt{x = x - \text{1}} \Rightarrow \{ \texttt{x} \mapsto 41, \texttt{y} \mapsto 17 \}

Here, we subtracted one from a variable with value 42, leaving it with a new value of 41.

There are two basic statements, and one of them quite literally does nothing. The inference rule for noop is very simple:

ρ, noopρ \rho,\ \texttt{noop} \Rightarrow \rho

For the assignment rule, we need to know how to evaluate the expression on the right side of the equal sign. This is why we needed to define the semantics of expressions first. Given those, the evaluation rule for assignment is as follows, with ρ[xv]\rho[x \mapsto v] meaning “the environment ρ\rho but mapping the variable xx to value vv”.

ρ,evρ,x=eρ[xv] \frac {\rho, e \Downarrow v} {\rho, x = e \Rightarrow \rho[x \mapsto v]}

Those are actually all the rules we need, and below, I am once again configuring a Bergamot instance, this time with simple statements. Try out noop or some sort of variable assignment, like x = x + 1.

The Agda implementation is once again just a data type with constructors-for-rules. This time they also look quite similar to the rules I’ve shown up until now, though I continue to explicitly quantify over variables like ρ.

From Semantics.agda, lines 37 through 40
37
38
39
40
data _,_⇒ᵇ_ : Env  BasicStmt  Env  Set where
    ⇒ᵇ-noop :  (ρ : Env)  ρ , noop ⇒ᵇ ρ
    ⇒ᵇ-← :  (ρ : Env) (x : String) (e : Expr) (v : Value) 
           ρ , e ⇒ᵉ v  ρ , (x  e) ⇒ᵇ ((x , v) List.∷ ρ)

Statements

Let’s work on non-simple statements next. The easiest rule to define is probably sequencing. When we use then (or ;) to combine two statements, what we actually want is to execute the first statement, which may change variables, and then execute the second statement while keeping the changes from the first. This means there are three environments: ρ1\rho_1 for the initial state before either statement is executed, ρ2\rho_2 for the state between executing the first and second statement, and ρ3\rho_3 for the final state after both are done executing. This leads to the following rule:

ρ1,s1ρ2ρ2,s2ρ3ρ1,s1;s2ρ3 \frac { \rho_1, s_1 \Rightarrow \rho_2 \quad \rho_2, s_2 \Rightarrow \rho_3 } { \rho_1, s_1; s_2 \Rightarrow \rho_3 }

We will actually need two rules to evaluate the conditional statement: one for when the condition evaluates to “true”, and one for when the condition evaluates to “false”. Only, I never specified booleans as being part of the language, which means that we will need to come up what “false” and “true” are. I will take my cue from C++ and use zero as “false”, and any other number as “true”.

If the condition of an if-else statement is “true” (nonzero), then the effect of executing the if-else should be the same as executing the “then” part of the statement, while completely ignoring the “else” part.

ρ1,evv0ρ1,s1ρ2ρ1,if e {s1} else {s2} ρ2 \frac { \rho_1 , e \Downarrow v \quad v \neq 0 \quad \rho_1, s_1 \Rightarrow \rho_2} { \rho_1, \textbf{if}\ e\ \{ s_1 \}\ \textbf{else}\ \{ s_2 \}\ \Rightarrow \rho_2 }

Notice that in the above rule, we used the evaluation judgement ρ1,ev\rho_1, e \Downarrow v to evaluate the expression that serves as the condition. We then had an additional premise that requires the truthiness of the resulting value vv. The rule for evaluating a conditional with a “false” branch is very similar.

ρ1,evv=0ρ1,s2ρ2ρ1,if e {s1} else {s2} ρ2 \frac { \rho_1 , e \Downarrow v \quad v = 0 \quad \rho_1, s_2 \Rightarrow \rho_2} { \rho_1, \textbf{if}\ e\ \{ s_1 \}\ \textbf{else}\ \{ s_2 \}\ \Rightarrow \rho_2 }

Now that we have rules for conditional statements, it will be surprisingly easy to define the rules for while loops. A while loop will also have two rules, one for when its condition is truthy and one for when it’s falsey. However, unlike the “false” case, a while loop will do nothing, leaving the environment unchanged:

ρ1,evv=0ρ1,while e {s} ρ1 \frac { \rho_1 , e \Downarrow v \quad v = 0 } { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_1 }

The trickiest rule is for when the condition of a while loop is true. We evaluate the body once, starting in environment ρ1\rho_1 and finishing in ρ2\rho_2, but then we’re not done. In fact, we have to go back to the top, and check the condition again, starting over. As a result, we include another premise, that tells us that evaluating the loop starting at ρ2\rho_2, we eventually end in state ρ3\rho_3. This encodes the “rest of the iterations” in addition to the one we just performed. The environment ρ3\rho_3 is our final state, so that’s what we use in the rule’s conclusion.

ρ1,evv0ρ1,sρ2ρ2,while e {s} ρ3ρ1,while e {s} ρ3 \frac { \rho_1 , e \Downarrow v \quad v \neq 0 \quad \rho_1 , s \Rightarrow \rho_2 \quad \rho_2 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 } { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 }

And that’s it! We have now seen every rule that defines the little object language I’ve been using for my Agda work. Below is a Bergamot widget that implements these rules. Try the following program, which computes the xth power of two, and stores it in y:

x = 5; y = 1; while (x) { y = y + y; x = x - 1 }

As with all the other rules we’ve seen, the mathematical notation above can be directly translated into Agda:

From Semantics.agda, lines 47 through 64
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
data _,_⇒ˢ_ : Env  Stmt  Env  Set where
    ⇒ˢ-⟨⟩ :  (ρ₁ ρ₂ : Env) (bs : BasicStmt) 
            ρ₁ , bs ⇒ᵇ ρ₂  ρ₁ ,  bs  ⇒ˢ ρ₂
    ⇒ˢ-then :  (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) 
              ρ₁ , s₁ ⇒ˢ ρ₂  ρ₂ , s₂ ⇒ˢ ρ₃ 
              ρ₁ , (s₁ then s₂) ⇒ˢ ρ₃
    ⇒ˢ-if-true :  (ρ₁ ρ₂ : Env) (e : Expr) (z : ) (s₁ s₂ : Stmt) 
        ρ₁ , e ⇒ᵉ (↑ᶻ z)  ¬ z  (+ 0)  ρ₁ , s₁ ⇒ˢ ρ₂ 
        ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
    ⇒ˢ-if-false :  (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) 
        ρ₁ , e ⇒ᵉ (↑ᶻ (+ 0))  ρ₁ , s₂ ⇒ˢ ρ₂ 
        ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
    ⇒ˢ-while-true :  (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ) (s : Stmt) 
        ρ₁ , e ⇒ᵉ (↑ᶻ z)  ¬ z  (+ 0)  ρ₁ , s ⇒ˢ ρ₂  ρ₂ , (while e repeat s) ⇒ˢ ρ₃ 
        ρ₁ , (while e repeat s) ⇒ˢ ρ₃
    ⇒ˢ-while-false :  (ρ : Env) (e : Expr) (s : Stmt) 
        ρ , e ⇒ᵉ (↑ᶻ (+ 0)) 
        ρ , (while e repeat s) ⇒ˢ ρ

Semantics as Ground Truth

Prior to this post, we had been talking about using lattices and monotone functions for program analysis. The key problem with using this framework to define analyses is that there are many monotone functions that produce complete nonsese; their output is, at best, unrelated to the program they’re supposed to analyze. We don’t want to write such functions, since having incorrect information about the programs in question is unhelpful.

What does it mean for a function to produce correct information, though? In the context of sign analysis, it would mean that if we say a variable x is +, then evaluating the program will leave us in a state in which x is posive. The semantics we defined in this post give us the “evaluating the program piece”. They establish what the programs actually do, and we can use this ground truth when checking that our analyses are correct. In subsequent posts, I will prove the exact property I informally stated above: for the program analyses we define, things they “claim” about our program will match what actually happens when executing the program using our semantics.

A piece of the puzzle still remains: how are we going to use the monotone functions we’ve been talking so much about? We need to figure out what to feed to our analyses before we can prove their correctness.

I have an answer to that question: we will be using control flow graphs (CFGs). These are another program representation, one that’s more commonly found in compilers. I will show what they look like in the next post. I hope to see you there!