Skip to content

Commit

Permalink
Merge pull request #93 from UQ-PAC/direct-spec-improvements
Browse files Browse the repository at this point in the history 
Specification Improvements
  • Loading branch information
@l-kent
l-kent authored Oct 13, 2023
2 parents 96bc93f + 7fabd61 commit ada2dd4
Show file tree
Hide file tree
Showing 7 changed files with 135 additions and 111 deletions.
102 changes: 59 additions & 43 deletions src/main/antlr4/Specifications.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,17 @@ relies: 'Rely:' expr (COMMA expr)*;
guarantees: 'Guarantee:' expr (COMMA expr)*;

directFunctions: 'DIRECT functions:' directFunction (COMMA directFunction)*;
directFunction: 'memory_load' size=nat endian #memoryLoad
| 'memory_store' size=nat endian #memoryStore
| 'gamma_load' size=nat #gammaLoad
| 'gamma_store' size=nat #gammaStore
| 'zero_extend' size1=nat UNDERSCORE size2=nat #zeroExtend
| 'sign_extend' size1=nat UNDERSCORE size2=nat #signExtend
| BV OPNAME size=nat #bvOp
directFunction: MEMORY_LOAD_DIRECT #memoryLoad
| MEMORY_STORE_DIRECT #memoryStore
| GAMMA_LOAD_DIRECT #gammaLoad
| GAMMA_STORE_DIRECT #gammaStore
| ZERO_EXTEND_DIRECT #zeroExtend
| SIGN_EXTEND_DIRECT #signExtend
| BVOP_DIRECT #bvOp
;

subroutine: 'Subroutine:' id requires* ensures*;
subroutine: 'Subroutine:' id modifies? requires* ensures*;
modifies: 'Modifies:' id (COMMA id)*;
requires: 'Requires:' expr #parsedRequires
| 'Requires DIRECT:' QUOTESTRING #directRequires
;
Expand All @@ -41,7 +42,6 @@ arrayAccess: id '[' nat ']';
id : ID;
nat: (DIGIT)+ ;
bv: value=nat BVSIZE;
endian: LE | BE;

// based upon boogie grammar: https://boogie-docs.readthedocs.io/en/latest/LangRef.html#grammar
expr : impliesExpr ( EQUIV_OP impliesExpr )* ;
Expand Down Expand Up @@ -70,7 +70,25 @@ atomExpr : boolLit #boolLitExpr
QUOTE : '"';
QUOTESTRING : QUOTE (~( '"' | '\n' | '\r'))+ QUOTE;

BV: 'bv';
BVOP_DIRECT: BV OPNAME DIGIT+;

MEMORY_LOAD_DIRECT: MEMORY_LOAD DIGIT+ ENDIAN;
MEMORY_STORE_DIRECT: MEMORY_STORE DIGIT+ ENDIAN;
GAMMA_LOAD_DIRECT: GAMMA_LOAD DIGIT+;
GAMMA_STORE_DIRECT: GAMMA_STORE DIGIT+;
ZERO_EXTEND_DIRECT: ZERO_EXTEND DIGIT+ UNDERSCORE DIGIT+;
SIGN_EXTEND_DIRECT: SIGN_EXTEND DIGIT+ UNDERSCORE DIGIT+;

fragment MEMORY_LOAD: 'memory_load';
fragment MEMORY_STORE: 'memory_store';
fragment GAMMA_LOAD: 'gamma_load';
fragment GAMMA_STORE: 'gamma_store';
fragment ZERO_EXTEND: 'zero_extend';
fragment SIGN_EXTEND: 'sign_extend';

ENDIAN: LE | BE;

fragment BV: 'bv';

LONG: 'long';
SHORT: 'short';
Expand All @@ -88,7 +106,7 @@ ELSE: 'else';
DIV_OP : 'div';
MOD_OP : 'mod';

BVSIZE: BV DIGIT DIGIT?;
BVSIZE: BV DIGIT+;

ID : NON_DIGIT ( NON_DIGIT | DIGIT )* ;
NON_DIGIT : ( [A-Z] | [a-z] | '\'' | '~' | '#' | '$' | '^' | '_' | '.' | '?' | '`') ;
Expand All @@ -115,13 +133,11 @@ SUB_OP : '-';
MUL_OP : '*';

