Skip to content

Commit 075fd4b

Browse files
marcoeilersmarcoeilers
committed
Renaming
1 parent 4c2e467 commit 075fd4b

10 files changed

Lines changed: 107 additions & 106 deletions

File tree

‎src/main/scala/viper/silver/ast/Expression.scala‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -385,15 +385,15 @@ object DomainFuncApp {
385385
DomainFuncApp(func.name,args,typVarMap)(pos, info, func.typ.substitute(typVarMap), func.domainName, errT)
386386
}
387387

388-
// --- References to built-in SMT Lib functions
388+
// --- References to backend (i.e., SMTLIB or Boogie 'builtin') functions
389389

390-
case class SMTFuncApp(smtFunc: SMTFunc, args: Seq[Exp])
391-
(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
390+
case class BackendFuncApp(backendFunc: BackendFunc, args: Seq[Exp])
391+
(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
392392
extends AbstractDomainFuncApp {
393393
override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
394-
override def func = (p: Program) => smtFunc
395-
def funcname = smtFunc.name
396-
override def typ = smtFunc.typ
394+
override def func = (p: Program) => backendFunc
395+
def funcname = backendFunc.name
396+
override def typ = backendFunc.typ
397397
}
398398

399399
// --- Field and predicate accesses

‎src/main/scala/viper/silver/ast/Program.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -771,7 +771,7 @@ case object NotOp extends UnOp with BoolDomainFunc {
771771
}
772772

773773

774-
case class SMTFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl])
774+
case class BackendFunc(name: String, smtName: String, override val typ: Type, override val formalArgs: Seq[LocalVarDecl])
775775
extends Node with AbstractDomainFunc with BuiltinDomainFunc
776776

