Skip to content

Commit

Permalink
Fixed Python build
Browse files Browse the repository at this point in the history
  • Loading branch information
@tochilinak
tochilinak committed Dec 20, 2024
1 parent 63fb14c commit 556fa95
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 20 deletions.
7 changes: 2 additions & 5 deletions .../usvm-python-annotations/src/main/kotlin/org/usvm/annotations/CPythonFunctionProcessor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,7 @@ class CPythonFunctionProcessor : AbstractProcessor() {
val firstType = executable.parameters
.first()
.asType()
.toString()
.split(".")
.last()
.getTypeName()
require(firstType == "ConcolicRunContext") {
"First argument of function annotated with CPythonFunction must be ConcolicRunContext"
}
Expand All @@ -74,8 +72,7 @@ class CPythonFunctionProcessor : AbstractProcessor() {
require(returnTypeName == "void" || returnTypeName == "SymbolForCPython") {
"Return type must be void or SymbolForCPython, not $returnTypeName"
}
val returnType = convertJavaType(executable.returnType)
when (returnType) {
when (val returnType = convertJavaType(executable.returnType)) {
JavaType.JObject -> {
val descr = ArgumentDescription(
CType.PyObject,
Expand Down
8 changes: 3 additions & 5 deletions ...n/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/SymbolicMethodProcessor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,15 +51,13 @@ class SymbolicMethodProcessor : AbstractProcessor() {
val arg0 = element.parameters
.first()
.asType()
.toString()
.split(".")
.last()
.getTypeName()
require(arg0 == "ConcolicRunContext") { formatMsg }
val arg1 = element.parameters[1].asType().toString().split(".").last()
val arg1 = element.parameters[1].asType().getTypeName()
require(arg1 == "SymbolForCPython") { formatMsg }
val arg2 = element.parameters[2].asType()
require(arg2 is ArrayType) { formatMsg }
val arg2Elem = arg2.componentType.toString().split(".").last()
val arg2Elem = arg2.componentType.getTypeName()
require(arg2Elem == "SymbolForCPython") { formatMsg }
val elementAnnotation = element.getAnnotation(SymbolicMethod::class.java)!!
require(elementAnnotation.id !in definedIds) {
Expand Down
5 changes: 5 additions & 0 deletions usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/Utils.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,15 @@ package org.usvm.annotations

import java.io.File
import javax.annotation.processing.ProcessingEnvironment
import javax.lang.model.element.VariableElement

Check warning

Code scanning / detekt

Detects unused imports Warning

Unused import
import javax.lang.model.type.TypeMirror

fun getHeaderPath(processingEnv: ProcessingEnvironment): File {
val headerPath = processingEnv.options["headerPath"] ?: error("Header path not specified")
val result = File(headerPath)
result.mkdirs()
return result
}

fun TypeMirror.getTypeName(): String =
toString().split('.').last().split(' ').last()
20 changes: 10 additions & 10 deletions usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ public class CPythonAdapter {
argCTypes = {CType.PyFrameObject},
argConverters = {ObjectConverter.FrameConverter}
)
public static void handlerInstruction(@NotNull ConcolicRunContext context, long frameRef) {
public static void handlerInstruction(ConcolicRunContext context, long frameRef) {
if (pythonExceptionOccurred() != 0)
return;
context.curOperation = null;
Expand Down Expand Up @@ -1255,60 +1255,60 @@ public static SymbolForCPython handlerCreateEmptyObject(ConcolicRunContext conte

@CPythonAdapterJavaMethod(cName = "symbolic_method_int")
@SymbolicMethod(id = SymbolicMethodId.Int)
public static SymbolForCPython symbolicMethodInt(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodInt(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
assert(self == null);
return withTracing(context, new SymbolicMethodParameters("int", null, args), () -> symbolicMethodIntKt(context, args));
}

@CPythonAdapterJavaMethod(cName = "symbolic_method_float")
@SymbolicMethod(id = SymbolicMethodId.Float)
public static SymbolForCPython symbolicMethodFloat(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodFloat(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
assert(self == null);
return withTracing(context, new SymbolicMethodParameters("float", null, args), () -> symbolicMethodFloatKt(context, args));
}

@CPythonAdapterJavaMethod(cName = "symbolic_method_enumerate")
@SymbolicMethod(id = SymbolicMethodId.Enumerate)
public static SymbolForCPython symbolicMethodEnumerate(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodEnumerate(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
assert(self == null);
return withTracing(context, new SymbolicMethodParameters("enumerate", null, args), () -> symbolicMethodEnumerateKt(context, args));
}

@CPythonAdapterJavaMethod(cName = "symbolic_method_list_append")
@SymbolicMethod(id = SymbolicMethodId.ListAppend)
public static SymbolForCPython symbolicMethodListAppend(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodListAppend(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("list_append", self, args), () -> symbolicMethodListAppendKt(context, self, args));
}
@SymbolicMethodDescriptor(nativeTypeName = "PyList_Type", nativeMemberName = "append")
public MemberDescriptor listAppendDescriptor = new MethodDescriptor(SymbolicMethodId.ListAppend);

@CPythonAdapterJavaMethod(cName = "symbolic_method_list_insert")
@SymbolicMethod(id = SymbolicMethodId.ListInsert)
public static SymbolForCPython symbolicMethodListInsert(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodListInsert(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("list_insert", self, args), () -> symbolicMethodListInsertKt(context, self, args));
}
@SymbolicMethodDescriptor(nativeTypeName = "PyList_Type", nativeMemberName = "insert")
public MemberDescriptor listInsertDescriptor = new MethodDescriptor(SymbolicMethodId.ListInsert);

@CPythonAdapterJavaMethod(cName = "symbolic_method_list_pop")
@SymbolicMethod(id = SymbolicMethodId.ListPop)
public static SymbolForCPython symbolicMethodListPop(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodListPop(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("list_pop", self, args), () -> symbolicMethodListPopKt(context, self, args));
}
@SymbolicMethodDescriptor(nativeTypeName = "PyList_Type", nativeMemberName = "pop")
public MemberDescriptor listPopDescriptor = new MethodDescriptor(SymbolicMethodId.ListPop);

@CPythonAdapterJavaMethod(cName = "symbolic_method_list_extend")
@SymbolicMethod(id = SymbolicMethodId.ListExtend)
public static SymbolForCPython symbolicMethodListExtend(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodListExtend(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("list_extend", self, args), () -> symbolicMethodListExtendKt(context, self, args));
}
@SymbolicMethodDescriptor(nativeTypeName = "PyList_Type", nativeMemberName = "extend")
public MemberDescriptor listExtendDescriptor = new MethodDescriptor(SymbolicMethodId.ListExtend);

@CPythonAdapterJavaMethod(cName = "symbolic_method_list_clear")
@SymbolicMethod(id = SymbolicMethodId.ListClear)
public static SymbolForCPython symbolicMethodListClear(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodListClear(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("list_clear", self, args), () -> symbolicMethodListClearKt(context, self, args));
}
@SymbolicMethodDescriptor(nativeTypeName = "PyList_Type", nativeMemberName = "clear")
Expand Down Expand Up @@ -1346,7 +1346,7 @@ public static SymbolForCPython symbolicMethodListClear(ConcolicRunContext contex

@CPythonAdapterJavaMethod(cName = "symbolic_method_set_add")
@SymbolicMethod(id = SymbolicMethodId.SetAdd)
public static SymbolForCPython symbolicMethodSetAdd(ConcolicRunContext context, @Nullable SymbolForCPython self, SymbolForCPython[] args) {
public static SymbolForCPython symbolicMethodSetAdd(ConcolicRunContext context, /* nullable */ SymbolForCPython self, SymbolForCPython[] args) {
return withTracing(context, new SymbolicMethodParameters("set_add", self, args), () -> symbolicMethodSetAddKt(context, self, args));
}

Expand Down

0 comments on commit 556fa95

Please sign in to comment.