Skip to content

Commit ca20a5a

Browse files
Yatin Manerkarpolgreen
Yatin Manerkar
authored and
polgreen
committed
Groups: Add the ability to pass groups as input parameters to modules
This commit required removing the extra "<rest of varname>__bound_input" variables that get created by ModuleInstantiatorPass.BoundInput. Doing so does not break any existing tests.
1 parent a17742d commit ca20a5a

File tree

7 files changed

+76
-24
lines changed

7 files changed

+76
-24
lines changed

‎src/main/resources/logback.xml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@
3535
<logger name="uclid.lang.VariableDependencyFinder" level="OFF"/>
3636
<logger name="uclid.lang.VerificationExpressionCheckerPass" level="OFF"/>
3737
<logger name="uclid.lang.VerificationExpressionPass" level="OFF"/>
38+
<logger name="uclid.lang.FiniteQuantsExpanderPass" level="OFF"/>
3839
<logger name="uclid.smt.Z3HornSolver" level="OFF"/>
3940
<logger name="uclid.smt.SExprLexical" level="OFF"/>
4041
<logger name="uclid.smt.SMTLIB2Base" level="OFF"/>

‎src/main/scala/uclid/lang/FiniteQuantsExpander.scala‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,11 @@
3939
package uclid
4040
package lang
4141

