Updated usvm-api and approximations (#204)

MchKosticyn · web-flow · commit e1e3ac7b8371 · 2024-08-07T20:20:51.000+03:00
* updated usvm-api

- added encoder api
- added implementations for 'Engine' methods

* updated approximations
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
@@ -28,6 +28,11 @@ fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefWithSameTy
 ): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
     mockSymbolicRef { objectTypeEquals(it, representative) }
 
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefWithSameType(
+    representative: UHeapRef
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { ctx.mkOr(objectTypeEquals(it, representative), ctx.mkEq(it, ctx.nullRef)) }
+
 fun <Method> UState<*, Method, *, *, *, *>.makeSymbolicRefUntyped(): UHeapRef =
     memory.mocker.createMockSymbol(trackedLiteral = null, ctx.addressSort)
 
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
@@ -70,6 +70,7 @@ import kotlin.reflect.KFunction0
 import kotlin.reflect.KFunction1
 import kotlin.reflect.KFunction2
 import kotlin.reflect.jvm.javaMethod
+import org.usvm.api.makeNullableSymbolicRefWithSameType
 
 class JcMethodApproximationResolver(
     private val ctx: JcContext,
@@ -110,63 +111,68 @@ class JcMethodApproximationResolver(
     }
 
     private fun approximateRegularMethod(methodCall: JcMethodCall): Boolean = with(methodCall) {
-        if (method.enclosingClass == usvmApiSymbolicList) {
+        val enclosingClass = method.enclosingClass
+        val className = enclosingClass.name
+
+        if (enclosingClass == usvmApiSymbolicList) {
             approximateUsvmSymbolicListMethod(methodCall)
             return true
         }
 
-        if (method.enclosingClass == usvmApiSymbolicMap) {
+        if (enclosingClass == usvmApiSymbolicMap) {
             approximateUsvmSymbolicMapMethod(methodCall)
             return true
         }
 
-        if (method.enclosingClass == usvmApiSymbolicIdentityMap) {
+        if (enclosingClass == usvmApiSymbolicIdentityMap) {
             approximateUsvmSymbolicIdMapMethod(methodCall)
             return true
         }
 
-        if (method.enclosingClass == ctx.cp.objectClass) {
+        if (enclosingClass == ctx.cp.objectClass) {
             if (approximateObjectVirtualMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass == ctx.classType.jcClass) {
+        if (enclosingClass == ctx.classType.jcClass) {
             if (approximateClassVirtualMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass.name == "jdk.internal.misc.Unsafe") {
+        if (className == "jdk.internal.misc.Unsafe") {
             if (approximateUnsafeVirtualMethod(methodCall)) return true
         }
 
-        if (method.name == "clone" && method.enclosingClass == ctx.cp.objectClass) {
+        if (method.name == "clone" && enclosingClass == ctx.cp.objectClass) {
             if (approximateArrayClone(methodCall)) return true
         }
 
         return approximateEmptyNativeMethod(methodCall)
     }
 
     private fun approximateStaticMethod(methodCall: JcMethodCall): Boolean = with(methodCall) {
-        if (method.enclosingClass == usvmApiEngine) {
+        val enclosingClass = method.enclosingClass
+        val className = enclosingClass.name
+        if (enclosingClass == usvmApiEngine) {
             approximateUsvmApiEngineStaticMethod(methodCall)
             return true
         }
 
-        if (method.enclosingClass == ctx.classType.jcClass) {
+        if (enclosingClass == ctx.classType.jcClass) {
             if (approximateClassStaticMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass.name == "java.lang.System") {
+        if (className == "java.lang.System") {
             if (approximateSystemStaticMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass.name == "java.lang.StringUTF16") {
+        if (className == "java.lang.StringUTF16") {
             if (approximateStringUtf16StaticMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass.name == "java.lang.Float") {
+        if (className == "java.lang.Float") {
             if (approximateFloatStaticMethod(methodCall)) return true
         }
 
-        if (method.enclosingClass.name == "java.lang.Double") {
+        if (className == "java.lang.Double") {
             if (approximateDoubleStaticMethod(methodCall)) return true
         }
 
@@ -208,6 +214,7 @@ class JcMethodApproximationResolver(
             scope.doWithState {
                 skipMethodInvocationWithValue(methodCall, classRef)
             }
+
             return true
         }
 
@@ -602,13 +609,27 @@ class JcMethodApproximationResolver(
                 val (ref0, ref1) = it.arguments.map { it.asExpr(ctx.addressSort) }
                 scope.calcOnState { objectTypeEquals(ref0, ref1) }
             }
+            dispatchUsvmApiMethod(Engine::typeIs) {
+                val (ref, classRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+                val classRefTypeRepresentative = scope.calcOnState {
+                    memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
+                }
+                scope.calcOnState { objectTypeEquals(ref, classRefTypeRepresentative) }
+            }
             dispatchMkRef(Engine::makeSymbolic) {
                 val classRef = it.arguments.single().asExpr(ctx.addressSort)
                 val classRefTypeRepresentative = scope.calcOnState {
                     memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
                 }
                 scope.makeSymbolicRefWithSameType(classRefTypeRepresentative)
             }
+            dispatchMkRef(Engine::makeNullableSymbolic) {
+                val classRef = it.arguments.single().asExpr(ctx.addressSort)
+                val classRefTypeRepresentative = scope.calcOnState {
+                    memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
+                }
+                scope.makeNullableSymbolicRefWithSameType(classRefTypeRepresentative)
+            }
             dispatchMkRef2(Engine::makeSymbolicArray) {
                 val (elementClassRefExpr, sizeExpr) = it.arguments
                 val elementClassRef = elementClassRefExpr.asExpr(ctx.addressSort)
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/Engine.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/Engine.java
@@ -1,121 +1,115 @@
 package org.usvm.api;
 
+import org.usvm.api.internal.SymbolicIdentityMapImpl;
+import org.usvm.api.internal.SymbolicListImpl;
+import org.usvm.api.internal.SymbolicMapImpl;
+
+import java.lang.reflect.Array;
+
 public class Engine {
+
     public static void assume(boolean expr) {
-        engineApiStubError();
+        assert expr;
     }
 
+    @SuppressWarnings("unused")
     public static <T> T makeSymbolic(Class<T> clazz) {
-        engineApiStubError();
+        return null;
+    }
+
+    @SuppressWarnings("unused")
+    public static <T> T makeNullableSymbolic(Class<T> clazz) {
         return null;
     }
 
     public static boolean makeSymbolicBoolean() {
-        engineApiStubError();
         return false;
     }
 
     public static byte makeSymbolicByte() {
-        engineApiStubError();
         return 0;
     }
 
     public static char makeSymbolicChar() {
-        engineApiStubError();
         return 0;
     }
 
     public static short makeSymbolicShort() {
-        engineApiStubError();
         return 0;
     }
 
     public static int makeSymbolicInt() {
-        engineApiStubError();
         return 0;
     }
 
     public static long makeSymbolicLong() {
-        engineApiStubError();
         return 0;
     }
 
     public static float makeSymbolicFloat() {
-        engineApiStubError();
         return 0;
     }
 
     public static double makeSymbolicDouble() {
-        engineApiStubError();
         return 0;
     }
 
+    @SuppressWarnings("unchecked")
     public static <T> T[] makeSymbolicArray(Class<T> clazz, int size) {
-        engineApiStubError();
-        return null;
+        assert clazz.isArray();
+
+        return (T[]) Array.newInstance(clazz, size);
     }
 
     public static boolean[] makeSymbolicBooleanArray(int size) {
-        engineApiStubError();
-        return null;
+        return new boolean[size];
     }
 
     public static byte[] makeSymbolicByteArray(int size) {
-        engineApiStubError();
-        return null;
+        return new byte[size];
     }
 
     public static char[] makeSymbolicCharArray(int size) {
-        engineApiStubError();
-        return null;
+        return new char[size];
     }
 
     public static short[] makeSymbolicShortArray(int size) {
-        engineApiStubError();
-        return null;
+        return new short[size];
     }
 
     public static int[] makeSymbolicIntArray(int size) {
-        engineApiStubError();
-        return null;
+        return new int[size];
     }
 
     public static long[] makeSymbolicLongArray(int size) {
-        engineApiStubError();
-        return null;
+        return new long[size];
     }
 
     public static float[] makeSymbolicFloatArray(int size) {
-        engineApiStubError();
-        return null;
+        return new float[size];
     }
 
     public static double[] makeSymbolicDoubleArray(int size) {
-        engineApiStubError();
-        return null;
+        return new double[size];
     }
 
     public static <T> SymbolicList<T> makeSymbolicList() {
-        engineApiStubError();
-        return null;
+        return new SymbolicListImpl<>();
     }
 
     public static <K, V> SymbolicMap<K, V> makeSymbolicMap() {
-        engineApiStubError();
-        return null;
+        return new SymbolicMapImpl<>();
     }
 
     public static <K, V> SymbolicIdentityMap<K, V> makeSymbolicIdentityMap() {
-        engineApiStubError();
-        return null;
+        return new SymbolicIdentityMapImpl<>();
     }
 
     public static boolean typeEquals(Object a, Object b) {
-        engineApiStubError();
-        return false;
+        return a.getClass() == b.getClass();
     }
 
-    private static void engineApiStubError() {
-        throw new IllegalStateException("Engine API method must not be invoked");
+    public static boolean typeIs(Object a, Class<?> type) {
+        return a.getClass() == type;
     }
 }
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/EncoderFor.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/EncoderFor.java
@@ -0,0 +1,9 @@
+package org.usvm.api.encoder;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+
+@Target({ElementType.TYPE})
+public @interface EncoderFor {
+    Class<?> value();
+}
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/ObjectEncoder.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/ObjectEncoder.java
@@ -0,0 +1,5 @@
+package org.usvm.api.encoder;
+
+public interface ObjectEncoder {
+    Object encode(Object object);
+}