777777
/**

‎src/main/scala/viper/silver/ast/Type.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ case class TypeVar(name: String) extends Type {
183183
//def !=(other: TypeVar) = name != other
184184
}
185185

186-
case class SMTType(boogieName: String, smtName: String) extends AtomicType
186+
case class BackendType(boogieName: String, smtName: String) extends AtomicType
187187

188188
trait ExtensionType extends Type{
189189
def getAstType: Type = ???

‎src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -624,7 +624,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
624624
case dt@DomainType(domainName, typVarsMap) =>
625625
val typArgs = dt.typeParameters map (t => show(typVarsMap.getOrElse(t, t)))
626626
text(domainName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space)))
627-
case SMTType(boogieName, _) => boogieName
627+
case BackendType(boogieName, _) if boogieName != null => boogieName
628+
case BackendType(_, smtName) => smtName
628629
}
629630
}
630631

@@ -775,7 +776,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
775776
parens(text(funcname) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(dfa.typ))
776777
else
777778
text(funcname) <> parens(ssep(args map show, char (',') <> space))
778-
case SMTFuncApp(func, args) =>
779+
case BackendFuncApp(func, args) =>
779780
text(func.name) <> parens(ssep(args map show, char(',') <> space))
780781
case EmptySeq(elemTyp) =>
781782
text("Seq[") <> showType(elemTyp) <> "]()"

‎src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
package viper.silver.ast.utility
2+
3+
import viper.silver.ast.{Bool, Int, LocalVarDecl, BackendFunc, BackendType}
4+
5+
/**
6+
* A factory for fixed-size bitvectors that offers convenient access to bitvector types, as well as
7+
* function definitions for unary and binary functions on bitvectors, as well as conversions from and
8+
* to integers.
9+
*/
10+
case class BVFactory(size: Int) {
11+
lazy val typ = BackendType(s"bv${size}", s"(_ BitVec ${size})")
12+
13+
def xor(name: String) = BackendFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
14+
def and(name: String) = BackendFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
15+
def or(name: String) = BackendFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
16+
def add(name: String) = BackendFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
17+
def mul(name: String) = BackendFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
18+
def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
19+
def shr(name: String) = BackendFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
20+
21+
def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
22+
def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
23+
24+
def from_int(name: String) = BackendFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
25+
def to_int(name: String) = BackendFunc(name, s"(_ bv2int ${size})", Int, Seq(LocalVarDecl("x", typ)()))
26+
def from_nat(name: String) = BackendFunc(name, s"(_ nat2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
27+
def to_nat(name: String) = BackendFunc(name, s"(_ bv2nat ${size})", Int, Seq(LocalVarDecl("x", typ)()))
28+
}
29+
30+
/**
31+
* Rounding modes for floating point operations.
32+
*/
33+
object RoundingMode extends Enumeration {
34+
type RoundingMode = Value
35+
val RNE, RNA, RTP, RTN, RTZ = Value
36+
}
37+
import RoundingMode._
38+
39+
/**
40+
* A factory for IEEE floating point numbers with "exp" bits for the exponent, "mant" bits for the significant,
41+
* including the hidden bit, and a given rounding mode for all operations that use one.
42+
* Offers access to types, unary and binary operations, comparisons, and conversions from and to
43+
* bitvectors of size exp + mant.
44+
*/
45+
case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
46+
47+
lazy val typ = BackendType(s"float${mant}e${exp}", s"(_ FloatingPoint ${exp} ${mant})")
48+
49+
def neg(name: String) = BackendFunc(name, "fp.neg", typ, Seq(LocalVarDecl("x", typ)()))
50+
def abs(name: String) = BackendFunc(name, "fp.abs", typ, Seq(LocalVarDecl("x", typ)()))
51+
52+
def add(name: String) = BackendFunc(name, s"fp.add ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
53+
def sub(name: String) = BackendFunc(name, s"fp.sub ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
54+
def mul(name: String) = BackendFunc(name, s"fp.mul ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
55+
def div(name: String) = BackendFunc(name, s"fp.div ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
56+
def min(name: String) = BackendFunc(name, s"fp.min ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
57+
def max(name: String) = BackendFunc(name, s"fp.max ${roundingMode}", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
58+
59+
def eq(name: String) = BackendFunc(name, s"fp.eq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
60+
def leq(name: String) = BackendFunc(name, s"fp.leq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
61+
def geq(name: String) = BackendFunc(name, s"fp.geq", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
62+
def lt(name: String) = BackendFunc(name, s"fp.lt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
63+
def gt(name: String) = BackendFunc(name, s"fp.gt", Bool, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
64+
65+
def isZero(name: String) = BackendFunc(name, s"fp.isZero", Bool, Seq(LocalVarDecl("x", typ)()))
66+
def isInfinite(name: String) = BackendFunc(name, s"fp.isInfinite", Bool, Seq(LocalVarDecl("x", typ)()))
67+
def isNaN(name: String) = BackendFunc(name, s"fp.isNaN", Bool, Seq(LocalVarDecl("x", typ)()))
68+
def isNegative(name: String) = BackendFunc(name, s"fp.isNegative", Bool, Seq(LocalVarDecl("x", typ)()))
69+
def isPositive(name: String) = BackendFunc(name, s"fp.isPositive", Bool, Seq(LocalVarDecl("x", typ)()))
70+
71+
def from_bv(name: String) = BackendFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
72+
def to_bv(name: String) = BackendFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
73+
}

‎src/main/scala/viper/silver/ast/utility/Expressions.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ object Expressions {
3333
| _: PermExp
3434
| _: FuncApp
3535
| _: DomainFuncApp
36-
| _: SMTFuncApp
36+
| _: BackendFuncApp
3737
| _: LocationAccess
3838
| _: AbstractLocalVar
3939
| _: SeqExp

‎src/main/scala/viper/silver/ast/utility/Nodes.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ object Nodes {
106106
case FuncApp(_, args) => args
107107
case DomainFuncApp(_, args, m) =>
108108
args ++ m.keys ++ m.values
109-
case SMTFuncApp(_, args) => args
109+
case BackendFuncApp(_, args) => args
110110

111111
case EmptySeq(elemTyp) => Seq(elemTyp)
112112
case ExplicitSeq(elems) => elems

‎src/main/scala/viper/silver/ast/utility/SMTTypeFactories.scala‎

Lines changed: 0 additions & 73 deletions
This file was deleted.

‎src/main/scala/viper/silver/ast/utility/Types.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ object Types {
6969
* @return The list of transitive type constituents of `typ`.
7070
*/
7171
def typeConstituents(typ: Type): List[Type] = typ match {
72-
case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: SMTType => Nil
72+
case Int | Bool | Perm | Ref | InternalType | _: TypeVar | Wand | _: BackendType => Nil
7373
case dt: DomainType => dt.typeParameters.map(_.substitute(dt.typVarsMap)).toList
7474
case SeqType(elementType) => elementType :: typeConstituents(elementType)
7575
case SetType(elementType) => elementType :: typeConstituents(elementType)

src/main/scala/viper/silver/testing/SMTTypeTest.scala renamed to src/main/scala/viper/silver/testing/BackendTypeTest.scala

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
package viper.silver.testing
22

33
import org.scalatest.{BeforeAndAfterAllConfigMap, ConfigMap, FunSuite, Matchers}
4-
import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, SMTFuncApp, Seqn, SetType, Stmt}
4+
import viper.silver.ast.{AnySetContains, Assert, EqCmp, Exp, Field, FieldAccess, FieldAccessPredicate, FullPerm, Function, Inhale, IntLit, LocalVarAssign, LocalVarDecl, Method, Program, Ref, Result, BackendFuncApp, Seqn, SetType, Stmt}
55
import viper.silver.ast.utility.{BVFactory, FloatFactory, RoundingMode}
66
import viper.silver.verifier.{Failure, Success, Verifier}
77
import viper.silver.verifier.errors.{AssertFailed, PostconditionViolated}
88

9-
trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
9+
trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap {
1010

1111
def generateTypeCombinationTest(success: Boolean) : (Program, Assert) = {
1212
val t = if (success) BVFactory(23).typ else FloatFactory(23, 11, RoundingMode.RNE).typ
@@ -52,16 +52,16 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
5252
val fp_eq = fp.eq("fp_eq")
5353
val fp_add = fp.add("fp_add")
5454

55-
val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
56-
val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
57-
val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
55+
val first_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(first)()))()))()
56+
val second_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(second)()))()))()
57+
val result_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(result)()))()))()
5858

59-
val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
59+
val zero_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(0)()))()))()
6060