42+
import com.typesafe.scalalogging.Logger
43+
4244
class FiniteQuantsExpanderPass() extends RewritePass {
45+
lazy val logger = Logger(classOf[FiniteQuantsExpanderPass])
46+
4347
def expandFiniteQuant(id : Identifier, gId : Identifier, ctx : Scope, operands : List[Expr], isForall : Boolean) : Option[Expr] =
4448
{
4549
def flattenQuant(exprs : List[Expr], isForall : Boolean) : Expr =
@@ -81,10 +85,12 @@ class FiniteQuantsExpanderPass() extends RewritePass {
8185
//Get the elements of the group.
8286
ctx.map.get(gId) match {
8387
case Some(Scope.Group(_, _, elems)) =>
88+
logger.debug("Expanding over group %s".format(gId.toString))
8489
Some(flattenQuant(operands.map(expandFiniteQuantInner(id, elems, ctx, _, isForall)), isForall))
8590
//We're inside the define's specification, so no need to rewrite. Returning None will signal the parent to return the original opApp.
8691
case Some(Scope.FunctionArg(_, GroupType(_))) => None
87-
case _ => throw new Utils.RuntimeError("Could not find group %s".format(gId.toString))
92+
case None => throw new Utils.RuntimeError("Could not find group %s".format(gId.toString))
93+
case Some(s) => throw new Utils.RuntimeError("Group %s was matched to %s, which isn't a Group or a FunctionArg".format(gId.toString, s.toString))
8894
}
8995
}
9096

‎src/main/scala/uclid/lang/ModuleFlattener.scala‎

Lines changed: 20 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,8 @@ class ModuleDependencyFinder(mainModuleName : Identifier) extends ASTAnalyzer(
8080
}
8181

8282
object ModuleInstantiatorPass {
83-
sealed abstract class InstanceVarRenaming(val ident : Identifier, val typ : Type)
84-
case class BoundInput(id : Identifier, t : Type, expr : Expr) extends InstanceVarRenaming(id, t)
83+
sealed abstract class InstanceVarRenaming(val expr : Expr, val typ : Type)
84+
case class BoundInput(exp : Expr, t : Type) extends InstanceVarRenaming(exp, t)
8585
case class UnboundInput(id : Identifier, t : Type) extends InstanceVarRenaming(id, t)
8686
case class BoundOutput(lhs : Lhs, t : Type) extends InstanceVarRenaming(lhs.ident, t)
8787
case class UnboundOutput(id : Identifier, t : Type) extends InstanceVarRenaming(id, t)
@@ -111,11 +111,11 @@ object ModuleInstantiatorPass {
111111
}
112112
}
113113

114-
// Convert a RewriteMap into a VarMap
114+
// Convert a VarMap into a RewriteMap.
115115
def toRewriteMap(varMap : VarMap, instVarMap : InstVarMap) : RewriteMap = {
116116
val empty : RewriteMap = Map.empty
117117
val rewriteMap1 = varMap.foldLeft(empty) {
118-
(acc, mapping) => acc + (mapping._1 -> mapping._2.ident)
118+
(acc, mapping) => acc + (mapping._1 -> mapping._2.expr)
119119
}
120120
val rewriteMap2 = instVarMap.foldLeft(rewriteMap1) {
121121
(acc, mapping) => {
@@ -146,8 +146,11 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule
146146
// map each input
147147
val idMap1 = targetModule.inputs.foldLeft(idMap0) {
148148
(mapAcc, inp) => {
149+
logger.debug("inp is %s".format(inp.toString))
149150
inst.argMap.get(inp._1) match {
150-
case Some(expr) => mapAcc + (inp._1 -> MIP.BoundInput(NameProvider.get(inp._1.toString + "_bound_input"), inp._2, expr))
151+
case Some(expr) =>
152+
logger.debug("expr is %s".format(expr.toString))
153+
mapAcc + (inp._1 -> MIP.BoundInput(expr, inp._2))
151154
case None => mapAcc + (inp._1 -> MIP.UnboundInput(NameProvider.get(inp._1.toString + "_unbound_input"), inp._2))
152155
}
153156
}
@@ -192,11 +195,18 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule
192195
val instVarMap1 = varMap.foldLeft(Map.empty[List[Identifier], Identifier]) {
193196
(instVarMap, renaming) => {
194197
renaming._2 match {
195-
case MIP.BoundInput(_, _, _) | MIP.UnboundInput(_, _) |
198+
case MIP.BoundInput(_, _) =>
199+
if (renaming._2.expr.isInstanceOf[Identifier])
200+
{
201+
instVarMap + (List(inst.instanceId, renaming._1) -> renaming._2.expr.asInstanceOf[Identifier])
202+
}
203+
else
204+
instVarMap
205+
case MIP.UnboundInput(_, _) |
196206
MIP.BoundOutput(_, _) | MIP.UnboundOutput(_, _) |
197207
MIP.StateVariable(_, _) | MIP.SharedVariable(_, _) |
198208
MIP.Constant(_, _) =>
199-
instVarMap + (List(inst.instanceId, renaming._1) -> renaming._2.ident)
209+
instVarMap + (List(inst.instanceId, renaming._1) -> renaming._2.expr.asInstanceOf[Identifier])
200210
case _ =>
201211
instVarMap
202212
}
@@ -228,7 +238,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule
228238
varMap.map {
229239
v => {
230240
v._2 match {
231-
case MIP.BoundInput(id, t, _) => fixPosition(Some(StateVarsDecl(List(id), t)), id.position)
241+
case MIP.BoundInput(_, _) => None
232242
case MIP.UnboundOutput(id, t) => fixPosition(Some(StateVarsDecl(List(id), t)), id.position)
233243
case MIP.StateVariable(id, t) => fixPosition(Some(StateVarsDecl(List(id), t)), id.position)
234244
case MIP.Constant(id, t) => fixPosition(Some(ConstantsDecl(List(id), t)), id.position)
@@ -244,7 +254,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule
244254
v => {
245255
v._2 match {
246256
case MIP.UnboundInput(id, t) => fixPosition(Some(InputVarsDecl(List(id), t)), id.position)
247-
case MIP.BoundInput(_, _, _) | MIP.BoundOutput(_, _) |
257+
case MIP.BoundInput(_, _) | MIP.BoundOutput(_, _) |
248258
MIP.UnboundOutput(_, _) | MIP.StateVariable(_, _) |
249259
MIP.SharedVariable(_, _) | MIP.Constant(_, _) | MIP.Function(_, _) =>
250260
None
@@ -253,18 +263,7 @@ class ModuleInstantiatorPass(module : Module, inst : InstanceDecl, targetModule
253263
}.toList.flatten
254264
}
255265

256-
def createNextInputAssignments(varMap : VarMap) : List[Statement] = {
257-
varMap.map {
258-
v => {
259-
v._2 match {
260-
case MIP.BoundInput(id, _, expr) =>
261-
fixPosition(Some(AssignStmt(List(LhsId(id)), List(expr))), id.position)
262-
case _ =>
263-
None
264-
}
265-
}
266-
}.toList.flatten
267-
}
266+
def createNextInputAssignments(varMap : VarMap) : List[Statement] = { List() }
268267

269268
val (varMap, externalSymbolMap) = createVarMap()
270269
val targetInstVarMap = targetModule.getAnnotation[InstanceVarMapAnnotation].get.iMap

‎src/main/scala/uclid/lang/StatelessAxiomFinder.scala‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,14 @@ class StatelessAxiomFinderPass(mainModuleName: Identifier)
106106
inds.forall(ind => isStatelessExpr(ind, context)) &&
107107
args.forall(arg => isStatelessExpr(arg, context)) &&
108108
isStatelessExpr(value, context)
109+
case OperatorApplication(FiniteForallOp(_, gId), _) =>
110+
val opapp = e.asInstanceOf[OperatorApplication]
111+
isStatelessExpr(gId, context) &&
112+
opapp.operands.forall(arg => isStatelessExpr(arg, context + opapp.op))
113+
case OperatorApplication(FiniteExistsOp(_, gId), _) =>
114+
val opapp = e.asInstanceOf[OperatorApplication]
115+
isStatelessExpr(gId, context) &&
116+
opapp.operands.forall(arg => isStatelessExpr(arg, context + opapp.op))
109117
case opapp : OperatorApplication =>
110118
opapp.operands.forall(arg => isStatelessExpr(arg, context + opapp.op))
111119
case a : ConstArray =>
@@ -188,6 +196,7 @@ class StatelessAxiomFinderPass(mainModuleName: Identifier)
188196
}
189197
override def applyOnAxiom(d : TraversalDirection.T, axiom : AxiomDecl, in : T, context : Scope) : T = {
190198
if (in._1 && d == TraversalDirection.Down && isStatelessExpr(axiom.expr, context)) {
199+
logger.debug("Making a new axiom for %s %s".format(axiom.expr.toString, axiom.params.toString))
191200
val moduleName = context.module.get.id
192201
val exprP = rewriteToExternalIds(moduleName, axiom.expr, context)
193202
val name = axiom.id match {

‎src/main/scala/uclid/lang/UclidLanguage.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -370,10 +370,10 @@ case class ExistsOp(vs: List[(Identifier, Type)], patterns: List[List[Expr]]) ex
370370

371371
case class FiniteForallOp(id : (Identifier, Type), groupId : Identifier) extends QuantifiedBooleanOperator {
372372
override def variables = List.empty
373-
override def toString = QuantifiedBooleanOperator.toString("finite_forall", List.empty, List.empty)
373+
override def toString = "finite_forall %s : %s in %s".format(id._1, id._2, groupId)
374374
}
375375
case class FiniteExistsOp(id : (Identifier, Type), groupId : Identifier) extends QuantifiedBooleanOperator {
376-
override def toString = QuantifiedBooleanOperator.toString("finite_exists", List.empty, List.empty)
376+
override def toString = "finite_exists %s : %s in %s".format(id._1, id._2, groupId)
377377
override def variables = List.empty
378378
}
379379

‎src/test/scala/VerifierSpec.scala‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -384,6 +384,9 @@ class GroupVerifSpec extends AnyFlatSpec {
384384
"test-group-3.ucl" should "verify one and fail one assertion." in {
385385
VerifierSpec.expectedFails("./test/test-group-3.ucl", 1)
386386
}
387+
"test-group-4.ucl" should "verify one and fail one assertion." in {
388+
VerifierSpec.expectedFails("./test/test-group-4.ucl", 1)
389+
}
387390
}
388391
class ModuleVerifSpec extends AnyFlatSpec {
389392
"test-modules.ucl" should "verify all assertions." in {

‎test/test-group-4.ucl‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
module decl {
2+
input myGroup : group(integer);
3+
4+
var a, b : boolean;
5+
6+
init {
7+
a = finite_forall (int : integer) in myGroup :: int > -1; //Satisfied by grp
8+
b = finite_exists (int : integer) in myGroup :: int < 0; //Not satisfied by grp
9+
}
10+
11+
next {
12+
}
13+
}
14+
15+
module main {
16+
group grp : integer = {0, 1, 2, 3};
17+
18+
instance declInst : decl(myGroup : (grp));
19+
20+
init {
21+
}
22+
23+
next {
24+
}
25+
26+
property f : declInst.a; //Should pass
27+
property t : declInst.b; //Should fail
28+
29+
control {
30+
v = unroll(0);
31+
check;
32+
print_results;
33+
}
34+
}

0 commit comments

Comments
 (0)