Uses symbolic execution and SMT solvers to accumulate knowledge about Slang program behaviors and to automatically show that programs conform to specifications included in the program. fooo bar bax

Intuition of Logika’s Verification Process

To effectively use Logika verification, it’s beneficial to understand how Logika accumulates knowledge about a program’s behavior, and how and when it leverages SMT solvers to make deductions. Compared to other program verifiers, Logika is very good about displaying this information in a developer-friendly manner. Before we describe the Logika display, we’ll first present some intuition about how symbolic execution-based program analysis works.

   :linenos:

   // #Sireum #Logika
   //   The special comments above recognized by the Sireum IVE
   //   indicate that this Scala script .sc file is a Slang script file
   //   that will be checked by Logika

   import org.sireum._ // imports Slang standard library

   val x = Z.random

   var y = x + 1
   y = y + 2

   assert (y > x)

Consider how we might accomulate knowledge about the code in the listing above as we build a mental model of the code’s execution (the before and after aspects correspond to the notions of pre-state and post-state which we will discuss in greater detail later).

• before the statement val x = Z.random we have no knowledge about code’s behavior or what variables it will use to compute; after the statement we know that the variable x will be involved in the computation. Based on our understanding of what the random function does, we don’t have any information about x’s value. Logika will actually introduce a marker which is presented to the developer using the label “random” that indicates that Logika doesn’t have any information about the specific value at that point – the value could be any member of the set of values associated with the type Z. We might represent this as follows::

   x == <a random value from Z>

• before the statement var y = x + 1 we have the same knowledge as the after case above; after the statement, we know that there is a new variable y. We don’t know the specific value that y holds, but based on the structure of the assignment statement, we know that it has some relationship to x. In particular, we know that y has a value that is one greater than whatever the value of x is. We might represent the information accumulated so far as follows::

   x == <a random value from Z>
   y == x + 1

• before the statement y = y + 2 we have the same knowledge as the after case above; after the statement, we know that there is a new version of y. We don’t know the specific value that the new version holds, but we know it’s related to the old version. In particular, the new version of y is two greater than the old version. And, we still know that the old version of y is one greater than whatever the value of x is. And, we still know that x has an random value from the type Z. This discussion indicates that to reason properly about a program, we need to distinguish between the value of the current version of a var and any previous versions. We will see below that Logika uses a notation based on line and column numbers to keep track of the older versions of a var. With this strategy, we might represent the information accumulated so far as follows::

   x == <a random value from Z>
   y<version defined at line 10, column 6> == x + 1
   y == y<version defined at line 10, column 6> + 2

When we come to the statement assert(y > x), we need to be concerned not just about accumulating knowledge about the computation, but about determining whether or not the assertion holds – we have a verification obligation. Intuitively, we consider the facts that we have about the current value of y and x (i.e., the constraints about the possible values of y and x at this point), and try to infer if the property y > x can hold based on those facts. That is, do the facts that we know about variables in the assertion (x and y) entail (imply) that the assertion expression y > x is true. This type of logical sentence / question is historically written in the following notation::

   x == <a random value from Z>,
   y<version defined at line 10, column 6> == x + 1,
   y == y<version defined at line 10, column 6> + 2,

    |-     

   y > x

where the |- is read “entails” or “implies”. The entire logical sentence above is historically referred to as a sequent. The logical statements to the left/above the |- are called the antecedent (technically, the antecedent is the conjunction of these statements, i.e., there is an implicit logical “and”/conjunction between each statement). The statement to the right/below the |- is called the consequent. A primary aspect of Logika’s automated reasoning involves using SMT solvers to determine whether or not such sequents hold. The sequent “holds” or “is true” or “is valid” if the consequent is true when all the statements in the antecedent are true.

Behind the scenes, Logika also keeps track of other knowledge about variables such as their types (which limits their possible values) as well as whether they are var’s or val’s. Knowing that a variable is a val can be useful because even when a bunch of complex computation happens in somewhere in the program, we know the values associated with val’s don’t change. Therefore, any knowledge that Logika had about the val’s before the computation is still valid after the computation.

Logika’s Display of Verification Information

Logika helps users understand how it is working by showing two types of markers that can be “drilled down into” for more information: (1) a “light bulb” marker indicates the knowledge that Logika knows about variables at a particular program point, and (2) a “lightning bolt” marker indicates that Logika is “summoning” the underlying SMT framework to prove a sequent, e.g., representing a verification obligation.

Logic Hints (a)

When the user clicks on the light bulb at line 11, Figure :ref:logic-hints-a illustrates that Logika opens a right-hand pane to display the knowledge that it has accumulated before the statement at line 11 is executed (review the bullets in the “reasoning process” above to see the correspondence between what we informally described and the knowledge that Logika has maintained in its automated deduction process). Note that Z.random@[8,11]#1 is Logika’s way of indicating a “unknown value picked from the type domain Z at line 8 column 11” **Robby: what is the “#1”?.

Logic Hints (b)

When the user clicks on the light bulb at line 13, Figure :ref:logic-hints-b, Logika indicates the knowledge it has accumulated before the assertion at line 13 is executed. We can see that Logika distinguishes the current value of y from the previous value using the marker y@10#6, i.e., the value of the version of y at line 10 column 6.

Logika Summonings (a)

Logika’s lightning bolt at line 13 indicates there is a verification obligation to prove that the assertion y > x holds and that it is “summoning” the SMT framework to attempt the proof. As shown in Figure :ref:summonings-a, clicking on the lightning bolt displays several types of information in right-hand pane. First, Logika shows a sequent representing the verification task associated with the selected lightning bolt. All such sequents have antecedents that contain knowledge that Logika has accumulated to that point, and a consequent corresponding to some boolean expression that needs to be proved true to support verification of a specification (explicit or implicit) or to determine the program path along which verification will continue. In this case, the consequent corresponds to the explicit assertion specification y > x. Typical Logika users will want to be able to read these sequents to understand if Logika’s accumulated knowledge and verification goal corresponds to their intuition. For example, looking at a sequent might reveal that Logika has not accumulated some fact that is necessary to prove the goal, and the user may need to introduce some additional assumptions or method pre-conditions, etc. to make the verification succeed.

Logika Summonings (b)

Scrolling down in the right-hand-side window shows the encoding of the sequent in terms of the standardized SMTLib input language for SMT solvers. The typical Logika user will not need to understand this information, but advanced users may find it useful for understanding Logika’s verification process. The encoding includes Logika’s SMTLib representation for Slang types and other information. At the bottom of the window, Figure :ref:summonings-b shows the encoding of the sequent antecedent clauses and consequent being sent to the SMT solver.

Fundamental Logika Verification Concepts

Symbolic Values ,,,,,,,,,,,,,,,

Symbolic Execution, like many other forms of program analysis and verification, tries to determine how a program will behave without actually performing a concrete execution of the program (e.g., running the program on concrete values).

Symbolic Execution Summarizes Many Concrete Executions ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,

Pre- and Post-States ,,,,,,,,,,,,,,,,,,,,

Schematic View of Symbolic Execution Steps ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,

Dealing with non-Termination ,,,,,,,,,,,,,,,,,,,,,,,,,,,,