Demo for HiFrog and UpProver

First, please download the demo examples of HiFrog and UpProver from here or by running the following command in your machine:

wget -q http://verify.inf.usi.ch/sites/default/files/executable/lab_hifrog_upprover.gz ; tar -xzvf lab_hifrog_upprover.gz

Part 1: HiFrog Demo:

` cd lab_hifrog_upprover/hifrogDemo` navigates to the directory that contains demo examples for HiFrog.

How to run HiFrog?

rm __summaries
hifrog [options] --logic <logic>  <file> --claim <N>

where <logic> could be qfuf, qflra, prop

Use of Function Summarization in verifying different assertions:

rm __summaries
hifrog --logic qflra ex1_lra.c --claim 1 --save-summaries __summaries 
hifrog --logic qflra ex1_lra.c --claim 3 --load-summaries __summaries 
hifrog  disk.c --show-claims

Exercise) In program disk.c, record the verification time for reasoning on –claim 79 (i) with using function summaries of claim 1 and (ii) without using function summaries of claim 1

Hints:

rm __summaries
hifrog --logic qflra  disk.c --claim 1 --save-summaries __summaries 
hifrog --logic qflra  disk.c --claim 79 --load-summaries __summaries 

For comparison, remove __summaries then run claim 79.

Use of Uninterpreted Functions (qfuf) vs. Propositional Logic (prop):

Use of Linear Real Arithmetic (qflra) vs. Uninterpreted Functions (qfuf):

Summary and Theory Refinement

First see how tedious might be to manually find an appropriate precision for each claim! Among qfuf (the cheapest), qflra, prop (the most expensive) encodings, let’s find the lightest possible (i.e., less expensive) encoding for verifying each claim of program sumtheoref2.c

By running manually for each claim:

rm __summaries
hifrog --logic <logic> sumtheoref2.c --claim <N> --save-summaries __summaries 

We trust the safe result (if the over-approximative theory is safe, more precise theories also will be safe), but we don’t trust the unsafe result (it might be a false positive due to abstraction) unless the prop encoding confirms that!

Now, run HiFrog with --sum-theoref option to see the tool automatically will find the appropriate encoding for each claim:

hifrog --sum-theoref sumtheoref2.c

Solution:

Exercise) Rune sumtheoref1.c with --sum-theoref

hifrog --sum-theoref sumtheoref1.c

Solution:

Removing redundant assertions:

HiFrog has an option –claims-opt which identifies and reports the redundant assertions using the threshold as the maximum number of SSA steps between the assertions including the SSA steps at the functions calls (if any) between the assertions.

rm __summaries
hifrog --logic qflra --claims-opt 20 ex_redundant.c

Error trace:

Whenever a safety property is violated, HiFrog prints a concrete counterexample mapping it to the exact lines in the program:

hifrog  --logic qflra --claim 1 ex_unsafe.c

User-Provided Summaries:

hifrog --logic qflra --list-templates sin_cos.c

Edit the summary of the nonlinear function and store it in file __summaries_nonlin and then link it to the verification of sin_cos.c by running:

hifrog --logic qflra sin_cos.c --load-summaries __summaries_nonlin

Exercise) verify the program mod_mult.c with Prop, 2) How about with EUF? 3) Generate a summary template with qflra and edit it based on your knowledge, then reuse it with LRA encoding

See the summary of mod_mult function stored in summaries_mult_mod

Tuning the strength of summaries

(or (<= 0 |abs::#return_value!0#1|) (not (<= 0 (* (- 1) |abs::#return_value!0#1|))))

(<= (- 2) |abs::#return_value!0#1|)

Proof reduction

See proof compression information

hifrog --verbose-solver 1 --reduce-proof --logic qfuf --itp-uf-algorithm 0 --claim 1 --save-summaries strong-summary-uf ex_equality.c

Part 2: UpProver Demo:

` cd lab_hifrog_upprover/upproverDemo` navigates to the directory that contains demo examples for UpProver.

How to run UpProver

rm __summaries __omega
upprover --logic qflra  version1.c --bootstrapping
upprover  --logic qflra  version1.c --summary-validation version2.c 
upprover --logic qflra ex_conj_itp_v1.c --bootstrapping
upprover --logic qflra ex_conj_itp_v1.c --TIP-check