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

Jump to bottom

implementation of #87 #88

Merged
merged 1 commit into from
Jul 18, 2023
Merged

implementation of #87 #88

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
14 changes: 8 additions & 6 deletions kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ import org.vorpal.research.kex.state.transformer.collectVariables
import org.vorpal.research.kex.state.transformer.getConstStringMap
import org.vorpal.research.kex.state.transformer.memspace
import org.vorpal.research.kex.util.kapitalize
import org.vorpal.research.kex.util.with
import org.vorpal.research.kthelper.assert.ktassert
import org.vorpal.research.kthelper.assert.unreachable
import org.vorpal.research.kthelper.logging.debug
Expand Down Expand Up @@ -657,13 +658,14 @@ class KSMTSolver(
val converter = KSMTConverter(executionContext)
val ksmtState = converter.convert(state, ef, ctx)
val ksmtQueries = queries.map { (hard, soft) ->
converter.convert(hard, ef, ctx) to soft.map { converter.convert(it, ef, ctx) }
val ctxCopy = KSMTContext(ctx)
Triple(converter.convert(hard, ef, ctx), soft.map { converter.convert(it, ef, ctx) }, ctxCopy)
}

log.debug("Check started")
val results = checkIncremental(ksmtState, ksmtQueries)
log.debug("Check finished")
results.mapIndexed { index, (status, any) ->
results.mapIndexed { index, (status, any, ctx) ->
when (status) {
KSolverStatus.UNSAT -> Result.UnsatResult
KSolverStatus.UNKNOWN -> Result.UnknownResult(any as String)
Expand Down Expand Up @@ -698,8 +700,8 @@ class KSMTSolver(

private suspend fun checkIncremental(
state: Bool_,
queries: List<Pair<Bool_, List<Bool_>>>
): List<Pair<KSolverStatus, Any>> = buildSolver().use { solver ->
queries: List<Triple<Bool_, List<Bool_>, KSMTContext>>
): List<Triple<KSolverStatus, Any, KSMTContext>> = buildSolver().use { solver ->
solver.assertAndTrackAsync(
state.asAxiom() as KExpr<KBoolSort>,
ef.ctx.mkConstDecl("State", ef.ctx.boolSort)
Expand All @@ -710,7 +712,7 @@ class KSMTSolver(
)
solver.push()

return queries.map { (hardConstraints, softConstraints) ->
return queries.map { (hardConstraints, softConstraints, ctx) ->
solver.assertAndTrackAsync(
hardConstraints.asAxiom() as KExpr<KBoolSort>,
ef.ctx.mkConstDecl("HardConstraints", ef.ctx.boolSort)
Expand Down Expand Up @@ -760,7 +762,7 @@ class KSMTSolver(
solver.pop()
}
solver.push()
}
}.with(ctx)
}
}

Expand Down
67 changes: 67 additions & 0 deletions kex-ksmt/src/test/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolverTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,13 +12,15 @@ import org.ksmt.sort.KBoolSort
import org.vorpal.research.kex.ExecutionContext
import org.vorpal.research.kex.KexTest
import org.vorpal.research.kex.ktype.KexInt
import org.vorpal.research.kex.ktype.KexString
import org.vorpal.research.kex.random.StubRandomizer
import org.vorpal.research.kex.smt.Result
import org.vorpal.research.kex.smt.ksmt.KSMTEngine.asExpr
import org.vorpal.research.kex.state.PredicateQuery
import org.vorpal.research.kex.state.basic
import org.vorpal.research.kex.state.predicate.path
import org.vorpal.research.kex.state.term.term
import org.vorpal.research.kex.util.StringInfoContext
import org.vorpal.research.kfg.ClassManager
import kotlin.test.Test
import kotlin.test.assertEquals
Expand Down Expand Up @@ -277,5 +279,70 @@ class KSMTSolverTest : KexTest("ksmt-solver") {
assertIs<Result.SatResult>(results[2])
assertIs<Result.SatResult>(results[3])
}

@Test
fun testIncrementalMemory() {
with(object : StringInfoContext {}) {
val string = term { generate(KexString()) }
val charArray = term { generate(valueArrayType) }

val state = basic {
state { charArray.initializeNew(3, 'a', 'b', 'c') }
state { string.new() }
state { string.field(valueArrayType, valueArrayName).store(const(null)) }
}

val paths = mutableListOf(
PredicateQuery(
basic {
state { string.field(valueArrayType, valueArrayName).store(charArray) }
val field = term { generate(valueArrayType) }
state { field equality string.field(valueArrayType, valueArrayName).load() }
path { field.length() equality 3 }
path { field[0].load() equality 'a' }
}
),
PredicateQuery(
basic {
val field = term { generate(valueArrayType) }
val loaded = term { generate(valueArrayType) }
state { field.new(10) }
state { field[0].store(const('0')) }
state { string.field(valueArrayType, valueArrayName).store(field) }
state { loaded equality string.field(valueArrayType, valueArrayName).load() }
path { loaded.length() equality 10 }
path { loaded[0].load() equality '0' }
}
),
PredicateQuery(
basic {
path { string.field(valueArrayType, valueArrayName).load() equality null }
}
),
PredicateQuery(
basic {
val loaded = term { generate(valueArrayType) }
state { loaded equality string.field(valueArrayType, valueArrayName) }
path { loaded equality charArray }
}
),
)

val solver = KSMTSolver(
ExecutionContext(
ClassManager(),
this.javaClass.classLoader,
StubRandomizer(),
emptyList()
)
)

val results = solver.isSatisfiable(state, paths)
assertIs<Result.SatResult>(results[0])
assertIs<Result.SatResult>(results[1])
assertIs<Result.SatResult>(results[2])
assertIs<Result.UnsatResult>(results[3])
}
}
}

Loading