Responses of HAHA

Error markers

HAHA reports errors by displaying error markers in the editor. Each marker has a tooltip which describes the reason why it was created. This information is also available in the console view (located in a tab in the bottom part of the window). This chapter describes various kinds of error markers produced by HAHA.

Syntax errors

Markers for syntax errors are created as the program is typed. No user action is necessary to trigger syntax checking. HAHA syntax is described in detail in section Language reference.

Type errors

Error markers related to typechecking are created and updated only when the source file is saved.

VCGen errors

Error markers are also produced whenever the solver is unable to prove validity of a formula generated from the program. These markers are updated whenever the verification conditions generator is run. Marker description contains context information, which describes why the formula was generated. Example of such information can be seen below:

Verification condition is not valid
  Program correctness
    Correctness of bsearch
      Block at lines 12 - 37
        Loop statement at line 17
          Single iteration preserves invariants.
            Block at lines 21 - 34
              If statement at line 24
                Case 1 - condition holds.
                  Postconditions are valid.
                    still_ordered at line 19

This description tells us that the solver was unable to prove that a loop invariant named still_ordered holds if the first branch of a conditional statement in line 24 is taken.

Verification conditions generator produces error markers in two cases

  • When the solver was able to prove the invalidity of a formula. In this case a counterexample is produced and appended to error description. A counterexample is simply an assignment of values to free varialbes occuring in an expression. For example, an attempt to validate the following program

    function test(x : Z) : Z
  postcondition test >= x
    test := 3 * x

    would result in this error:

    Verification condition is not valid
Program correctness
  Correctness of test
    Postcondition at line 2 (after substitution)

Counterexample:
  x = (- 1)

  • When the solver could neither prove nor disprove the formula. This case also covers problems caused by timeouts, internal solver errors and bugs in HAHA.

In case the program under consideration contains arrays, the counterexamples contain information about arrays. A statement of the form:

A = (_ as-array k!17),

means that the local variable A that holds an array is represented in the further lines of the counterexample as a function under the variable k!17. There is no special meaning hidden neither in the name k nor in the number 17. These are random values from the point of view of the verification process.

Subsequently, statements that describe the variable k!17 follow. Typically, we can observe here a formula like this:

k!17 = 0,

and this means that all the cells of the array are equal to 0. Another typical statement is:

k!17(x!1) = (ite (= x!1 0) 7 1)

This statement means that the array k!17 is actually a function that assumes 7 when applied to 0 and assumes 1 in any other situation. Similarly:

k!17(x!1) = (ite (>= x!1 0) 5 2)

states that the function assumes 5 for all non-negative arguments and 2 for negative ones (yes, as the arrays are indexed with Z, the indices can be negative numbers). Of course, the ite expressions can be combined as in:

k!17(x!1) = (ite (>= x!1 0) (ite (>= x!1 2) 5 3) 2)

which represents the array that has 2 on negative indices, 3 on indices 0, 1, and 5 on positive indices starting with 2. It should not come as surprise that the assertion:

k!17(x!1) = (k!17!19 (k!18 x!1))

says that k!17 is a composition of the arrays k!18 and k!17!19 understood as a composition of functions.

Console output

When the verification condition generator is run, a console is displayed in the lower pane. This console logs all messages printed during the process of creating and discharging verification conditions. Messages in the console are more detailed (but somewhat harder to read) than error marker descriptions.

First, all computed verification conditions are printed. Each condition consists of a list of assumptions, followed by a goal. Goal is separated from assumptions by a horizontal line. Note that all expressions are displayed in prefix notation. The following example shows a single verification condition:

n_ge_one : (>= len 1)
orderedA : (CALL-PREDICATE ordered A 1 len)
is_inA : (CALL-PREDICATE is_in A v 1 len)
---------------------------------------------
(AND (= 1 1) (AND (>= len 1) (AND (CALL-PREDICATE ordered A 1 len) (CALL-PREDICATE is_in A v 1 len))))

Declared variables, axioms and predicates are also printed at this stage.

In the second stage, computed conditions are discharged by the solver. During this stage, commands sent to the solver are printed. Possible commands include

  • Declaration of a variable or predicate (DECLARE VAR)
  • New assumption (DECLARE AXIOM)
  • Context management commands MARK and RESET. The latter removes all declarations (both variables and assumptions) since last unmatched occurence of the former.
  • Validity check IS_VALID. This command checks if the goal formula is valid in the current context. After this command, solver response (including a counterexample, if applicable) is printed to the console.

Text lines preceded by >> represent raw text sent to the external SMT solver. Similarly, lines starting with << contain raw solver responses. This is mainly useful for finding bugs related to translation of solver commands to the SMT2 format.