|
| 1 | +package org.usvm |
| 2 | + |
| 3 | +import kotlinx.serialization.SerialName |
| 4 | +import kotlinx.serialization.Serializable |
| 5 | +import kotlinx.serialization.encodeToString |
| 6 | +import kotlinx.serialization.json.Json |
| 7 | +import org.usvm.gameserver.GameMap |
| 8 | +import org.usvm.gameserver.GameOver |
| 9 | +import org.usvm.gameserver.GameState |
| 10 | +import org.usvm.gameserver.Searcher |
| 11 | +import org.usvm.gameserver.serialization.createGameState |
| 12 | +import org.usvm.runner.JavaMethodRunner |
| 13 | +import org.usvm.runner.defaultOptions |
| 14 | +import org.usvm.statistics.BasicBlock |
| 15 | +import org.usvm.utils.AIGameStep |
| 16 | +import org.usvm.utils.Mode |
| 17 | +import org.usvm.utils.OnnxModelImpl |
| 18 | +import java.io.File |
| 19 | +import java.net.Socket |
| 20 | +import java.nio.file.Paths |
| 21 | +import kotlin.math.floor |
| 22 | +import kotlin.time.Duration |
| 23 | +import kotlin.time.Duration.Companion.seconds |
| 24 | +import kotlin.time.DurationUnit |
| 25 | + |
| 26 | +@Serializable |
| 27 | +data class AIGameStepSerializable( |
| 28 | + @SerialName("GameState") val GameState: GameState, @SerialName("Output") val NNOutput: Array<FloatArray> |
| 29 | +) { |
| 30 | + // autogenerated |
| 31 | + override fun equals(other: Any?): Boolean { |
| 32 | + if (this === other) return true |
| 33 | + if (javaClass != other?.javaClass) return false |
| 34 | + |
| 35 | + other as AIGameStepSerializable |
| 36 | + |
| 37 | + if (GameState != other.GameState) return false |
| 38 | + if (!NNOutput.contentDeepEquals(other.NNOutput)) return false |
| 39 | + |
| 40 | + return true |
| 41 | + } |
| 42 | + |
| 43 | + override fun hashCode(): Int { |
| 44 | + var result = GameState.hashCode() |
| 45 | + result = 31 * result + NNOutput.contentDeepHashCode() |
| 46 | + return result |
| 47 | + } |
| 48 | +} |
| 49 | + |
| 50 | +fun sendModelRunner( |
| 51 | + port: Int, |
| 52 | + stepsToPlay: Int, |
| 53 | + stepsToStart: Int, |
| 54 | + defaultSearcher: Searcher, |
| 55 | + assemblyFullName: String, |
| 56 | + nameOfObjectToCover: String, |
| 57 | + mapName: String, |
| 58 | + outFolder: String, |
| 59 | + model: String, |
| 60 | + useGPU: Boolean |
| 61 | +) { |
| 62 | + val gameMap = GameMap( |
| 63 | + stepsToPlay = stepsToPlay.toUInt(), |
| 64 | + stepsToStart = stepsToStart.toUInt(), |
| 65 | + defaultSearcher = defaultSearcher, |
| 66 | + assemblyFullName = assemblyFullName, |
| 67 | + nameOfObjectToCover = nameOfObjectToCover, |
| 68 | + mapName = mapName |
| 69 | + ) |
| 70 | + |
| 71 | + val (gameOver, gameSteps) = sendModelExplorer(model, if (useGPU) Mode.GPU else Mode.CPU, gameMap) |
| 72 | + println("Running for ${gameMap.mapName} finished with coverage ${gameOver.percent}, tests ${gameOver.test}, steps ${gameOver.stepsCount}, errors ${gameOver.error}.") |
| 73 | + |
| 74 | + // lets save the results |
| 75 | + val directory = File(outFolder) |
| 76 | + if (!directory.exists()) { |
| 77 | + directory.mkdirs() |
| 78 | + } |
| 79 | + val serializedGameOver = "${gameOver.percent} ${gameOver.test} ${gameOver.stepsCount} ${gameOver.error}" |
| 80 | + val outFile = Paths.get(outFolder, "${gameMap.mapName}result") |
| 81 | + File(outFile.toString()).writeText(serializedGameOver) |
| 82 | + |
| 83 | + // send steps to the client if needed |
| 84 | + val needToSendSteps = Socket("localhost", port).let { socket -> |
| 85 | + val inputStream = socket.getInputStream() |
| 86 | + val buffer = ByteArray(1) |
| 87 | + val bytesRead = inputStream.read(buffer) |
| 88 | + if (bytesRead == -1) { |
| 89 | + throw RuntimeException("No data received from port=$port") |
| 90 | + } |
| 91 | + buffer[0].toInt() != 0 |
| 92 | + } |
| 93 | + |
| 94 | + if (!needToSendSteps) { |
| 95 | + return |
| 96 | + } |
| 97 | + val stepsFile = Paths.get(outFolder, "${gameMap.mapName}_steps") |
| 98 | + val gameStepsString = Json { }.encodeToString(gameSteps) |
| 99 | + File(stepsFile.toString()).writeText(gameStepsString) |
| 100 | +} |
| 101 | + |
| 102 | + |
| 103 | +fun sendModelExplorer( |
| 104 | + model: String, |
| 105 | + mode: Mode, |
| 106 | + gameMap: GameMap, |
| 107 | +): Pair<GameOver, ArrayList<AIGameStepSerializable>> { |
| 108 | + val steps = ArrayList<AIGameStepSerializable>() |
| 109 | + fun <Block : BasicBlock> saveStep(aiGameStep: AIGameStep<Block>) { |
| 110 | + val gameState = createGameState(aiGameStep.Game) |
| 111 | + val gameStep = AIGameStepSerializable(gameState.copy(), aiGameStep.NNOutput) |
| 112 | + steps.add(gameStep) |
| 113 | + } |
| 114 | + |
| 115 | + val runner = JavaMethodRunner( |
| 116 | + defaultOptions.copy( |
| 117 | + oracle = OnnxModelImpl( |
| 118 | + model, |
| 119 | + mode, |
| 120 | + true, |
| 121 | + ::saveStep, |
| 122 | + ), |
| 123 | + stepLimit = (gameMap.stepsToPlay + gameMap.stepsToStart).toULong(), |
| 124 | + timeout = (30 * 60).seconds, |
| 125 | + stepsToStart = (gameMap.stepsToPlay + gameMap.stepsToStart) |
| 126 | + ), |
| 127 | + classpath = gameMap.assemblyFullName, |
| 128 | + ) |
| 129 | + |
| 130 | + val (results, percentageCoverage) = runner.cover(gameMap.nameOfObjectToCover) |
| 131 | + val errors = results.count { it.isExceptional } |
| 132 | + val tests = results.size - errors |
| 133 | + |
| 134 | + return Pair( |
| 135 | + GameOver( |
| 136 | + floor(percentageCoverage).toUInt(), |
| 137 | + test = tests.toUInt(), |
| 138 | + stepsCount = gameMap.stepsToStart + gameMap.stepsToPlay, // TODO: send the actual step count |
| 139 | + error = errors.toUInt() |
| 140 | + ), steps |
| 141 | + ) |
| 142 | +} |
0 commit comments