From a94eb5ba67f052c0e103d0ed639f8e8a742c7c20 Mon Sep 17 00:00:00 2001 From: Mark Efremov <140056918+jefremof@users.noreply.github.com> Date: Tue, 3 Sep 2024 06:42:43 +0300 Subject: [PATCH] [python] Introducing virtual objects with multiple sets of slots (#209) * Support multiple virtual object types * Fix mask declared type * Fix mask const qualifier * Fix mask const qualifier * Fix mask const qualifier * Fix typo * Fix header * Fix header * Fix header * Fix: Remove trailing space * Rename: allocateVirtualObject -> allocateRawVirtualObject * Feat: slot mapping using enum * Feat: generation of available slots based on enum * Add slot disabling test * Fix type mismatch * Minor fixes * Linter fix * fix: simplify mandatory slots integration * minor fixes * linter fix --- usvm-python/build.gradle.kts | 1 + .../src/main/c/include/virtual_objects.h | 13 +- .../c/org_usvm_interpreter_CPythonAdapter.c | 18 +- .../src/main/c/virtual_objects.c | 156 +++++++++++++--- .../org/usvm/samples/VirtualObjectsTest.kt | 174 ++++++++++++++++++ .../annotations/SymbolicMethodProcessor.kt | 6 + .../codegeneration/AvailableSlotGeneration.kt | 19 ++ .../kotlin/org/usvm/annotations/ids/SlotId.kt | 52 ++++++ .../org/usvm/interpreter/CPythonAdapter.java | 3 +- .../concrete/ConcretePythonInterpreter.kt | 17 +- .../concrete/utils/VirtualPythonObject.kt | 4 + 11 files changed, 427 insertions(+), 36 deletions(-) create mode 100644 usvm-python/src/test/kotlin/org/usvm/samples/VirtualObjectsTest.kt create mode 100644 usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/codegeneration/AvailableSlotGeneration.kt create mode 100644 usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/ids/SlotId.kt diff --git a/usvm-python/build.gradle.kts b/usvm-python/build.gradle.kts index 3aa8e32844..3f940910a7 100644 --- a/usvm-python/build.gradle.kts +++ b/usvm-python/build.gradle.kts @@ -12,6 +12,7 @@ dependencies { implementation(project(":usvm-core")) implementation(project(":$USVM_PYTHON_MAIN_MODULE")) implementation(project(":$USVM_PYTHON_COMMONS_MODULE")) + implementation(project(":$USVM_PYTHON_ANNOTATIONS_MODULE")) implementation(Libs.python_types_api) implementation(Libs.logback) } diff --git a/usvm-python/cpythonadapter/src/main/c/include/virtual_objects.h b/usvm-python/cpythonadapter/src/main/c/include/virtual_objects.h index 43356483e8..180f958632 100644 --- a/usvm-python/cpythonadapter/src/main/c/include/virtual_objects.h +++ b/usvm-python/cpythonadapter/src/main/c/include/virtual_objects.h @@ -4,9 +4,11 @@ extern "C" { #endif +#include "limits.h" #include "Python.h" #include "utils.h" #include "symbolicadapter.h" +#include "AvailableSlots.h" // generated #define VirtualObjectTypeName "ibmviqhlye.___virtual_object___ibmviqhlye" @@ -17,12 +19,17 @@ typedef struct { SymbolicAdapter *adapter; } VirtualPythonObject; -void initialize_virtual_object_type(); -PyObject *allocate_raw_virtual_object(JNIEnv *env, jobject object); +void initialize_virtual_object_available_slots(); +void deinitialize_virtual_object_available_slots(); +void initialize_virtual_object_ready_types(); +void deinitialize_virtual_object_ready_types(); +PyObject *_allocate_raw_virtual_object(JNIEnv *env, jobject object, const unsigned char *mask, size_t length); +PyObject *allocate_raw_virtual_object_with_all_slots(JNIEnv *env, jobject object); +PyObject *allocate_raw_virtual_object(JNIEnv *env, jobject object, jbyteArray mask); void finish_virtual_object_initialization(VirtualPythonObject *object, ConcolicContext *ctx, SymbolicAdapter *adapter); PyObject *create_new_virtual_object(ConcolicContext *ctx, jobject object, SymbolicAdapter *adapter); int is_virtual_object(PyObject *obj); -void register_virtual_methods(); +void register_virtual_methods(SymbolicAdapter *adapter); #ifdef __cplusplus } diff --git a/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c b/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c index e1a4ef7ada..9c1ba78822 100644 --- a/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c +++ b/usvm-python/cpythonadapter/src/main/c/org_usvm_interpreter_CPythonAdapter.c @@ -77,7 +77,8 @@ JNIEXPORT void JNICALL Java_org_usvm_interpreter_CPythonAdapter_initializePython SET_LONG_FIELD("pyNoneRef", (jlong) Py_None) initialize_java_python_type(); - initialize_virtual_object_type(); + initialize_virtual_object_available_slots(); + initialize_virtual_object_ready_types(); PySys_AddAuditHook(audit_hook, &illegal_operation); @@ -89,6 +90,8 @@ JNIEXPORT void JNICALL Java_org_usvm_interpreter_CPythonAdapter_initializeSpecia } JNIEXPORT void JNICALL Java_org_usvm_interpreter_CPythonAdapter_finalizePython(JNIEnv *env, jobject cpython_adapter) { + deinitialize_virtual_object_available_slots(); + deinitialize_virtual_object_ready_types(); release_global_refs(env); clean_methods(); Py_FinalizeEx(); @@ -363,8 +366,17 @@ JNIEXPORT jlong JNICALL Java_org_usvm_interpreter_CPythonAdapter_getCodeFromFram return (jlong) PyFrame_GetCode((PyFrameObject *) frame_ref); } -JNIEXPORT jlong JNICALL Java_org_usvm_interpreter_CPythonAdapter_allocateVirtualObject(JNIEnv *env, jobject cpython_adapter, jobject virtual_object) { - return (jlong) allocate_raw_virtual_object(env, virtual_object); +JNIEXPORT jlong JNICALL Java_org_usvm_interpreter_CPythonAdapter_allocateRawVirtualObjectWithAllSlots(JNIEnv *env, jobject cpython_adapter, jobject virtual_object) { + return (jlong) allocate_raw_virtual_object_with_all_slots(env, virtual_object); +} + +JNIEXPORT jlong JNICALL Java_org_usvm_interpreter_CPythonAdapter_allocateRawVirtualObject( + JNIEnv *env, + jobject cpython_adapter, + jobject virtual_object, + jbyteArray mask +) { + return (jlong) allocate_raw_virtual_object(env, virtual_object, mask); } JNIEXPORT jlong JNICALL Java_org_usvm_interpreter_CPythonAdapter_makeList(JNIEnv *env, jobject cpython_adapter, jlongArray elements) { diff --git a/usvm-python/cpythonadapter/src/main/c/virtual_objects.c b/usvm-python/cpythonadapter/src/main/c/virtual_objects.c index a3519b9299..1208f81e32 100644 --- a/usvm-python/cpythonadapter/src/main/c/virtual_objects.c +++ b/usvm-python/cpythonadapter/src/main/c/virtual_objects.c @@ -186,6 +186,13 @@ nb_matrix_multiply(PyObject *first, PyObject *second) { } PyType_Slot Virtual_nb_matrix_multiply = {Py_nb_matrix_multiply, nb_matrix_multiply}; +static PyObject * +sq_concat(PyObject *first, PyObject *second) { + DEBUG_OUTPUT("sq_concat") + BINARY_FUNCTION +} +PyType_Slot Virtual_sq_concat = {Py_sq_concat, sq_concat}; + static Py_ssize_t sq_length(PyObject *self) { DEBUG_OUTPUT("sq_length") @@ -229,31 +236,87 @@ tp_setattro(PyObject *self, PyObject *attr, PyObject *value) { } PyType_Slot Virtual_tp_setattro = {Py_tp_setattro, tp_setattro}; +PyType_Slot final_slot = {0, NULL}; + + +PyType_Slot *AVAILABLE_SLOTS = 0; +PyObject *ready_virtual_object_types = 0; -PyTypeObject *VirtualPythonObject_Type = 0; void -initialize_virtual_object_type() { - PyType_Slot slots[] = { - Virtual_tp_dealloc, - Virtual_tp_richcompare, - Virtual_tp_getattro, - Virtual_tp_setattro, - Virtual_tp_iter, - Virtual_tp_hash, - Virtual_tp_call, - Virtual_nb_bool, - Virtual_nb_add, - Virtual_nb_subtract, - Virtual_nb_multiply, - Virtual_nb_matrix_multiply, - Virtual_nb_negative, - Virtual_nb_positive, - Virtual_sq_length, - Virtual_mp_subscript, - Virtual_mp_ass_subscript, - {0, 0} - }; +initialize_virtual_object_ready_types() { + ready_virtual_object_types = PyDict_New(); +} + +void +deinitialize_virtual_object_ready_types() { + Py_DECREF(ready_virtual_object_types); + ready_virtual_object_types = 0; +} + +void +initialize_virtual_object_available_slots() { + AVAILABLE_SLOT_INITIALIZATION +} + +void +deinitialize_virtual_object_available_slots() { + PyMem_RawFree(AVAILABLE_SLOTS); + AVAILABLE_SLOTS = 0; +} + +#define MASK_SIZE (sizeof(unsigned char) * CHAR_BIT) + +int mask_count_ones(const unsigned char mask) { + unsigned char copy = mask; + int count = 0; + for (size_t i=0; i < MASK_SIZE; i++) { + count += copy & 1; + copy >>= 1; + } + return count; +} + +/* +The length of the mask may be less than the number +of slots available. +In that case blank_byte will be used as the continuation +of the mask. +*/ +PyType_Slot * +create_slot_list(const unsigned char *mask, size_t length) { + PyType_Slot *slots = 0; + int counter = 1; + for (size_t i = 0; i < length; i++) { + counter += mask_count_ones(mask[i]); + } + slots = PyMem_RawMalloc(sizeof(PyType_Slot) * counter); + const unsigned char *current_byte = mask + length - 1; + int i = 0, j = 0, k = 0; + const unsigned char blank_byte = 0; + + while (AVAILABLE_SLOTS[k].slot) { + if (*current_byte & (1 << j)) { + slots[i++] = AVAILABLE_SLOTS[k]; + } + j++; + k++; + if (j >= MASK_SIZE) { + j = 0; + if (k < MASK_SIZE * length) { + current_byte--; + } else { + current_byte = &blank_byte; + } + } + } + slots[i++] = final_slot; + return slots; +} + +static PyTypeObject * +create_new_virtual_object_type(const unsigned char *mask, size_t length) { + PyType_Slot *slots = create_slot_list(mask, length); PyType_Spec spec = { VirtualObjectTypeName, sizeof(VirtualPythonObject), @@ -261,12 +324,28 @@ initialize_virtual_object_type() { Py_TPFLAGS_DEFAULT | Py_TPFLAGS_HEAPTYPE, slots }; - VirtualPythonObject_Type = (PyTypeObject*) PyType_FromSpec(&spec); + PyTypeObject *result = (PyTypeObject*) PyType_FromSpec(&spec); + PyMem_RawFree(slots); + return result; } PyObject * -allocate_raw_virtual_object(JNIEnv *env, jobject object) { - VirtualPythonObject *result = PyObject_New(VirtualPythonObject, VirtualPythonObject_Type); +_allocate_raw_virtual_object(JNIEnv *env, jobject object, const unsigned char *mask, size_t length) { + PyObject *mask_as_number = _PyLong_FromByteArray(mask, length, 0, 0); + PyTypeObject *virtual_object_type = (PyTypeObject *) PyDict_GetItem(ready_virtual_object_types, mask_as_number); + if (!virtual_object_type) + virtual_object_type = create_new_virtual_object_type(mask, length); + if (!virtual_object_type) { + char err_str[200]; + sprintf(err_str, "Something went wrong in virtual object type creation"); + PyErr_SetString(PyExc_AssertionError, err_str); + return 0; + } + + PyDict_SetItem(ready_virtual_object_types, mask_as_number, (PyObject *)virtual_object_type); + Py_DECREF(mask_as_number); + + VirtualPythonObject *result = PyObject_New(VirtualPythonObject, virtual_object_type); if (!result) return 0; @@ -278,6 +357,27 @@ allocate_raw_virtual_object(JNIEnv *env, jobject object) { return (PyObject *) result; } +PyObject * +allocate_raw_virtual_object(JNIEnv *env, jobject object, jbyteArray mask) { + unsigned char *mask_as_char_array = (unsigned char *) (*env)->GetByteArrayElements(env, mask, 0); + const unsigned char *mask_as_array = (const unsigned char *) mask_as_char_array; + size_t mask_length = (*env)->GetArrayLength(env, mask); + PyObject *result = _allocate_raw_virtual_object(env, object, mask_as_array, mask_length); + (*env)->ReleaseByteArrayElements(env, mask, (jbyte*) mask_as_char_array, 0); + return result; +} + +// Since there are about 80 slots, a mask with 96 bits (12 bytes) in it +// should be enough to cover all of them +#define MAX_NEEDED_MASK_BYTE_NUMBER 12 + +PyObject * +allocate_raw_virtual_object_with_all_slots(JNIEnv *env, jobject object) { + const unsigned char all = 0b11111111; // This byte enables all 8 slots that сorrespond to it. + const unsigned char mask[MAX_NEEDED_MASK_BYTE_NUMBER] = {all, all, all, all, all, all, all, all, all, all, all, all}; + return _allocate_raw_virtual_object(env, object, mask, MAX_NEEDED_MASK_BYTE_NUMBER); +} + void finish_virtual_object_initialization(VirtualPythonObject *object, ConcolicContext *ctx, SymbolicAdapter *adapter) { object->ctx = ctx; @@ -286,7 +386,7 @@ finish_virtual_object_initialization(VirtualPythonObject *object, ConcolicContex PyObject * create_new_virtual_object(ConcolicContext *ctx, jobject object, SymbolicAdapter *adapter) { - VirtualPythonObject *result = (VirtualPythonObject *) allocate_raw_virtual_object(ctx->env, object); + VirtualPythonObject *result = (VirtualPythonObject *) allocate_raw_virtual_object_with_all_slots(ctx->env, object); finish_virtual_object_initialization(result, ctx, adapter); return (PyObject *) result; @@ -296,8 +396,8 @@ int is_virtual_object(PyObject *obj) { if (!obj) return 0; - return Py_TYPE(obj) == VirtualPythonObject_Type; -} + return strcmp(Py_TYPE(obj)->tp_name, VirtualObjectTypeName) == 0; // Temporary solution +} void register_virtual_methods(SymbolicAdapter *adapter) { adapter->virtual_tp_richcompare = tp_richcompare; diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/VirtualObjectsTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/VirtualObjectsTest.kt new file mode 100644 index 0000000000..1477e3e4d1 --- /dev/null +++ b/usvm-python/src/test/kotlin/org/usvm/samples/VirtualObjectsTest.kt @@ -0,0 +1,174 @@ +package org.usvm.samples + +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.BeforeAll +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import org.usvm.annotations.ids.SlotId +import org.usvm.annotations.ids.setSlotBit +import org.usvm.machine.interpreters.concrete.ConcretePythonInterpreter +import org.usvm.machine.interpreters.concrete.PyObject +import org.usvm.machine.interpreters.concrete.utils.VirtualPythonObject + +class VirtualObjectsTest { + companion object { + val slotMethods: Map Boolean> = mapOf( + SlotId.NbBool to ConcretePythonInterpreter.typeHasNbBool, + SlotId.NbAdd to ConcretePythonInterpreter.typeHasNbAdd, + SlotId.NbSubtract to ConcretePythonInterpreter.typeHasNbSubtract, + SlotId.NbMultiply to ConcretePythonInterpreter.typeHasNbMultiply, + SlotId.NbMatrixMultiply to ConcretePythonInterpreter.typeHasNbMatrixMultiply, + SlotId.NbNegative to ConcretePythonInterpreter.typeHasNbNegative, + SlotId.NbPositive to ConcretePythonInterpreter.typeHasNbPositive, + SlotId.SqLength to ConcretePythonInterpreter.typeHasSqLength, + SlotId.SqConcat to ConcretePythonInterpreter.typeHasSqConcat, + SlotId.MpSubscript to ConcretePythonInterpreter.typeHasMpSubscript, + SlotId.MpAssSubscript to ConcretePythonInterpreter.typeHasMpAssSubscript, + SlotId.TpRichcompare to ConcretePythonInterpreter.typeHasTpRichcmp, + SlotId.TpGetattro to ConcretePythonInterpreter.typeHasTpGetattro, + SlotId.TpSetattro to ConcretePythonInterpreter.typeHasTpSetattro, + SlotId.TpIter to ConcretePythonInterpreter.typeHasTpIter, + SlotId.TpCall to ConcretePythonInterpreter.typeHasTpCall, + SlotId.TpHash to ConcretePythonInterpreter.typeHasTpHash + ) + } + + fun checkSlotDisabling( + slotId: SlotId, + ): Boolean? { + val obj = VirtualPythonObject(-1 - slotId.ordinal) + obj.slotMask.setSlotBit(slotId, false) + val pyObj = ConcretePythonInterpreter.allocateVirtualObject(obj) + val type = ConcretePythonInterpreter.getPythonObjectType(pyObj) + val method = slotMethods[slotId] ?: return null + return !method(type) + } + + @Test + fun testAllEnabled() { + val obj = VirtualPythonObject(-1) + val pyObj = ConcretePythonInterpreter.allocateVirtualObject(obj) + val type = ConcretePythonInterpreter.getPythonObjectType(pyObj) + var result = true + for (method in slotMethods.values) { + if (!method(type)) { + result = false + break + } + } + assertTrue(result) + } + + @Test + fun testNbBoolDisabled() { + val result = checkSlotDisabling(SlotId.NbBool) ?: return + assertTrue(result) + } + + @Test + fun testNbAddDisabled() { + val result = checkSlotDisabling(SlotId.NbAdd) ?: return + assertTrue(result) + } + + @Test + fun testNbSubtractDisabled() { + val result = checkSlotDisabling(SlotId.NbSubtract) ?: return + assertTrue(result) + } + + @Test + fun testNbMultiplyDisabled() { + val result = checkSlotDisabling(SlotId.NbMultiply) ?: return + assertTrue(result) + } + + @Test + fun testNbMatrixMultiplyDisabled() { + val result = checkSlotDisabling(SlotId.NbMatrixMultiply) ?: return + assertTrue(result) + } + + @Test + fun testNbNegativeDisabled() { + val result = checkSlotDisabling(SlotId.NbNegative) ?: return + assertTrue(result) + } + + @Test + fun testNbPositiveDisabled() { + val result = checkSlotDisabling(SlotId.NbPositive) ?: return + assertTrue(result) + } + + @Test + fun testSqLengthDisabled() { + val result = checkSlotDisabling(SlotId.SqLength) ?: return + assertTrue(result) + } + + @Test + fun testSqConcatDisabled() { + val result = checkSlotDisabling(SlotId.SqConcat) ?: return + assertTrue(result) + } + + @Test + fun testMpSubscriptDisabled() { + val result = checkSlotDisabling(SlotId.MpSubscript) ?: return + assertTrue(result) + } + + @Test + fun testMpAssSubscriptDisabled() { + val result = checkSlotDisabling(SlotId.MpAssSubscript) ?: return + assertTrue(result) + } + + @Test + fun testTpRichcompareDisabled() { + /* + * Check that attempt to disable tp_hash does not + * interfere with disabling tp_richcompare. + */ + val obj = VirtualPythonObject(-1 - SlotId.TpRichcompare.ordinal) + obj.slotMask.setSlotBit(SlotId.TpRichcompare, false).setSlotBit(SlotId.TpHash, false) + val pyObj = ConcretePythonInterpreter.allocateVirtualObject(obj) + val type = ConcretePythonInterpreter.getPythonObjectType(pyObj) + val checkTpRichCompare = slotMethods[SlotId.TpRichcompare] ?: return + val checkTpHash = slotMethods[SlotId.TpHash] ?: return + assertFalse(checkTpRichCompare(type)) + assertTrue(checkTpHash(type)) // hash cannot be disabled + } + + @Test + fun testTpGetattroDisabled() { + val result = checkSlotDisabling(SlotId.TpGetattro) ?: return + assertFalse(result) // tp_getattro is marked as mandatory + } + + @Test + fun testTpSetattroDisabled() { + val result = checkSlotDisabling(SlotId.TpSetattro) ?: return + assertFalse(result) // tp_setattro is marked as mandatory + } + + @Test + fun testTpIterDisabled() { + val result = checkSlotDisabling(SlotId.TpIter) ?: return + assertTrue(result) + } + + @Test + fun testTpCallDisabled() { + val result = checkSlotDisabling(SlotId.TpCall) ?: return + assertTrue(result) + } + + @Test + fun testTpHashDisabled() { + val result = checkSlotDisabling(SlotId.TpHash) ?: return + assertFalse(result) // tp_hash is marked as mandatory + } +} \ No newline at end of file diff --git a/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/SymbolicMethodProcessor.kt b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/SymbolicMethodProcessor.kt index 74b0bf2121..8bd07bfe89 100644 --- a/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/SymbolicMethodProcessor.kt +++ b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/SymbolicMethodProcessor.kt @@ -2,6 +2,7 @@ package org.usvm.annotations import org.usvm.annotations.codegeneration.generateSymbolicMethod import org.usvm.annotations.codegeneration.generateSymbolicMethodInitialization +import org.usvm.annotations.codegeneration.generateAvailableSlotInitialization import org.usvm.annotations.ids.SymbolicMethodId import java.io.File import javax.annotation.processing.AbstractProcessor @@ -33,6 +34,11 @@ class SymbolicMethodProcessor : AbstractProcessor() { val file = File(headerPath, "SymbolicMethods.h") file.writeText(init + "\n\n" + functionsCode) file.createNewFile() + // Temporary, available slots are generated here + val slotsInit = generateAvailableSlotInitialization() + val file2 = File(headerPath, "AvailableSlots.h") + file2.writeText(slotsInit) + file2.createNewFile() return true } diff --git a/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/codegeneration/AvailableSlotGeneration.kt b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/codegeneration/AvailableSlotGeneration.kt new file mode 100644 index 0000000000..1cf05f4712 --- /dev/null +++ b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/codegeneration/AvailableSlotGeneration.kt @@ -0,0 +1,19 @@ +package org.usvm.annotations.codegeneration + +import org.usvm.annotations.ids.SlotId + +fun generateAvailableSlotInitialization(): String { + val size = SlotId.entries.size + val prefix = """ + AVAILABLE_SLOTS = PyMem_RawMalloc(sizeof(PyType_Slot) * ${size + 1}); + """.trimIndent() + val items = SlotId.entries.map { + requireNotNull(it.slotName) + "AVAILABLE_SLOTS[${it.getMaskBit()}] = Virtual_${it.slotName};".trimIndent() + } + val postfix = "AVAILABLE_SLOTS[$size] = final_slot;" + return "#define AVAILABLE_SLOT_INITIALIZATION \\\n" + + prefix.replace("\n", "\\\n") + "\\\n" + + items.joinToString("\n").replace("\n", "\\\n") + "\\\n" + + postfix.replace("\n", "\\\n") + "\n" +} diff --git a/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/ids/SlotId.kt b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/ids/SlotId.kt new file mode 100644 index 0000000000..617371a1b4 --- /dev/null +++ b/usvm-python/usvm-python-annotations/src/main/kotlin/org/usvm/annotations/ids/SlotId.kt @@ -0,0 +1,52 @@ +package org.usvm.annotations.ids + +/* + * tp_hash cannot be disabled, however + * if you don't explicitly specify that the type HAS that slot, + * you will not be able to disable the tp_richcompare slot + * + * For that reason, some slots are marked as mandatory. + * They cannot be disabled using mask, so they do not have + * a mask bit number. + * + * The usage of swapSlotBit or setSlotBit with these slots + * will not have any effect on the mask. + */ +enum class SlotId( + val slotName: String, + val mandatory: Boolean = false, +) { + TpGetattro("tp_getattro", true), + TpSetattro("tp_setattro", true), + TpRichcompare("tp_richcompare"), + TpIter("tp_iter"), + TpHash("tp_hash", true), + TpCall("tp_call"), + TpDealloc("tp_dealloc", true), + NbBool("nb_bool"), + NbAdd("nb_add"), + NbSubtract("nb_subtract"), + NbMultiply("nb_multiply"), + NbMatrixMultiply("nb_matrix_multiply"), + NbNegative("nb_negative"), + NbPositive("nb_positive"), + SqLength("sq_length"), + MpSubscript("mp_subscript"), + MpAssSubscript("mp_ass_subscript"), + SqConcat("sq_concat"), + ; + fun getMaskBit(): Int = ordinal +} + +fun ByteArray.setSlotBit(slot: SlotId, state: Boolean): ByteArray { + if (slot.mandatory) return this + val bitPosition = this.size * Byte.SIZE_BITS - 1 - slot.getMaskBit() + val byteIndex = bitPosition / Byte.SIZE_BITS + val bitMask = 1 shl (slot.getMaskBit() % Byte.SIZE_BITS) + if (state) { + this[byteIndex] = (this[byteIndex].toInt() or bitMask).toByte() + } else { + this[byteIndex] = (this[byteIndex].toInt() and (bitMask.inv())).toByte() + } + return this // just to allow Builder-like usage +} diff --git a/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java b/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java index 867e2e4736..1ebc097479 100644 --- a/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java +++ b/usvm-python/usvm-python-main/src/main/java/org/usvm/interpreter/CPythonAdapter.java @@ -76,7 +76,8 @@ public class CPythonAdapter { public native String getNameOfPythonType(long type); public static native int getInstructionFromFrame(long frameRef); public static native long getCodeFromFrame(long frameRef); - public native long allocateVirtualObject(VirtualPythonObject object); + public native long allocateRawVirtualObjectWithAllSlots(VirtualPythonObject object); + public native long allocateRawVirtualObject(VirtualPythonObject object, byte[] mask); public native long makeList(long[] elements); public native long allocateTuple(int size); public native void setTupleElement(long tuple, int index, long element); diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt index c4a22560f3..ccc1a3bd2f 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/ConcretePythonInterpreter.kt @@ -162,7 +162,22 @@ object ConcretePythonInterpreter { } fun allocateVirtualObject(virtualObject: VirtualPythonObject): PyObject { - val ref = pythonAdapter.allocateVirtualObject(virtualObject) + /* + * Usage example: + * pythonAdapter.allocateRawVirtualObject(virtualObject, mask), where + * Mask is a sequence of bits, written in the reverse order and + * packed into a ByteArray + * (ABCDEFGHIJ -> {000000JI, HGFEDCBA}) + * So, THE LAST bit in the ByteArray (A) enables THE FIRST slot from the list. + * + * pythonAdapter.allocateRawVirtualObjectWithAllSlots(object) does exactly the same as + * pythonAdapter.allocateRawVirtualObject(virtualObject, List(12) {0b11111111.toByte()}.toByteArray()) + * + * In order to manually enable/disable some slots, use swapSlotBit or setSlotBit: + * pythonAdapter.allocateRawVirtualObject(obj, obj.slotMask.swapSlotBit(SlotId.NbAdd)) + * pythonAdapter.allocateRawVirtualObject(obj, obj.slotMask.setSlotBit(SlotId.NbAdd, false)) + */ + val ref = pythonAdapter.allocateRawVirtualObject(virtualObject, virtualObject.slotMask) if (ref == 0L) { throw CPythonExecutionException() } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/utils/VirtualPythonObject.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/utils/VirtualPythonObject.kt index cfb68e487a..e66db94723 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/utils/VirtualPythonObject.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/concrete/utils/VirtualPythonObject.kt @@ -1,6 +1,10 @@ package org.usvm.machine.interpreters.concrete.utils +private const val MAX_NEEDED_MASK_BYTE_NUMBER: Int = 12 +private const val ALL_SLOTS_BYTE: Int = 0b11111111 + class VirtualPythonObject( @JvmField val interpretedObjRef: Int, + val slotMask: ByteArray = List(MAX_NEEDED_MASK_BYTE_NUMBER) { ALL_SLOTS_BYTE.toByte() }.toByteArray(), )