Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixed Python build #231

Merged
merged 1 commit into from
Dec 20, 2024
Merged

Fixed Python build #231

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions .../usvm-python-annotations/src/main/kotlin/org/usvm/annotations/CPythonFunctionProcessor.kt
View file
Open in desktop
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
Open in desktop
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
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,15 @@

import java.io.File
import javax.annotation.processing.ProcessingEnvironment
import javax.lang.model.element.VariableElement
Dismissed Show dismissed Hide dismissed
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
Open in desktop
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
Loading