#program verification

Click Here

SN Computer Science - AutoAlias: Automatic Variable-Precision Alias Analysis for Object-Oriented Programs #aliasanalysis #oop #programming #programverification

From the journal, SN Computer Science, comes a paper on AutoAlias: Automatic Variable-Precision Alias Analysis for Object-Oriented Programs. This paper is free to read (link) through 2021.

Abstract

The aliasing question (can two reference expressions point, during an execution, to the same object?) is both one of the most critical in practice, for applications ranging from compiler…

Given what I figured out in yesterday's post about hints, I have fixed the memory use problem I had before while checking my Mesh invariant for admissibility.

I think I finally understand where VCC Hints can be used.

Here is some example code. It is like the PairedList code I posted before, but now has internal arrays which are only partially used, and the use of witnesses has been removed. The important parts are the ownership invariants and the in_array invariants.

#include <vcc.h> #include <stdlib.h> //malloc typedef struct Paired Paired; typedef struct Paired { Paired* pair; } Paired; typedef _(dynamic_owns) struct PairedVarLists { //Used size of the arrays size_t num1; size_t num2; //Maximum sizes of the arrays size_t cap1; size_t cap2; //Size invariants _(invariant num1 <= cap1) _(invariant num2 <= cap2) _(invariant cap1 > 0) _(invariant cap2 > 0) //Arrays storing Paired objects Paired* pairarray1; Paired* pairarray2; //Require that the arrays do not overlap _(invariant pairarray1 != pairarray2) _(invariant \arrays_disjoint(pairarray1, cap1, pairarray2, cap2)) //Array objects (needed for free/dispose) _(ghost \object arrayob1) _(ghost \object arrayob2) //Array object invariants _(invariant arrayob1 == (Paired[cap1])pairarray1) _(invariant arrayob2 == (Paired[cap2])pairarray2) _(invariant \malloc_root(arrayob1)) _(invariant \malloc_root(arrayob2)) _(invariant \mine(arrayob1) && \mine(arrayob2)) //Ownership invariants _(invariant \forall \natural i; {&pairarray1[i]} i < cap1 ==> \mine(&pairarray1[i]) ) _(invariant \forall \natural j; {&pairarray2[j]} j < cap2 ==> \mine(&pairarray2[j]) ) //in_array invariants //Note that either the :hints or the \mine()s are needed _(invariant \forall \natural i; {:hint \mine(&pairarray1[i])} i < num1 ==> //\mine(&pairarray1[i]) && \in_array(pairarray1[i].pair, pairarray2, num2) ) _(invariant \forall \natural j; {:hint \mine(&pairarray2[j])} j < num2 ==> //\mine(&pairarray2[j]) && \in_array(pairarray2[j].pair, pairarray1, num1) ) //Pairing invariants (paired structure) //...omitted } PairedVarLists;

Either the "{:hint \mine(&pairarray1[i])}" hints or the "\mine(&pairarray1[i])" parts of the in_array invariants are needed. The hints hearken to the ownership invariants, while the "\mine"s introduce the ownership information again in a redundant way. In this case, the \mine versions let the admissibility check succeed faster. If both are omitted, the admissibility check fails by running out of memory.