Lab 8: Hoare logic

Overview

In the class, we've discussed the Hoare logic, an axiomatic semantics for formal reasoning about program correctness. One important application of Hoare logic is in the field of program verification, where the desired properties of the programs can be reasoned formally and rigorously. To be specific, there are two different styles to reason about the program: the backward style, which scans the program in a reverse order and is suitable for the structured programs; and the forward style, which scans the program from the beginning to the end, and is suitable for either the structured or unstructured programs.

In this assignment, you'll implement a Hoare logic system by completing both a backward and a forward verification systems. To be specific, this assignment is divided into two parts, each of which contains both some tutorials and problems. The first part covers a backward verification system, which operates on the aforementioned language C--; and the second part covers a forward verification system which operates on a low-level assembly-like intermediate language TAC, which is a modified version of the Three Address Code. Strictly speaking, these two systems are equivalent in their expressiveness, but having both of them will get you more familiarized with the different verification technologies on different flavors of languages. Some problems are tagged with Exercise, which you should solve. And several problems are tagged with Challenge, which are optional. Download code templates to start with.

Before starting with this assignment, make sure you've finished Software Setup in the lab 1, and have Z3 and Python(3.12+ recommended) properly installed on your computer. For any problems, please feel free to contact us for help.

Hand-in Procedure

When you finished the lab, zip you code files with file name <ID>-lab-8.zip (e.g., SA19225789-lab-8.zip), and submit it to USTC Online Teaching Platform. Any late submission will NOT be accepted.

Part A: Backward verification

The first verifier you'll be building is of backward style, and operates on the C-- language. Below is the syntax of C--, with some modifications from last assignment: we add the implication ->, and && , or ||, and negation ~: 

    bop ::= + | - | * | / | == | != | > | < | >= | <= | -> | && | ||
    E   ::= n | x | E bop E | ~E
    S   ::= skip
          | x=E
          | S;S
          | f(E1, ..., En)
          | if(E, S, S)
          | while I(E, S)
    F   ::= f(x1, ..., xn){S; return E;}

As with last assignment, we need to build a group of abstract syntax tree data structures to represent the C-- syntax. We have supplied you these data structures, which you should first get yourself familiarized of.

Exercise 1: Read the code in imp_ast.py, make sure you understand these data structures. Pay special attention to the loop invariant and modified variables in the StmWhile class, and the pre- and post-conditions in the Function class. Your job in this exercise is to write down the data structure for the function sum() as given in the comment. Make sure to test your implementation before continuing.
Exercise 2: Later in this assigment (and generally in any verification condition generation systems), we often need to estimate how large the generated verification condition (an expression) is, so we can write a function exp_num_nodes(), to count the number of nodes in a given expression. Complete that function in imp_ast.py, by filling in the missing code.

We've discussed the backward verification condition generation rules in the class, which are repeated below for your reference: 

    VC(skip, P)         = P
    VC(S1;S2, P)        = VC(S1, VC(S2, P))
    VC(x=e, P)          = P[x↦e]
    VC(if(e;s1;s2), P)  = (e → VC(s1, P))∧(~e → VC(s2, P))
    VC(while I(e;s), P) = I ∧ (∀x1 x2 ... xn.I →(e → VC(s, I) ∧ (~e → P)))

Pay special attention to the universal quantifier in the rule for the while statement: the variables x1, x2, ..., and xn are assigned in the while body. Basically, this rule requires the while statement is annotated with the modified variables in the loop body. This StmWhile class record this information in the modified_vars field.

Exercise 3: Calculate the modified variables in any while statement by filling in the function fill_in_modified_vars() module. You won't need to use a functional programming style, instead, you may record this information directly on the appropriate tree nodes.
Exercise 4: Read the code in backward.py file, in which the function vc() scans a function f backward, generates a verification condition for f and returns the verification condition. Your task is to fill in this function, based on the rules above. Think carefully how to do the variable substitution, and how to handle pre- and post-conditions. Make sure to test your implementation thoroughly, you can use the test cases in the ast module. How large the generated VCs are?

As usual, after generating the verification conditions, we continue to convert them to Z3 format, and send it to the Z3 solver to prove it. If Z3 proves the VC, the target program is verified, or else if Z3 reports some contradiction, the verification fails. The reason is either the program is wrong, or the supplied specification does not specify the programs correctly.