COLON: ':';
UNDERSCORE: '_';
LE: '_le';
BE: '_be';


fragment UNDERSCORE: '_';
fragment LE: '_le';
fragment BE: '_be';

OPNAME : AND
fragment OPNAME : AND
| OR
| ADD
| MUL
Expand Down Expand Up @@ -149,32 +165,32 @@ OPNAME : AND
| COMP
;

AND : 'and';
OR : 'or';
ADD : 'add';
MUL : 'mul';
UDIV : 'udiv';
UREM : 'urem';
SHL : 'shl';
LSHR : 'lshr';
ULT : 'ult';
NAND : 'nand';
NOR : 'nor';
XOR : 'xor';
XNOR : 'xnor';
SUB : 'sub';
SREM : 'srem';
SDIV : 'sdiv';
SMOD : 'smod';
ASHR : 'ashr';
ULE : 'ule';
UGT : 'ugt';
UGE : 'uge';
SLT : 'slt';
SLE : 'sle';
SGT : 'sgt';
SGE : 'sge';
COMP : 'comp';
fragment AND : 'and';
fragment OR : 'or';
fragment ADD : 'add';
fragment MUL : 'mul';
fragment UDIV : 'udiv';
fragment UREM : 'urem';
fragment SHL : 'shl';
fragment LSHR : 'lshr';
fragment ULT : 'ult';
fragment NAND : 'nand';
fragment NOR : 'nor';
fragment XOR : 'xor';
fragment XNOR : 'xnor';
fragment SUB : 'sub';
fragment SREM : 'srem';
fragment SDIV : 'sdiv';
fragment SMOD : 'smod';
fragment ASHR : 'ashr';
fragment ULE : 'ule';
fragment UGT : 'ugt';
fragment UGE : 'uge';
fragment SLT : 'slt';
fragment SLE : 'sle';
fragment SGT : 'sgt';
fragment SGE : 'sge';
fragment COMP : 'comp';

// Ignored
NEWLINE : '\r'? '\n' -> skip;
Expand Down
3 changes: 2 additions & 1 deletion src/main/scala/boogie/BProgram.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,8 @@ case class BProcedure(
body.flatMap(c => c.functionOps).toSet ++ ensures.flatMap(c => c.functionOps).toSet ++ requires
.flatMap(c => c.functionOps)
.toSet ++ freeEnsures.flatMap(c => c.functionOps).toSet ++ freeRequires.flatMap(c => c.functionOps).toSet
def globals: Set[BVar] = body.flatMap(c => c.globals).toSet

def globals: Set[BVar] = body.flatMap(c => c.globals).toSet ++ modifies
}

case class BAxiom(body: BExpr) extends BDeclaration {
Expand Down
52 changes: 18 additions & 34 deletions src/main/scala/ir/Program.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,16 +32,20 @@ class Program(
procedures = procedures.filter(f => reachableNames.contains(f.name))
}

def setModifies(): Unit = {
//val procToModifies: mutable.Map[Procedure, mutable.Set[Global]] = mutable.Map()
def setModifies(specModifies: Map[String, List[String]]): Unit = {

val procToCalls: mutable.Map[Procedure, Set[Procedure]] = mutable.Map()
for (p <- procedures) {
//procToModifies(p) = mutable.Set()
//procToModifies(p).addAll(p.blocks.flatMap(_.modifies))
p.modifies.addAll(p.blocks.flatMap(_.modifies))
procToCalls(p) = p.calls
}

for (p <- procedures) {
if (specModifies.contains(p.name)) {
p.modifies.addAll(specModifies(p.name).map(nameToGlobal))
}
}

// very naive implementation but will work for now
var hasChanged: Boolean = true
while (hasChanged) {
Expand All @@ -58,39 +62,19 @@ class Program(
}
}
}
}

/*
val visited: mutable.Set[Procedure] = mutable.Set()
val waiting: mutable.Set[Procedure] = mutable.Set()
val loops: mutable.Set[Set[Procedure]] = mutable.Set()
// need to add support for back edges - do a fixed point on them so all procedures in a loop have the same modifies
DFSVisit(mainProcedure, Vector(mainProcedure))
def DFSVisit(p: Procedure, path: Vector[Procedure]): Vector[Procedure] = {
val children = procToCalls(p)
if (visited.contains(p)) {
return path
}
if (waiting.contains(p)) {
val loopPath = path.slice(path.indexOf(p), path.size)
loops.add(loopPath.toSet)
return path
//throw new Exception("back edge in intraprocedural control flow graph, not currently supported")
}
waiting.add(p)
p.modifies.addAll(procToModifies(p))
for (child <- children) {
if (child != p) {
DFSVisit(child, path :+ p)
}
}
for (child <- children) {
p.modifies.addAll(child.modifies)
// this is very crude but the simplest thing for now until we have a more sophisticated specification system that can relate to the IR instead of the Boogie
def nameToGlobal(name: String): Global = {
if ((name.startsWith("R") || name.startsWith("V")) && (name.length == 2 || name.length == 3) && name.substring(1).forall(_.isDigit)) {
if (name.startsWith("R")) {
Register(name, BitVecType(64))
} else {
Register(name, BitVecType(128))
}
waiting.remove(p)
visited.add(p)
path :+ p
} else {
Memory(name, 64, 8)
}
*/
}

