From 45926c441fe967cc4af06dc5dab6f1a23bc52345 Mon Sep 17 00:00:00 2001 From: Francesco Protopapa Date: Wed, 11 Sep 2024 13:27:34 +0200 Subject: [PATCH] Adjustments --- chapters/1-Introduction.typ | 12 ++++++------ chapters/2-Background.typ | 8 ++++---- preface/copyright.typ | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/chapters/1-Introduction.typ b/chapters/1-Introduction.typ index 18ebb92..5db8c67 100644 --- a/chapters/1-Introduction.typ +++ b/chapters/1-Introduction.typ @@ -4,7 +4,7 @@ = Introduction -Aliasing is a topic that has been studied for decades @Aliasing-OOP @beyondGenevaConvention @GenevaConvention in computer science and it refers to the situation where two or more references point to the same object. +Aliasing is a topic that has been studied for decades in computer science @Aliasing-OOP @beyondGenevaConvention @GenevaConvention and it refers to the situation where two or more references point to the same object. Aliasing is an important characteristic of object-oriented programming languages allowing the programmers to develope complex designs involving sharing. However, reasoning about programs written with languages that allow aliasing without any kind of control is a hard task for programmers, compilers and formal verification tools. In fact, as reported in _the Geneva Convention on the Treatment of Object Aliasing_ @GenevaConvention, without having guarantees about aliasing it can be difficult to prove the correctness of a simple Hoare formula like the following. $ {x = "true"} space y := "false" {x = "true"} $ Indeed, when $x$ and $y$ are aliased, the formula is not valid, and most of the time proving that aliasing cannot occur is not straightforward. @@ -15,7 +15,7 @@ This verification is possible because separation logic allows to express that $x This work demonstrates how controlling aliasing through an annotation system can enhance the formal verification process performed by SnaKt @FormVerPlugin, an existing plugin for the Kotlin language @KotlinSpec @Kotlin. SnaKt verifies Kotlin using Viper @ViperWebSite @Viper, an intermediate verification language developed by ETH Zurich. Viper is designed to verify programs by enabling the specification of functions with preconditions and postconditions, which are then checked for correctness. This verification is performed using one of two back-ends: symbolic execution @MuellerSchwerhoffSummers16b or verification condition generation @HeuleKassiosMuellerSummers13, both of which rely on an SMT solver to validate the specified conditions. -In order to verify to Kotlin with Viper, it is necessary to translate the former language into the latter. However, this translation presents challenges due to fundamental differences between the two languages. Specifically, Viper's memory model is based on separation logic, which disallows shared mutable references. In contrast, Kotlin does not restrict aliasing, meaning that references in Kotlin can be both shared and mutable, posing a significant challenge when trying to encode Kotlin code into Viper. +In order to verify to Kotlin with Viper, it is necessary to translate the former language into the latter. However, this translation presents several challenges due to fundamental differences between the two languages. Specifically, Viper's memory model is based on separation logic, which disallows shared mutable references. In contrast, Kotlin does not restrict aliasing, meaning that references in Kotlin can be both shared and mutable, posing a significant challenge when trying to encode Kotlin code into Viper. This issue is clearly illustrated in the Kotlin code example provided in @intro-comp. In that example, the language allows the same reference to be passed multiple times when calling function `f`, thereby creating aliasing. Additionally, @intro-comp presents a naive approach for encoding that Kotlin code into Viper. Despite the Viper code closely resembling the original Kotlin code, it fails verification when `f(x, x)` is called. This failure occurs because `f` requires write access to the field `n` of its arguments, but as previously mentioned, Viper’s separation logic disallows references from being both shared and mutable simultaneously. @@ -42,12 +42,12 @@ The rest of the thesis is organized as follows: / @cap:background : provides a description of the background information needed to understand the concepts presented by this work. In particular, this chapter presents the Kotlin programming language and its feature of interest for the thesis. Following this, the chapter provides an overview of the "Aliasing" topic in Computer Science and presents an introduction to the Viper language and its set of verification tools. -/ @cap:related-work : analyzes works that has been fundamental for the development of this thesis. The chapter is divided in two parts, the former describing existing works about aliasing and systems for controlling it; the latter gives an overview of the already existing tools that perform formal verification using Viper. +/ @cap:related-work : analyzes works that have been fundamental for the development of this thesis. The chapter is divided in two parts, the former describing existing works about aliasing and systems for controlling it; the latter giving an overview of the already existing tools that perform formal verification using Viper. -/ @cap:annotation-system : presents a novel annotation system for controlling aliasing on a language that can represent a significant subset of the Kotlin language. After introducing the language and several auxiliary rules and functions, the typing rules for the system are formalized. +/ @cap:annotations-kt : introduces a uniqueness system for the Kotlin language. It shows several examples of Kotlin code extended with uniqueness annotations and explores how the annotations can be used for bringing improvements to the language. -/ @cap:annotations-kt : discusses the application of the proposed annotation system in the Kotlin language. It shows several examples of Kotlin code extended with these annotations and explores how the annotations can be used for bringing improvements to the language. +/ @cap:annotation-system : formalizes the annotation system introduced before on a language that can represent a significant subset of the Kotlin language. After introducing the language and several auxiliary rules and functions, the typing rules for the system are formalized. -/ @cap:encoding : shows how the annotation system presented before can be used to obtain a better encoding of Kotlin into Viper, thus improving the quality of verification. +/ @cap:encoding : shows how the annotation system presented before can be used to obtain a better encoding of Kotlin into Viper, thus improving the quality of verification performed by SnaKt. / @cap:conclusion : summarizes the contributions of this research and points out reasonable extensions to this work as well as potential new areas for future research. diff --git a/chapters/2-Background.typ b/chapters/2-Background.typ index 5df5db4..ff3d081 100644 --- a/chapters/2-Background.typ +++ b/chapters/2-Background.typ @@ -39,7 +39,7 @@ In Kotlin, when the compiler can determine that a variable's type is more specif === Null Safety -Kotlin's type system has been designed with the goal of eliminating the danger of null references. In many programming languages, including Java, accessing a member of a null reference results in a null reference exception. This is more difficult to happen in Kotlin since the type system distinguishes between references that can hold `null` and those that cannot, the former are called nullable references while the latter are called non-nullable reference. @kt-null-safety shows how nullable references are declared by appending a question mark to the type name and it shows that trying to assign `null` to a non-nullable reference leads to a compilation error. +Kotlin's type system has been designed with the goal of eliminating the danger of null references. In many programming languages, including Java, accessing a member of a null reference results in a null reference exception. Kotlin avoids most of these situations because the type system distinguishes between references that can hold `null` and those that cannot, the former are called nullable references while the latter are called non-nullable references. @kt-null-safety shows how nullable references are declared by appending a question mark to the type name and it shows that trying to assign `null` to a non-nullable reference leads to a compilation error. #figure( caption: "Kotlin null safety example", @@ -86,7 +86,7 @@ A backing field is generated under two conditions: if the property relies on the set(value) { // setter if (value > 0) field = value // accessing backing field else throw IllegalArgumentException( - "Square size must be greater than 0" + "Square width must be greater than 0" ) } val area @@ -99,7 +99,7 @@ A backing field is generated under two conditions: if the property relies on the Kotlin contracts @KotlinContracts are an experimental feature introduced in Kotlin 1.3 designed to provide additional guarantees about code behavior, helping the compiler in performing more precise analysis and optimizations. Contracts are defined using a special contract block within a function, describing the relationship between input parameters and the function's effects. This can include conditions such as whether a lambda is invoked or if a function returns under certain conditions. By specifying these relationships, contracts provide guarantees to the caller of a function, offering the compiler additional information that enable more advanced code analysis. -It is important to point out that currently contracts correctness is not statically verified. The compiler trusts contracts unconditionally meaning that the programmer is responsible for writing correct and sound contracts. +It is important to point out that currently contracts are only partially verified by the compiler. In certain cases, the compiler trusts the contracts without verification, placing the responsibility on the programmer to ensure that the contracts are correct. In @contract-1 it is possible to see how contracts allow the initialization of immutable variables within the body of a lambda, doing this is not possible without using a contract (@contract-2). @@ -404,7 +404,7 @@ As well as being declared in preconditions and postconditions, field permissions Sometimes, exclusive permissions can be too restrictive. Viper also allows to have fractional permissions for heap locations that can be shared but only read. Fractional permissions are declared with a permission amount between 0 and 1 or with the `wildcard` keyword. The value represented by a `wildcard` is not constant, instead it is reselected each time an expression involving a `wildcard` is identified. -The `wildcard` permission amount provides a convenient way to implement duplicable read-only resources, which is often suitable for the representation of immutable data. The example in @vpr-fractional shows how fractional permissions can be combined to gain full permissions (Line 6-7). In the same example it is also possible to see that Viper does not allow to have a permission amount greater than 1, in fact, since `wildcard` is an amount grater than 0, a situation in which `x == y == z` is not possible and so the assertion on Line 11 can be verified. +The `wildcard` permission amount provides a convenient way to implement duplicable read-only resources, which is often suitable for the representation of immutable data. The example in @vpr-fractional shows how fractional permissions can be combined to gain full permissions (Line 6-7). In the same example it is also possible to see that Viper does not allow to have a permission amount greater than 1, in fact, since `wildcard` is an amount greater than 0, a situation in which `x == y == z` is not possible and so the assertion on Line 11 can be verified. #figure( caption: "Viper fractional permissions example", diff --git a/preface/copyright.typ b/preface/copyright.typ index 019c292..352028a 100644 --- a/preface/copyright.typ +++ b/preface/copyright.typ @@ -3,5 +3,5 @@ #set page(numbering: none) #align(left + bottom, [ - #text(myName): #text(style: "italic", myTitle.replace("\n","")), #text(myDegree), #sym.copyright #text(myTime) + #text(myName): #text(style: "italic", myTitle.replace("\n"," ")), #text(myDegree), #sym.copyright #text(myTime) ]) \ No newline at end of file