-
Notifications
You must be signed in to change notification settings - Fork 18
/
viper.scala
132 lines (111 loc) · 4.53 KB
/
viper.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
package gapt.testing
import gapt.expr.Expr
import gapt.expr.formula.hol.{ containsQuantifier, isExtendedAtom }
import gapt.expr.formula.{ All, Formula, Imp }
import gapt.utils._
import scala.concurrent.duration._
import gapt.formats.tip.TipSmtImporter
import gapt.proofs.context.Context
import gapt.proofs.expansion.ExpansionProofToLK
import gapt.proofs.lk.LKProof
import gapt.proofs.lk.rules.InductionRule
import gapt.proofs.lk.transformations.{ LKToExpansionProof, cleanStructuralRules }
import gapt.proofs.lk.util.extractInductionAxioms
import gapt.provers.viper.aip.axioms.{ IndependentInductionAxioms, SequentialInductionAxioms }
import gapt.provers.viper.spin.SpinOptions
import gapt.provers.viper.{ AipOptions, Viper, ViperOptions }
object parseMode {
def apply( modeName: String ): ViperOptions = modeName match {
case "analytic_sequential" => ViperOptions( mode = "analytic", aipOptions = AipOptions( axioms = SequentialInductionAxioms() ) )
case "analytic_independent" => ViperOptions( mode = "analytic", aipOptions = AipOptions( axioms = IndependentInductionAxioms() ) )
case "treegrammar" => ViperOptions( mode = "treegrammar" )
case "spin" => ViperOptions( mode = "spin" )
case "spin_nogen" => ViperOptions( mode = "spin", spinOptions = SpinOptions( performGeneralization = false ) )
case "spin_notest" => ViperOptions( mode = "spin", spinOptions = SpinOptions( sampleTestTerms = 0 ) )
}
}
object testViper extends App {
def countInductions( prf: LKProof ): ( Int, Int ) = {
val ( n, d ) = prf.immediateSubProofs.map( countInductions ).foldLeft( ( 0, 0 ) ) {
case ( ( n1, d1 ), ( n2, d2 ) ) => ( n1 + n2, d1 max d2 )
}
prf match {
case InductionRule( _, _, _ ) => ( n + 1, d + 1 )
case _ => ( n, d )
}
}
// This turns the cuts into induction inferences
def cleanProof( prf: LKProof )( implicit ctx: Context ): LKProof = {
val prf1 = cleanStructuralRules( prf )
val expPrf = LKToExpansionProof( prf1 )( ctx )
ExpansionProofToLK( expPrf )( ctx ).toOption.get
}
def removeOuterAlls( e: Expr ): Expr =
e match {
case All( _, e1 ) => removeOuterAlls( e1 )
case _ => e
}
def inductionTarget( e: Expr ): Expr =
removeOuterAlls( e ) match {
case Imp( _, e1 ) => removeOuterAlls( e1 )
}
val logger = Logger( "testViper" )
val ( fileName, mode ) =
( args.toList: @unchecked ) match {
case Seq( f, m ) => ( f, m )
}
val metricsPrinter = new MetricsPrinter
LogHandler.current.value = metricsPrinter
logger.metric( "file", fileName )
logger.metric( "mode", mode )
logger.time( "total" ) {
val problem = try logger.time( "parse" ) {
TipSmtImporter.fixupAndLoad( fileName )
} catch {
case e: Throwable =>
logger.metric( "status", e match {
case _: OutOfMemoryError => "parsing_out_of_memory"
case _: StackOverflowError => "parsing_stack_overflow"
case _: Throwable => "parsing_other_exception"
} )
logger.metric( "exception", e.toString )
throw e
}
val options = parseMode( mode )
var prf: Option[LKProof] = None
try logger.time( "viper" ) {
withTimeout( 120 seconds ) {
Viper( problem, options ) match {
case Some( prf1 ) =>
logger.metric( "status", "ok" )
prf = Some( prf1 )
case None => logger.metric( "status", "saturated" )
}
}
} catch {
case e: Throwable =>
logger.metric( "status", e match {
case _: OutOfMemoryError => "viper_out_of_memory"
case _: StackOverflowError => "viper_stack_overflow"
case _: TimeOutException => "viper_timeout"
case _: Throwable => "viper_other_exception"
} )
logger.metric( "exception", e.toString )
throw e
}
prf match {
case None =>
case Some( prf1 ) =>
val prf2 = cleanProof( prf1 )( problem.context )
val ( inds, depth ) = countInductions( prf2 )
logger.metric( "inductions", inds )
logger.metric( "induction_depth", depth )
val axs = extractInductionAxioms( prf2 )( problem.context )
val targets = axs.map( inductionTarget )
val atomic = targets.count( e => isExtendedAtom( e.asInstanceOf[Formula] ) )
val quantified = targets.count( e => containsQuantifier( e.asInstanceOf[Formula] ) )
logger.metric( "atomic", atomic )
logger.metric( "quantified", quantified )
}
}
}