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.

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

Sygus2 #2016

Closed
wants to merge 8 commits into from
Closed

Sygus2 #2016

wants to merge 8 commits into from

Conversation

andreistefanescu
Copy link
Contributor

No description provided.

yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym)
_ <- W4.setOpt yicesTimeoutSetting timeout

auxOutSetting <- W4.getOptionSetting solverInteractionFile (W4.getConfiguration sym)
_ <- W4.setOpt auxOutSetting $ Text.pack "foo.smt2"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for debugging; expose as a setting to show how crucible and saw are interacting

return (SomeOnlineBackend (bak :: Backend Yices.Connection))

newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout =
do bak <- newOnlineBackend sym (SMT2.defaultFeatures Z3.Z3)
W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

addz3 addz3 is a failure in the second, but no addz3 is a failure. This adds the backend-support for all solvers to allow flexibility in invoking them as alternatives during the analysis.

(invSubst, loopFunEquivConds) <- liftIO $ case maybe_ref of
Just fixpoint_state_ref -> do
uninterp_inv_fns <- Crucible.LLVM.Fixpoint.executionFeatureContextInvPreds <$> readIORef fixpoint_state_ref
subst <- C.runCHC bak uninterp_inv_fns
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

get the result of the inference for the invariant predicate, which is then checked for equivalence to the state from the fixpoint evaluation


setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func =
Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar fixpoint_func
setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Crucible only understands what4, not saw-core, so this function: takes the what4-internals inputs, converts to saw-core, evaluates the results, then converts back to what4. This is used because saw-core is NOT a dependency of crucible, and therefore crucible is not capable of performing the saw-core concepts here.

TopLevel (SolverStats, [MS.VCStats])
checkGoals bak opts nm sc tactic mdMap = do
gs <- liftIO $ getPoststateObligations sc bak mdMap
checkGoals bak opts nm loc sc tactic mdMap invSubst loopFunEquivConds = do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now need to verify both the invSubst, but also any loopFunEquivConds

@RyanGlScott RyanGlScott mentioned this pull request Jan 24, 2024
@RyanGlScott
Copy link
Contributor

Superseded by #2037.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants