theodore-norvell / harpo Goto Github PK

Interfaces translated into constants in Boogie.

(interface MyInterface interface)

Translated to: const unique MyInterface: ClassName

Client initiate server thread but finishes it and one initiated by that server thread.

Apparently, thread body contains following commands and expressions. I'll move them out one by one into a separate issue for each.
(1) If expression translation – Some commands and statement translation
(2) While statement translation - Some commands and statement translation
(3) For statement translation - Some commands and statement translation
(4) Assignment translation
(a) Expression Translation
(5) Expression translation
(6) Method Call translation
(7) Co statement translation
(8) Assert/assume translation

OutputBuilder contains the errors set on supplied coordinated of the source file. We need mapping of verification errors to HARPO's errors.

HARPO Types are converted into Boogie Types according to following Map:
Int8 -> int
Int16 -> int
Int32 -> int
Int64 -> int
Real16 -> real
Real32 -> real
Real64 -> real
bool -> bool
CName -> Ref where CName is a reference to an instance of a class
Perm (Real(*)) -> Perm (real) (We are not using Perm types so far in HARPO, we are using Real types in HARPO to represent the permissions)
[T[N]] -> ArrayRef Tr[T]

Initialization Expressions for Heap left in another Issue.

All fields of class are translated into
Heap[This_ClassName, FieldName] := Initialization Expression.

All fields are initialized in constructor procedure of Boogie.

ObjectIdentifierCodeGeneration() method create the boogie variables of the objects in the beginning of the translated code.

if Field is constant then field declared declared and const unique ClassName.FieldName : Field Type;
axiom ClassName.FieldName == ConstValue.

All local fields are promoted to class fields.

Translation of HARPO Class declaration into Boogie.

const unique C: ClassName;

unique modifier declares that the value of the constant differs from other unique constants.

Class Implementing an interface :
<: used to represent subtyping in Boogie

(class C implements I)

const unique C:ClassName < I;

Include simple literal expressions to chain expressions.

Claim LocSet@PM

Implement the permission map using:
LocSet has two concrete cases:

-> ObjectIdLSN (exp: ExpNd)
-> ArrayLSN (forDecl: ForDecl,offSet: ExpNd,bound: ExpNd, boundInclusive: Boolean, locSet: LocSetNd)

(class Counter()
claim [email protected]
invariant canRead(count)
invariant count >_ 0
proc increment()
takes [email protected]
pre count>_0
post count'>0
gives [email protected]
obj count: Int32 := 0
(thread (t0)
(while true
do
(accept increment()
(with this
do
count := count+1
with)
accept)
while)
thread)
class)

local objects declaration and initialization need to be translated into modeled memory(Heap) with permissions on initialization.

Local Fields are promoted to class Fields Translation is similar Class Field Translation.

Contains:
a) ‘pre’
b) ‘post’
e) Some commands translation

The thread which initiates other threads is one who finishes them.

Generate Boogie code for buffer class implemented in HARPO
Compare the generated boogie code with expected boogie code

"generate Boogie code for HARPO Class Declaration "
"generate Boogie code for HARPO Interface Declaration "
"generate Boogie code for HARPO Object Declaration/Initialization "
"generate Boogie code for HARPO Constant Declaration"
"generate Boogie code for HARPO Field Declaration"
"generate Boogie code for HARPO Boolean Expression"
"generate Boogie code for HARPO Chain Expression "
"generate Boogie code for HARPO Arithmetic Expression"
"generate Boogie code for HARPO Assignment Command"
"generate Boogie code for HARPO While Command"
"generate Boogie code for HARPO For Command"
"generate Boogie code for HARPO if Expression"
"generate Boogie code for HARPO Thread Declaration"
"generate Boogie code for HARPO Method Declaration"
"generate Boogie code for HARPO Method Call"
"generate Boogie code for HARPO Class Constructor"
"generate Boogie code for HARPO Co Command"

'pre' condition
'post' condition
'gives' permission specification
'takes' permission specification
'borrows' permission specification

(class Counter()
claim [email protected]

invariant canRead(count)

invariant count >_ 0

proc increment()

takes [email protected]
pre count>_0
post count'>0
gives [email protected]
	
obj count: Int32 := 0

(thread (*t0*)
	(while true
	do
		(accept increment()
			(with this
				do
				count := count+1
			with)
		accept)
	while)
thread)

class)

Initialization expressions are checked with their defindness and converted to Boogie Expressions.

Constants are translated into constants in Boogie.
Constant declaration enforce axiom.

const C: Int32 := 30;

boogie:
const C: int;
axiom C == 10;

The client starts two server threads but finishing one of them, in turn, finish the one who left.