Skip to content

Commit af207a4

Browse files
committed
small fix
1 parent d3b3a68 commit af207a4

File tree

2 files changed

+18
-7
lines changed

2 files changed

+18
-7
lines changed

usvm-python/src/test/kotlin/manualTest.kt

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,9 @@ private fun buildSampleRunConfig(): RunConfig {
5757
return RunConfig(program, typeSystem, functions)
5858
}
5959

60-
private val ignoreFunctions = listOf<String>()
60+
private val ignoreFunctions = listOf<String>(
61+
"get_transitions"
62+
)
6163
private val ignoreModules = listOf<String>(
6264
"odd_even_transposition_parallel"
6365
)
@@ -74,10 +76,10 @@ private fun getFunctionInfo(
7476
return null
7577
if (ignoreFunctions.contains(name))
7678
return null
77-
if (module != "viterbi")
78-
return null
79-
//if (name != "RedBlackTree.insert")
80-
// return null
79+
// if (module != "markov_chain")
80+
// return null
81+
// if (name != "get_transitions")
82+
// return null
8183
if (description.argumentKinds.any { it == PythonCallableTypeDescription.ArgKind.ARG_STAR || it == PythonCallableTypeDescription.ArgKind.ARG_STAR_2 })
8284
return null
8385
runCatching {
@@ -109,7 +111,7 @@ private fun getFunctionInfo(
109111
*/
110112

111113
private fun buildProjectRunConfig(): RunConfig {
112-
val projectPath = "D:\\projects\\Python\\dynamic_programming"
114+
val projectPath = "D:\\projects\\Python\\graphs"
113115
val mypyRoot = "D:\\projects\\mypy_tmp"
114116
val files = getPythonFilesFromRoot(projectPath)
115117
val modules = getModulesFromFiles(projectPath, files)

usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/symbolicobjects/ConverterToPythonObject.kt

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ package org.usvm.machine.symbolicobjects
33
import io.ksmt.expr.KInt32NumExpr
44
import org.usvm.*
55
import org.usvm.api.readArrayIndex
6+
import org.usvm.api.typeStreamOf
67
import org.usvm.language.PythonCallable
78
import org.usvm.language.VirtualPythonObject
89
import org.usvm.language.types.*
@@ -14,6 +15,7 @@ import org.usvm.machine.utils.DefaultValueProvider
1415
import org.usvm.machine.utils.MAX_INPUT_ARRAY_LENGTH
1516
import org.usvm.machine.utils.PyModelHolder
1617
import org.usvm.memory.UMemory
18+
import org.usvm.types.first
1719

1820
class ConverterToPythonObject(
1921
private val ctx: UPythonContext,
@@ -119,7 +121,14 @@ class ConverterToPythonObject(
119121
) as UConcreteHeapRef
120122
if (element.address == 0 && forcedConcreteTypes[element] == null)
121123
numberOfUsagesOfVirtualObjects += 1
122-
val elemInterpretedObject = InterpretedInputSymbolicPythonObject(element, obj.modelHolder, typeSystem)
124+
val elemInterpretedObject =
125+
if (isStaticHeapRef(element)) {
126+
val type = memory.typeStreamOf(element).first()
127+
require(type is ConcretePythonType)
128+
InterpretedAllocatedOrStaticSymbolicPythonObject(element, type, typeSystem)
129+
} else {
130+
InterpretedInputSymbolicPythonObject(element, obj.modelHolder, typeSystem)
131+
}
123132
convert(elemInterpretedObject)
124133
}
125134
}

0 commit comments

Comments
 (0)