Reorganization of tests in good_contracts (#242)

Currently we have plenty of tests which should be verified but don't
contain any contracts and/or don't check any properties related to
translation of contracts. Hence, a broader `verifies` directory is
introduced instead of `good_contracts` with tests divided by topic.

Where possible, contracts are replaced with `verify` builtin. It is also
made `vararg`.

plugins/formal-verification/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt

@@ -10,4 +10,4 @@ package org.jetbrains.kotlin.formver.plugin
  * This function hooks-in in the `formver` plugin, its invocation in a Kotlin
  * program does not do anything.
  */
-fun verify(@Suppress("UNUSED_PARAMETER") predicate: Boolean) = Unit
+fun verify(@Suppress("UNUSED_PARAMETER") vararg predicates: Boolean) = Unit

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt

@@ -22,6 +22,8 @@ import org.jetbrains.kotlin.fir.visitors.FirVisitor
 import org.jetbrains.kotlin.formver.UnsupportedFeatureBehaviour
 import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature
+import org.jetbrains.kotlin.formver.embeddings.callables.FunctionEmbedding
+import org.jetbrains.kotlin.formver.embeddings.callables.SpecialVerifyFunction
 import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
 import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.embeddings.types.buildType
@@ -186,11 +188,24 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         }
     }
 
+    private fun List<FirExpression>.withVarargsHandled(data: StmtConversionContext, function: FunctionEmbedding?) =
+        flatMap { arg ->
+            when (arg) {
+                is FirVarargArgumentsExpression -> {
+                    check(function is SpecialVerifyFunction) {
+                        "vararg arguments are currently supported for `verify` function only"
+                    }
+                    arg.arguments.map(data::convert)
+                }
+                else -> listOf(data.convert(arg))
+            }
+        }
+
     override fun visitFunctionCall(functionCall: FirFunctionCall, data: StmtConversionContext): ExpEmbedding {
         val symbol = functionCall.toResolvedCallableSymbol()
         val callee = data.embedFunction(symbol as FirFunctionSymbol<*>)
         return callee.insertCall(
-            functionCall.functionCallArguments.map(data::convert),
+            functionCall.functionCallArguments.withVarargsHandled(data, callee),
             data,
             data.embedType(functionCall.resolvedType),
         )
@@ -204,7 +219,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
             ?: throw NotImplementedError("Implicit invoke calls only support a limited range of receivers at the moment.")
         val returnType = data.embedType(implicitInvokeCall.resolvedType)
         val receiverSymbol = receiver.calleeReference.toResolvedSymbol<FirBasedSymbol<*>>()!!
-        val args = implicitInvokeCall.argumentList.arguments.map(data::convert)
+        val args = implicitInvokeCall.argumentList.arguments.withVarargsHandled(data, function = null)
         return when (val exp = data.embedLocalSymbol(receiverSymbol).ignoringMetaNodes()) {
             is LambdaExp -> {
                 // The lambda is already the receiver, so we do not need to convert it.

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt

@@ -144,11 +144,20 @@ object SpecialVerifyFunction : SpecialKotlinFunction {
     override val name: String = "verify"
 
     override fun insertCall(args: List<ExpEmbedding>, ctx: StmtConversionContext): ExpEmbedding {
-        return Assert(args[0])
+        return args.map { Assert(it) }.toBlock()
     }
 
     override val callableType: FunctionTypeEmbedding = buildFunctionPretype {
-        withParam { boolean() }
+        withParam {
+            klass {
+                withName(
+                    buildName {
+                        packageScope(listOf("kotlin"))
+                        ClassKotlinName(listOf("BooleanArray"))
+                    }
+                )
+            }
+        }
         withReturnType { unit() }
     }
 }

plugins/formal-verification/testData/diagnostics/bad_contracts/viper_verify.fir.diag.txt

@@ -1,4 +1,6 @@
 /viper_verify.kt:(125,137): info: Generated Viper text for verify_false:
+field bf$size: Ref
+
 method f$verify_false$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
@@ -10,6 +12,8 @@ method f$verify_false$TF$() returns (ret$0: Ref)
 /viper_verify.kt:(153,158): warning: Viper verification error: Assert might fail. Assertion false might not hold.
 
 /viper_verify.kt:(181,196): info: Generated Viper text for verify_compound:
+field bf$size: Ref
+
 method f$verify_compound$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {

plugins/formal-verification/testData/diagnostics/no_contracts/classes/multiple_interfaces.fir.diag.txt

@@ -63,4 +63,3 @@ method pg$public$field(this$dispatch: Ref) returns (ret: Ref)
 
 
 method ps$public$field(this$dispatch: Ref, anon$0: Ref) returns (ret: Ref)
-

plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/try_catch.fir.diag.txt

@@ -245,4 +245,3 @@ method pg$public$cause(this$dispatch: Ref) returns (ret: Ref)
 
 
 method pg$public$message(this$dispatch: Ref) returns (ret: Ref)
-

plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt → plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.fir.diag.txt

@@ -15,24 +15,24 @@ method f$isString$TF$NT$Any(p$x: Ref) returns (ret$0: Ref)
 method pg$public$length(this$dispatch: Ref) returns (ret: Ref)
 
 
-/is_type_contract.kt:(509,517): info: Generated Viper text for isString:
+/is_type_contract.kt:(322,330): info: Generated Viper text for isString:
 field bf$length: Ref
 
-method f$isString$TF$T$Any(p$obj: Ref) returns (ret$0: Ref)
+method f$isString$TF$T$Any(this$extension: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == true ==>
-    df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$c$pkg$kotlin$String())
+    df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$c$pkg$kotlin$String())
 {
-  inhale df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$anyType())
-  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$c$pkg$kotlin$String()))
+  inhale df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$anyType())
+  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$c$pkg$kotlin$String()))
   goto lbl$ret$0
   label lbl$ret$0
 }
 
 method pg$public$length(this$dispatch: Ref) returns (ret: Ref)
 
 
