Skip to content

Commit

Permalink
refactoring in usvm-python-annotations
Browse files Browse the repository at this point in the history
  • Loading branch information
tochilinak committed Jun 10, 2024
1 parent 191a6a1 commit fef890b
Show file tree
Hide file tree
Showing 13 changed files with 73 additions and 73 deletions.
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
package org.usvm.annotations;

import org.usvm.annotations.codegeneration.CType;
import org.usvm.annotations.codegeneration.ObjectConverter;

import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package org.usvm.annotations

import org.usvm.annotations.codegeneration.DefinitionDescriptor
import org.usvm.annotations.codegeneration.generateCPythonAdapterDefs
import java.io.File
import javax.annotation.processing.AbstractProcessor
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,5 @@
package org.usvm.annotations

import org.usvm.annotations.codegeneration.ArgumentDescription
import org.usvm.annotations.codegeneration.CPythonFunctionDescription
import org.usvm.annotations.codegeneration.CType
import org.usvm.annotations.codegeneration.JavaType
import org.usvm.annotations.codegeneration.ObjectConverter
import org.usvm.annotations.codegeneration.generateCPythonFunctionHeader
import org.usvm.annotations.codegeneration.generateCPythonFunctionsImpls
import java.io.File
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
package org.usvm.annotations

data class MemberDescriptorInfo(
val nativeTypeName: String,
val nativeMemberName: String,
val javaMemberName: String,
)

const val MEMBER_DESCRIPTION_QUALNAME = "Lorg/usvm/interpreter/MemberDescriptor;"

enum class ObjectConverter(val repr: String) {
StandardConverter("object_converter"),
FrameConverter("frame_converter"),
IntConverter("int_converter"),
RefConverter("ref_converter"),
ObjectWrapper("object_wrapper"),
ArrayConverter("array_converter"),
TupleConverter("tuple_converter"),
StringConverter("string_converter"),
ObjectIdConverter("object_id_converter"),
NoConverter(""),
}

enum class CType(val repr: String) {
PyObject("PyObject *"),
PyObjectArray("PyObject **"),
PyFrameObject("PyFrameObject *"),
CInt("int"),
CStr("const char *"),
JObject("jobject"),
}

enum class JavaType(val repr: String, val call: String) {
JObject("jobject", "Object"),
JLong("jlong", "Long"),
JInt("jint", "Int"),
JBoolean("jboolean", "Boolean"),
JObjectArray("jobjectArray", "Object"),
NoType("", "Void"),
}

data class ArgumentDescription(
val cType: CType,
val javaType: JavaType,
val converter: ObjectConverter,
)

data class CPythonFunctionDescription(
val cName: String,
val args: List<ArgumentDescription>,
val result: ArgumentDescription,
val failValue: String,
val defaultValue: String,
val addToSymbolicAdapter: Boolean,
)

data class DefinitionDescriptor(
val cName: String,
val javaName: String,
val javaSignature: String,
)
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package org.usvm.annotations

import org.usvm.annotations.codegeneration.MemberDescriptorInfo
import org.usvm.annotations.codegeneration.generateDescriptorChecks
import java.io.File
import javax.annotation.processing.AbstractProcessor
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package org.usvm.annotations

import org.usvm.annotations.codegeneration.MemberDescriptorInfo
import org.usvm.annotations.codegeneration.generateMethodDescriptorChecks
import java.io.File
import javax.annotation.processing.AbstractProcessor
Expand Down
Original file line number Diff line number Diff line change
@@ -1,50 +1,7 @@
package org.usvm.annotations.codegeneration

enum class ObjectConverter(val repr: String) {
StandardConverter("object_converter"),
FrameConverter("frame_converter"),
IntConverter("int_converter"),
RefConverter("ref_converter"),
ObjectWrapper("object_wrapper"),
ArrayConverter("array_converter"),
TupleConverter("tuple_converter"),
StringConverter("string_converter"),
ObjectIdConverter("object_id_converter"),
NoConverter(""),
}

enum class CType(val repr: String) {
PyObject("PyObject *"),
PyObjectArray("PyObject **"),
PyFrameObject("PyFrameObject *"),
CInt("int"),
CStr("const char *"),
JObject("jobject"),
}

enum class JavaType(val repr: String, val call: String) {
JObject("jobject", "Object"),
JLong("jlong", "Long"),
JInt("jint", "Int"),
JBoolean("jboolean", "Boolean"),
JObjectArray("jobjectArray", "Object"),
NoType("", "Void"),
}

data class ArgumentDescription(
val cType: CType,
val javaType: JavaType,
val converter: ObjectConverter,
)

data class CPythonFunctionDescription(
val cName: String,
val args: List<ArgumentDescription>,
val result: ArgumentDescription,
val failValue: String,
val defaultValue: String,
val addToSymbolicAdapter: Boolean,
)
import org.usvm.annotations.CPythonFunctionDescription
import org.usvm.annotations.JavaType

fun generateCPythonFunction(description: CPythonFunctionDescription): Pair<String, String> {
val cName = description.cName
Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
package org.usvm.annotations.codegeneration

data class DefinitionDescriptor(
val cName: String,
val javaName: String,
val javaSignature: String,
)
import org.usvm.annotations.DefinitionDescriptor

fun generateCPythonAdapterDefs(defs: List<DefinitionDescriptor>): String {
val jmethodIDMacro = defs.fold("#define HANDLERS_DEFS ") { acc, def ->
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,7 @@
package org.usvm.annotations.codegeneration

data class MemberDescriptorInfo(
val nativeTypeName: String,
val nativeMemberName: String,
val javaMemberName: String,
)
import org.usvm.annotations.MEMBER_DESCRIPTION_QUALNAME
import org.usvm.annotations.MemberDescriptorInfo

fun generateDescriptorCheck(info: MemberDescriptorInfo): String =
"""
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
package org.usvm.annotations.codegeneration

import org.usvm.annotations.ArgumentDescription
import org.usvm.annotations.CPythonFunctionDescription
import org.usvm.annotations.CType
import org.usvm.annotations.JavaType
import org.usvm.annotations.ObjectConverter
import org.usvm.annotations.ids.SymbolicMethodId

fun generateSymbolicMethod(id: SymbolicMethodId): String {
Expand Down Expand Up @@ -55,7 +60,7 @@ fun generateSymbolicMethodInitialization(): String {
}

fun generateMethodCheck(): String {
val items = SymbolicMethodId.values().map {
val items = SymbolicMethodId.entries.map {
"""
if (ptr == ${it.cName})
return ${it.cName};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import org.usvm.annotations.*;
import org.usvm.annotations.codegeneration.CType;
import org.usvm.annotations.codegeneration.ObjectConverter;
import org.usvm.annotations.ids.ApproximationId;
import org.usvm.annotations.ids.SymbolicMethodId;
import org.usvm.language.*;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,4 @@ class BadModelException : PyExecutionExceptionFromJava()

class InstructionLimitExceededException : PyExecutionExceptionFromJava()

class CancelledExecutionException : PyExecutionExceptionFromJava()
class CancelledExecutionException : PyExecutionExceptionFromJava()

0 comments on commit fef890b

Please sign in to comment.