Exercise 5: Finish the function vc_2_z3() in the prover.py file, to prove or disprove the generated verification conditions. Don't forget to test your code. Hint: although there can be no decision procedures for first-order logic in general, z3 can solve a large set of formulas that use quantifiers, say: ForAll([x, y], f(x, y) == 0). You'll need this capability when processing the while statement.

As we discussed in the class, for target programs with many if statement, the generated verification conditions can grow exponentially, this is called verification condition explosion. This brings several challenges to the verification system implementation: first, the time spent in the generation tends to be longer; second, the generated verification condition tends to be larger; finally, the generated VC may be beyond the capability of modern solvers.

Exercise 6: To understand these challenges and to study how to mitigate them, we experiment some large target program in this exercise. In the file gen_prog.py, we provide you a generator, which can generate some test programs. You can run this command like this: 
    
        $ python3 gen_prog.py 10
to generate a test file, where 10 is number of statements you want to generate, you can change it to try other values. This command will generate a file large_prog.py which contains a test program. Run the generated program, and be sure to answer the following problems:
Challenge: In the implementation we supplied, there is no support for function calls and returns. Try to modify the code to support them. Think carefully the verification generation rules for function call/returns. Feel free to change any code you think necessary.

Part B: Forward verification

In this part of the assignment, we'll build a forward verification generator, which scans the program from the beginning to the end. The generator you'll build work on an unstructured language: TAC, which is an abbreviation of Three Address Code, though the version we'll be using is a variant of the standard one. The key difference is that the expression we'll be using are compound, instead of atomic. Though the TAC language here is not suitable for program analysis and optimization, it's enough for our verification purpose in this assignment.

The intermediate language we'll be using is given by the following syntax: 

    bop ::= + | - | * | / | == | != | > | < | >= | <= | -> | && | ||
    E ::= n | x | E bop E | ~E
    S ::= skip             // empty
        | x=E              // assignment
        | L:               // label
        | inv E            // an invariant E
        | f(E1, …, En)     // function call
        | if(E, L1, L2)    // branching
        | goto L           // jump
        | return E         // function return
    F ::= f(x1, …, xn){S*}

Control flows are not structured any more, but only explicit labels and jumps.

Exercise 7: Read the code in tac.py, make sure you understand these data structures for TAC. Notice that we both have the symbolic (label) address and physical address for the code sequence. Take the StmIf statement as an example, the fields true_label, false_label are symbolic address, whereas the fields true_address, false_address are physical address. When implementing the symbolic executor, the physical address is more convenient, as it allows direct jump.

In principal, we can also write down the TAC programs manually, making use of the data structures, as we've done for the C-- programs. However, doing so will be painfully and tedious, due to the low-level nature of the TAC language. Luckily, there is a more convenient and easier way: to compile the C-- programs directly down to equivalent TAC program. We have supplied the code for the compiler to you.

Exercise 8: Skim the compiler code in compiler.py file. You are NOT required to understand this code. But you are encouraged to do so, if you're curious.
Exercise 9: Read the code in forward.py file, which contains code performing forward verification condition generation. Your task in this exercise is to finish this generator by filling missing code in the function vc(). You'll be using the symbolic execution idea from previous assignment.

As in the backward generator, we can send the generated VC to a prover/solver to prove it, as described by the following process: 

    programs ---> verification         ---> verification ---> solver ---> prove/disprove
                  condition generator       condition
Challenge: As for the C-- language, add verification condition generation support for function call/return; so that your generator can deal with large programs.
Challenge: One key advantage of generating verification conditions at a relatively low-level is that one can generate Proof-carrying code, in which a explicit formal proof about the VC is generated and attached to the low-level code. Thus, the receiver of the low-level code can re-generate the VC and checks the VC against the proof, to guarantee the safety of the code. One such example in common use is the Java bytecode: the Java compiler will generate necessary type information (among other information) and attach these information to the binary class files. Before a client runs the class file, it will scan these type information and check the type safety of the class file. Z3 has builtin support for proof generation, for this purpose, you can configure Z3 like this: 
        from z3 import *

        ctx = Context(proof=True)
        solver = Solver(ctx=ctx)
        x = Bool('x', ctx=ctx)
        solver.add(Not(Implies(x, x)))
        res = solver.check()
        print(res)
        proof = solver.proof()
        print(proof)

This completes this assignment. Remember to zip you homework with file name <ID>-lab-8.zip (e.g., SA19225789-lab-8.zip), and submit it to USTC Online Teaching Platform.

Happy hacking!