Skip to content
This repository has been archived by the owner on Feb 1, 2020. It is now read-only.

Program Verification

Jump to bottom
Daejun Park edited this page Aug 26, 2016 · 4 revisions

0. Getting Started Guide

VM image:

NOTE:

  • Since the VM image contains a 64-bit guest OS (Ubuntu 14.04), it may not work if your system does not support a proper virtualization. For example, you may not able to run it in VirtualBox if the CPU does not support hardware virtualization such as AMD-V or VT-x.

  • The VM guest requires minimum of 6GB memory.

  • The VM image was created and tested by VirtualBox 4.3.22 on Ubuntu 12.04.

QUICK CHECK

To quickly test if you correctly setup VM, run the following commands: (We will explain what this command means later.)

$ cd ~/oopsla16/kernelc
$ krun tests/binary_search_tree/insert.c \
  --prove tests/binary_search_tree/insert_spec.k \
  --smt_prelude ../k/include/z3/search_tree.smt2 \
  --z3-executable

You will get the following output: (Note that time will vary by machines.)

## TIME TOTAL 5265
## TIME IMPLIES 198
## TIME APPLY_RULES 2727
## TIME REWRITE_STEPS 2182
## STEP TOTAL 150
## STEP TERMS 336
## STEP PEAK_TERMS 4
## STEP AVERAGE_TERMS 2.24
## RULE TOTAL 1040
## RULE STEP_TOTAL 363
## RULE PEAK 60
## RULE AVERAGE 2.8650137741046833
## TIME Z3_TOTAL 4306
## TIME Z3_IMPLIES 99
## TIME Z3_APPLY_RULES 2522
## TIME Z3_REWRITE_STEPS 1620
## CNT Z3_TOTAL 160
## CNT Z3_IMPLIES 3
## CNT Z3_APPLY_RULES 82
## CNT Z3_REWRITE_STEPS 72
true

1. Step by Step Instructions

To simply reproduce all the results shown in Table 1, run:

$ cd ~/oopsla16
$ ./run-all.sh

The expected output is available at:

~/oopsla16/run-all.sh.out

NOTE: Running all of the experiments will take several hours in VM. For example, the above command took ~3 hours in the given VirtualBox VM on the top of a machine with Intel Xeon CPU 3.40GHz and DDR3 RAM 8GB 1600MHz. We recommend to install our verification framework in a native machine to enjoy the full benefit.

Let's break down the above command.

The script ~/oopsla16/run-all.sh essentially runs the following four sub-scripts, one for each language:

~/oopsla16/kernelc/run.sh                                // KernelC
~/oopsla16/c-semantics/verification/run.sh               // C
~/oopsla16/java-semantics/src/run.sh                     // Java
~/oopsla16/javascript-semantics/verification/Makefile    // JavaScript

and each script simply runs our verifier for each programs shown in Table 1.

Let's look at one of them in kernelc/run.sh, the one shown in the beginning:

$ krun tests/binary_search_tree/insert.c \
  --prove tests/binary_search_tree/insert_spec.k \
  --smt_prelude ../k/include/z3/search_tree.smt2 \
  --z3-executable

Essentially it says: verify the program insert.c (as shown in Figure 2) against the specification insert_spec.k (as shown in Figure 3).

The last two options are related to Z3 SMT solver integration (Section 5.3). --smt_prelude specifies the prelude file to generate Z3 query. --z3-executable says that Z3 should be invoked as an external process rather than a library call, which is much safer but slower way to invoke Z3 from Java in which our verifier is written.

Each run of the verifier outputs statistics as shown in the beginning. The numbers in Table 1 was obtained by using such statistics output. For each language, we have four types of numbers, calculated as follows:

Execution Time   = ( 'TIME APPLY_RULES' + 'TIME REWRITE_STEPS'
                   - 'TIME Z3_APPLY_RULES' - 'TIME Z3_REWRITE_STEPS') / 1000
Execution #Step  = 'STEP TERMS'
Reasoning Time   = ( 'TIME IMPLIES' 
                   + 'TIME Z3_APPLY_RULES' + 'TIME Z3_REWRITE_STEPS') / 1000
Reasoning #Query = 'CNT Z3_TOTAL'

where:

TIME APPLY_RULES    the time taken by (line 6 of the algorithm in Section 5)
TIME REWRITE_STEPS  the time taken by (line 9)
TIME IMPLIES        the time taken by (line 5)

STEP TERMS          the total   number of successors at (line 9)
STEP PEAK_TERMS     the peak    number of successors at (line 9)
STEP AVERAGE_TERMS  the average number of successors at (line 9)

Note that you will get higher number for time than ones in Table 1, since you are running it in VM.

DIRECTORY STRUCTURE

Verification framework (in binary):
    ~/oopsla16/k

Scripts running experiments (Table 1):
    ~/oopsla16/kernelc/run.sh
    ~/oopsla16/c-semantics/verification/run.sh
    ~/oopsla16/java-semantics/src/run.sh
    ~/oopsla16/javascript-semantics/verification/Makefile

Programs to be verified (Figure 2):
    ~/oopsla16/kernelc/test/*/*.c
    ~/oopsla16/c-semantics/verification/*.c
    ~/oopsla16/java-semantics/src/verification/*.java
    ~/oopsla16/javascript-semantics/verification/*/*.js

Specifications (Figure 3):
    ~/oopsla16/kernelc/test/*/*_spec.k
    ~/oopsla16/c-semantics/verification/*_spec.k
    ~/oopsla16/java-semantics/src/verification/*-spec.k
    ~/oopsla16/javascript-semantics/verification/*/*_spec.k

Abstractions and auxiliary functions used in specifications (Table 2):
    ~/oopsla16/kernelc/patterns/*_pattern.k
    ~/oopsla16/c-semantics/verification/*_pattern.k
    ~/oopsla16/java-semantics/src/verification/*_pattern.k
    ~/oopsla16/javascript-semantics/verification/patterns/*/*_pattern.k

Domain reasoning (Section 5.3):
    ~/oopsla16/k/include/z3/*.smt2
    ~/oopsla16/kernelc/patterns/*_{set,list}.k
    ~/oopsla16/c-semantics/verification/*_{set,list}.k
    ~/oopsla16/java-semantics/src/verification/*_{set,list}.k
    ~/oopsla16/javascript-semantics/verification/patterns/*/*.smt2
    ~/oopsla16/javascript-semantics/verification/patterns/*/*_{set,list}.k

Note that we also include each language semantics here in order to instantiate our verification framework, but those semantics are not our contribution, thus not subject to the artifact evaluation.

RUNNING VERIFIER

To verify programs, use the following command:

$ krun -d <semantics> --prove <specification> <program>

where:

<program>        the program to be verified
<specification>  the specification to be checked against <program>
<semantics>      the semantics of the language in which <program> is written

You may also need additional options regarding Z3 integration:

--smt_prelude <smt-prelude>
--z3-executable

and language semantics-specific options as well.

Refer to the full list of commands for each languages and programs at:

~/oopsla16/kernelc/run.sh                                // KernelC
~/oopsla16/c-semantics/verification/run.sh               // C
~/oopsla16/java-semantics/src/run.sh                     // Java
~/oopsla16/javascript-semantics/verification/Makefile    // JavaScript

When it succeeds in verifying the program, it will output true in the end.

Note that the verifier may crash or fail to terminate when the program is not correct. We will improve usability of the verifier in the future.

Clone this wiki locally