def stackIdentification(): Unit = {
Expand Down
2 changes: 2 additions & 0 deletions src/main/scala/ir/Visitor.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,6 +307,8 @@ class Renamer(reserved: Set[String]) extends Visitor {
class ExternalRemover(external: Set[String]) extends Visitor {
override def visitProcedure(node: Procedure): Procedure = {
if (external.contains(node.name)) {
// update the modifies set before removing the body
node.modifies.addAll(node.blocks.flatMap(_.modifies))
node.blocks = ArrayBuffer()
}
super.visitProcedure(node)
Expand Down
3 changes: 2 additions & 1 deletion src/main/scala/specification/Specification.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,8 @@ case class SubroutineSpec(
requires: List[BExpr],
requiresDirect: List[String],
ensures: List[BExpr],
ensuresDirect: List[String]
ensuresDirect: List[String],
modifies: List[String]
)

case class ExternalFunction(name: String, offset: BigInt)
67 changes: 41 additions & 26 deletions src/main/scala/translating/SpecificationLoader.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,35 +51,41 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
}

def visitDirectFunction(ctx: DirectFunctionContext): FunctionOp = ctx match {
case m: MemoryLoadContext => MemoryLoadOp(64, 8, visitEndian(m.endian), Integer.parseInt(m.size.getText))
case m: MemoryStoreContext => MemoryStoreOp(64, 8, visitEndian(m.endian), Integer.parseInt(m.size.getText))
case m: MemoryLoadContext =>
val suffix = m.getText.stripPrefix("memory_load")
val size = suffix.stripSuffix("_le").stripSuffix("_be")
val endian = suffix.stripPrefix(size)
MemoryLoadOp(64, 8, parseEndian(endian), Integer.parseInt(size))
case m: MemoryStoreContext =>
val suffix = m.getText.stripPrefix("memory_store")
val size = suffix.stripSuffix("_le").stripSuffix("_be")
val endian = suffix.stripPrefix(size)
MemoryStoreOp(64, 8, parseEndian(endian), Integer.parseInt(size))
case g: GammaLoadContext =>
val size = Integer.parseInt(g.size.getText)
val sizeText = g.getText.stripPrefix("gamma_load")
val size = Integer.parseInt(sizeText)
GammaLoadOp(64, size, size / 8)
case g: GammaStoreContext =>
val size = Integer.parseInt(g.size.getText)
val sizeText = g.getText.stripPrefix("gamma_store")
val size = Integer.parseInt(sizeText)
GammaStoreOp(64, size, size / 8)
case z: ZeroExtendContext =>
val extension = Integer.parseInt(z.size1.getText)
val bodySize = Integer.parseInt(z.size2.getText)
BVFunctionOp(
s"zero_extend${extension}_$bodySize",
s"zero_extend $extension",
List(BParam(BitVecBType(bodySize))),
BParam(BitVecBType(bodySize + extension))
)
val suffix = z.getText.stripPrefix("zero_extend")
val sizes = suffix.split("_")
val extension = Integer.parseInt(sizes(0))
val bodySize = Integer.parseInt(sizes(1))
BVFunctionOp(s"zero_extend${extension}_$bodySize", s"zero_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(BitVecBType(bodySize + extension)))
case s: SignExtendContext =>
val extension = Integer.parseInt(s.size1.getText)
val bodySize = Integer.parseInt(s.size2.getText)
BVFunctionOp(
s"sign_extend${extension}_$bodySize",
s"sign_extend $extension",
List(BParam(BitVecBType(bodySize))),
BParam(BitVecBType(bodySize + extension))
)
val suffix = s.getText.stripPrefix("sign_extend")
val sizes = suffix.split("_")
val extension = Integer.parseInt(sizes(0))
val bodySize = Integer.parseInt(sizes(1))
BVFunctionOp(s"sign_extend${extension}_$bodySize", s"sign_extend $extension", List(BParam(BitVecBType(bodySize))), BParam(BitVecBType(bodySize + extension)))
case b: BvOpContext =>
val size = Integer.parseInt(b.size.getText)
val op = b.OPNAME.getText
val body = b.getText.stripPrefix("bv")
val sizeText = body.replaceAll("\\D+","")
val size = Integer.parseInt(sizeText)
val op = body.stripSuffix(sizeText)
val outType = op match {
case "and" | "or" | "add" | "mul" | "udiv" | "urem" | "shl" | "lshr" | "nand" | "nor" | "xor" | "xnor" | "sub" |
"srem" | "sdiv" | "smod" | "ashr" =>
Expand All @@ -94,7 +100,7 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
BVFunctionOp(s"bv$op$size", s"bv$op", List(BParam(BitVecBType(size)), BParam(BitVecBType(size))), BParam(outType))
}

def visitEndian(ctx: EndianContext): Endian = ctx.getText match {
def parseEndian(endian: String): Endian = endian match {
case "_le" => Endian.LittleEndian
case "_be" => Endian.BigEndian
}
Expand Down Expand Up @@ -362,8 +368,13 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
visitExpr(r.expr, nameToGlobals, params)
}.toList

val ensures = ctx.ensures.asScala.collect { case e: ParsedEnsuresContext =>
visitExpr(e.expr, nameToGlobals, params)
val modifies = Option(ctx.modifies) match {
case Some(_) => visitModifies(ctx.modifies)
case None => List()
}

val ensures = ctx.ensures.asScala.collect {
case e: ParsedEnsuresContext => visitExpr(e.expr, nameToGlobals, params)
}.toList

val requiresDirect = ctx.requires.asScala.collect { case r: DirectRequiresContext =>
Expand All @@ -374,7 +385,11 @@ case class SpecificationLoader(symbols: Set[SpecGlobal], program: Program) {
r.QUOTESTRING.getText.stripPrefix("\"").stripSuffix("\"")
}.toList

SubroutineSpec(ctx.id.getText, requires, requiresDirect, ensures, ensuresDirect)
SubroutineSpec(ctx.id.getText, requires, requiresDirect, ensures, ensuresDirect, modifies)
}

def visitModifies(ctx: ModifiesContext): List[String] = {
ctx.id.asScala.map(_.getText).toList
}

}
17 changes: 11 additions & 6 deletions src/main/scala/util/RunUtils.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,18 +91,23 @@ object RunUtils {
IRProgram = externalRemover.visitProgram(IRProgram)
IRProgram = renamer.visitProgram(IRProgram)

if (performAnalysis) {
iterations += 1;
IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
}

if (dumpIL) {
dump_file(serialiseIL(IRProgram), "before-analysis.il")
}


if (performAnalysis) {
iterations += 1;
IRProgram = analyse(IRProgram, externalFunctions, globals, globalOffsets)
if (dumpIL) {
dump_file(serialiseIL(IRProgram), "after-analysis.il")
}
}
IRProgram.stripUnreachableFunctions()
IRProgram.stackIdentification()
IRProgram.setModifies()

val specModifies = specification.subroutines.map(s => s.name -> s.modifies).toMap
IRProgram.setModifies(specModifies)

Logger.info("[!] Translating to Boogie")
val boogieTranslator = IRToBoogie(IRProgram, specification)
Expand Down

0 comments on commit ada2dd4

Please sign in to comment.