61-
val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
62-
val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
61+
val addition = BackendFuncApp(fp_add, Seq(first_float, second_float))()
62+
val result_addition = BackendFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
6363

64-
val equality = SMTFuncApp(fp_eq, Seq(addition, result_addition))()
64+
val equality = BackendFuncApp(fp_eq, Seq(addition, result_addition))()
6565
val assert = Assert(equality)()
6666
(wrapInProgram(Seq(assert), Seq(), Seq()), assert)
6767
}
@@ -78,16 +78,16 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
7878
val fp_eq = fp.eq("fp_eq")
7979
val fp_add = fp.add("fp_add")
8080

81-
val first_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(first)()))()))()
82-
val second_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(second)()))()))()
83-
val result_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(result)()))()))()
81+
val first_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(first)()))()))()
82+
val second_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(second)()))()))()
83+
val result_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(result)()))()))()
8484

85-
val zero_float = SMTFuncApp(to_fp, Seq(SMTFuncApp(from_int, Seq(IntLit(0)()))()))()
85+
val zero_float = BackendFuncApp(to_fp, Seq(BackendFuncApp(from_int, Seq(IntLit(0)()))()))()
8686

87-
val addition = SMTFuncApp(fp_add, Seq(first_float, second_float))()
88-
val result_addition = SMTFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
87+
val addition = BackendFuncApp(fp_add, Seq(first_float, second_float))()
88+
val result_addition = BackendFuncApp(fp_add, Seq(result_float, if (success) zero_float else first_float))()
8989

90-
val equality = SMTFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
90+
val equality = BackendFuncApp(fp_eq, Seq(Result(fp.typ)(), result_addition))()
9191

9292
val fun = Function("test", Seq(), fp.typ, Seq(), Seq(equality), Some(addition))()
9393
val program = Program(Seq(), Seq(), Seq(fun), Seq(), Seq(), Seq())()
@@ -100,14 +100,14 @@ trait SMTTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfigMap
100100
val two_lit = IntLit(2)()
101101
val three_lit = IntLit(3)()
102102
val one_lit = IntLit(1) ()
103-
val two = SMTFuncApp(from_int, Seq(two_lit))()
104-
val three = SMTFuncApp(from_int, Seq(three_lit))()
105-
val one = SMTFuncApp(from_int, Seq(one_lit))()
103+
val two = BackendFuncApp(from_int, Seq(two_lit))()
104+
val three = BackendFuncApp(from_int, Seq(three_lit))()
105+
val one = BackendFuncApp(from_int, Seq(one_lit))()
106106
val result_decl = LocalVarDecl("three", bv23.typ)()
107107
val result_ref = result_decl.localVar
108108
val assign = LocalVarAssign(result_ref, if (success) three else one)()
109109
val xor = bv23.xor("xorBV23")
110-
val xor_app = SMTFuncApp(xor, Seq(one, two))()
110+
val xor_app = BackendFuncApp(xor, Seq(one, two))()
111111
val equality1 = EqCmp(result_ref, xor_app)()
112112
val assertion1 = Assert(equality1)()
113113
(wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1)

0 commit comments

Comments
 (0)
⚡