-/is_type_contract.kt:(675,692): info: Generated Viper text for subtypeTransitive:
+/is_type_contract.kt:(491,508): info: Generated Viper text for subtypeTransitive:
 method f$subtypeTransitive$TF$T$Unit(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
   ensures true ==>
@@ -43,7 +43,7 @@ method f$subtypeTransitive$TF$T$Unit(p$x: Ref) returns (ret$0: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
-/is_type_contract.kt:(870,891): info: Generated Viper text for constructorReturnType:
+/is_type_contract.kt:(686,707): info: Generated Viper text for constructorReturnType:
 field bf$bar: Ref
 
 method con$c$Foo$() returns (ret: Ref)
@@ -63,7 +63,7 @@ method f$constructorReturnType$TF$() returns (ret$0: Ref)
   label lbl$ret$0
 }
 
-/is_type_contract.kt:(1016,1032): info: Generated Viper text for subtypeSuperType:
+/is_type_contract.kt:(832,848): info: Generated Viper text for subtypeSuperType:
 field bf$bar: Ref
 
 method f$subtypeSuperType$TF$T$Bar(p$bar: Ref) returns (ret$0: Ref)
@@ -76,7 +76,7 @@ method f$subtypeSuperType$TF$T$Bar(p$bar: Ref) returns (ret$0: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
-/is_type_contract.kt:(1149,1160): info: Generated Viper text for typeOfField:
+/is_type_contract.kt:(965,976): info: Generated Viper text for typeOfField:
 field bf$bar: Ref
 
 method f$typeOfField$TF$T$Foo(p$foo: Ref) returns (ret$0: Ref)
@@ -88,12 +88,7 @@ method f$typeOfField$TF$T$Foo(p$foo: Ref) returns (ret$0: Ref)
   inhale acc(p$c$Foo$shared(p$foo), wildcard)
   unfold acc(p$c$Foo$shared(p$foo), wildcard)
   anon$0 := p$foo.bf$bar
-  if (df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$c$Bar())) {
-    ret$0 := df$rt$boolToRef(true)
-    goto lbl$ret$0
-  } else {
-    ret$0 := df$rt$boolToRef(false)
-    goto lbl$ret$0
-  }
+  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$c$Bar()))
+  goto lbl$ret$0
   label lbl$ret$0
 }

plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.kt → plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.kt

@@ -11,14 +11,12 @@ fun <!VIPER_TEXT!>isString<!>(x: Any?): Boolean {
     return x is String
 }
 
-// Note: this function was originally modelled as an extension on the [Any] type.
-// For the moment, since we do not support extension functions, we use an object of type [Any] as parameter.
 @OptIn(ExperimentalContracts::class)
-fun <!VIPER_TEXT!>isString<!>(obj: Any): Boolean {
+fun Any.<!VIPER_TEXT!>isString<!>(): Boolean {
     contract {
-        returns(true) implies (obj is String)
+        returns(true) implies (this@isString is String)
     }
-    return obj is String
+    return this is String
 }
 
 @OptIn(ExperimentalContracts::class)
@@ -54,10 +52,6 @@ fun <!VIPER_TEXT!>typeOfField<!>(foo: Foo): Boolean {
     contract {
         returns(true)
     }
-    if (foo.bar is Bar) {
-        return true
-    } else {
-        return false
-    }
+    return foo.bar is Bar
 }
 

plugins/formal-verification/testData/diagnostics/good_contracts/returns_booleans.fir.diag.txt → plugins/formal-verification/testData/diagnostics/verifies/contracts/returns_booleans.fir.diag.txt

@@ -85,30 +85,30 @@ method f$call_fun_with_contracts$TF$T$Boolean(p$b: Ref)
   label lbl$ret$0
 }
 
-/returns_booleans.kt:(1467,1480): info: Generated Viper text for isNullOrEmpty:
+/returns_booleans.kt:(1268,1281): info: Generated Viper text for isNullOrEmpty:
 field sp$size: Ref
 
-method f$isNullOrEmpty$TF$NT$Collection(p$collection: Ref)
+method f$isNullOrEmpty$TF$NT$Collection(this$extension: Ref)
   returns (ret$0: Ref)
-  requires p$collection != df$rt$nullValue() ==>
-    acc(p$collection.sp$size, write)
-  requires p$collection != df$rt$nullValue() ==>
-    df$rt$intFromRef(p$collection.sp$size) >= 0
-  ensures p$collection != df$rt$nullValue() ==>
-    acc(p$collection.sp$size, write)
-  ensures p$collection != df$rt$nullValue() ==>
-    df$rt$intFromRef(p$collection.sp$size) >= 0
+  requires this$extension != df$rt$nullValue() ==>
+    acc(this$extension.sp$size, write)
+  requires this$extension != df$rt$nullValue() ==>
+    df$rt$intFromRef(this$extension.sp$size) >= 0
+  ensures this$extension != df$rt$nullValue() ==>
+    acc(this$extension.sp$size, write)
+  ensures this$extension != df$rt$nullValue() ==>
+    df$rt$intFromRef(this$extension.sp$size) >= 0
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == false ==>
-    p$collection != df$rt$nullValue()
+    this$extension != df$rt$nullValue()
 {
-  inhale df$rt$isSubtype(df$rt$typeOf(p$collection), df$rt$nullable(df$rt$c$pkg$kotlin_collections$Collection()))
-  inhale p$collection != df$rt$nullValue() ==>
-    acc(p$pkg$kotlin_collections$c$Collection$shared(p$collection), wildcard)
-  if (p$collection == df$rt$nullValue()) {
+  inhale df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$nullable(df$rt$c$pkg$kotlin_collections$Collection()))
+  inhale this$extension != df$rt$nullValue() ==>
+    acc(p$pkg$kotlin_collections$c$Collection$shared(this$extension), wildcard)
+  if (this$extension == df$rt$nullValue()) {
     ret$0 := df$rt$boolToRef(true)
   } else {
-    ret$0 := f$pkg$kotlin_collections$c$Collection$isEmpty$TF$T$Collection(p$collection)}
+    ret$0 := f$pkg$kotlin_collections$c$Collection$isEmpty$TF$T$Collection(this$extension)}
   goto lbl$ret$0
   label lbl$ret$0
 }

plugins/formal-verification/testData/diagnostics/good_contracts/returns_booleans.kt → plugins/formal-verification/testData/diagnostics/verifies/contracts/returns_booleans.kt

@@ -55,13 +55,11 @@ fun <!VIPER_TEXT!>call_fun_with_contracts<!>(b: Boolean): Boolean {
     return a
 }
 
-// Note: this function was originally modelled as an extension on the [Collection<T>?] type.
-// For the moment, since we do not support extension functions, we pass an object of type [Collection<T>?] as parameter.
 @OptIn(ExperimentalContracts::class)
-public fun <T> <!VIPER_TEXT!>isNullOrEmpty<!>(collection: Collection<T>?): Boolean {
+public fun <T> Collection<T>?.<!VIPER_TEXT!>isNullOrEmpty<!>(): Boolean {
     contract {
-        returns(false) implies (collection != null)
+        returns(false) implies (this@isNullOrEmpty != null)
     }
 
-    return collection == null || collection.isEmpty()
+    return this == null || isEmpty()
 }