Skip to content

Commit

Permalink
Adapted isinf and isfinite to match C standard
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Jul 25, 2023
1 parent e53fa27 commit d817bb1
Show file tree
Hide file tree
Showing 5 changed files with 50 additions and 30 deletions.
4 changes: 4 additions & 0 deletions subprojects/common/grammar/src/main/antlr/CommonTokens.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,10 @@ FP_FROM_BV
: 'fpfrombv' FP_TYPE_DECL (LBRACK ('u' | 's') RBRACK) FP_ROUNDINGMODE?
;

FP_IS_INF
: 'isinfinite'
;

FP_IS_NAN
: 'fpisnan'
;
Expand Down
2 changes: 1 addition & 1 deletion subprojects/common/grammar/src/main/antlr/Expr.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ bvExtendExpr

unaryExpr
: bitwiseNotExpr
| LPAREN oper=(PLUS | MINUS | BV_POS | BV_NEG | FP_ABS | FP_IS_NAN | FPROUNDTOINT | FPSQRT | FPTOFP | FPTOBV | FP_FROM_BV | FPNEG | FPPOS ) op=expr RPAREN
| LPAREN oper=(PLUS | MINUS | BV_POS | BV_NEG | FP_ABS | FP_IS_INF | FP_IS_NAN | FPROUNDTOINT | FPSQRT | FPTOFP | FPTOBV | FP_FROM_BV | FPNEG | FPPOS ) op=expr RPAREN
;

bitwiseNotExpr
Expand Down
1 change: 1 addition & 0 deletions subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -616,6 +616,7 @@ class ExpressionWrapper(scope: Scope, content: String) {
PLUS -> AbstractExprs.Pos(op)
MINUS -> AbstractExprs.Neg(op)
FP_ABS -> FpExprs.Abs(op as Expr<FpType?>)
FP_IS_INF -> FpExprs.IsInfinite(op as Expr<FpType?>)
FP_IS_NAN -> FpExprs.IsNan(op as Expr<FpType?>)
FPROUNDTOINT -> FpExprs.RoundToIntegral(getRoundingMode(ctx.oper.text),
op as Expr<FpType?>)
Expand Down
42 changes: 17 additions & 25 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,11 +23,11 @@ import hu.bme.mit.theta.core.type.Expr
import hu.bme.mit.theta.core.type.Type
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs
import hu.bme.mit.theta.core.type.anytype.RefExpr
import hu.bme.mit.theta.core.type.booltype.BoolExprs
import hu.bme.mit.theta.core.type.fptype.*
import hu.bme.mit.theta.core.utils.TypeUtils
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CSignedInt
import hu.bme.mit.theta.xcfa.model.*
import java.util.function.BiFunction

Expand Down Expand Up @@ -147,37 +147,29 @@ class FpFunctionsToExprsPass(val parseContext: ParseContext) : ProcedurePass {
Preconditions.checkState(callStmt.params.size == 2, "Function is presumed to be unary!")
val expr = callStmt.params[0]
Preconditions.checkState(expr is RefExpr<*>)
if (parseContext.getMetadata().getMetadataValue(expr, "cType").isPresent) {
val type = CComplexType.getType(expr, parseContext)
val assign: AssignStmt<*> = Stmts.Assign(
TypeUtils.cast((expr as RefExpr<*>).decl as VarDecl<*>, type.smtType),
TypeUtils.cast(AbstractExprs.Ite<Type>(
FpIsInfiniteExpr.of(callStmt.params[1] as Expr<FpType?>), type.unitValue,
type.nullValue), type.smtType))
parseContext.getMetadata().create(assign.expr, "cType", type)
return StmtLabel(assign, metadata = callStmt.metadata)
} else {
throw UnsupportedOperationException("Not yet supported without cType")
}
val type = CSignedInt(null, parseContext)
val assign: AssignStmt<*> = Stmts.Assign(
TypeUtils.cast((expr as RefExpr<*>).decl as VarDecl<*>, type.smtType),
TypeUtils.cast(AbstractExprs.Ite<Type>(
FpIsInfiniteExpr.of(callStmt.params[1] as Expr<FpType?>), type.unitValue, type.nullValue),
type.smtType))
parseContext.metadata.create(assign.expr, "cType", type)
return StmtLabel(assign, metadata = callStmt.metadata)
}

private fun handleIsfinite(builder: XcfaProcedureBuilder,
callStmt: InvokeLabel): XcfaLabel {
Preconditions.checkState(callStmt.params.size == 2, "Function is presumed to be unary!")
val expr = callStmt.params[0]
Preconditions.checkState(expr is RefExpr<*>)
if (parseContext.getMetadata().getMetadataValue(expr, "cType").isPresent) {
val type = CComplexType.getType(expr, parseContext)
val assign: AssignStmt<*> = Stmts.Assign(
TypeUtils.cast((expr as RefExpr<*>).decl as VarDecl<*>, type.smtType),
TypeUtils.cast(AbstractExprs.Ite<Type>(
BoolExprs.Not(FpIsInfiniteExpr.of(callStmt.params[1] as Expr<FpType?>)),
type.unitValue, type.nullValue), type.smtType))
parseContext.getMetadata().create(assign.expr, "cType", type)
return StmtLabel(assign, metadata = callStmt.metadata)
} else {
throw UnsupportedOperationException("Not yet supported without cType")
}
val type = CSignedInt(null, parseContext)
val assign: AssignStmt<*> = Stmts.Assign(
TypeUtils.cast((expr as RefExpr<*>).decl as VarDecl<*>, type.smtType),
TypeUtils.cast(AbstractExprs.Ite<Type>(
FpIsInfiniteExpr.of(callStmt.params[1] as Expr<FpType?>), type.nullValue, type.unitValue),
type.smtType))
parseContext.metadata.create(assign.expr, "cType", type)
return StmtLabel(assign, metadata = callStmt.metadata)
}

private fun handleIsnormal(builder: XcfaProcedureBuilder,
Expand Down
31 changes: 27 additions & 4 deletions subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,14 @@ import hu.bme.mit.theta.core.decl.Decls.Var
import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.stmt.AssignStmt
import hu.bme.mit.theta.core.stmt.Stmts.Assign
import hu.bme.mit.theta.core.type.bvtype.BvExprs.BvType
import hu.bme.mit.theta.core.type.fptype.FpExprs.FpType
import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
import hu.bme.mit.theta.core.type.inttype.IntType
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig
import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.cint.CSignedInt
import hu.bme.mit.theta.frontend.transformation.model.types.complex.real.CFloat
import hu.bme.mit.theta.xcfa.getFlatLabels
import hu.bme.mit.theta.xcfa.model.*
import org.junit.jupiter.api.Assertions
Expand Down Expand Up @@ -54,6 +57,7 @@ class PassTests {

private val dummyXcfa = xcfa("") {}
private val parseContext = ParseContext()
private val fpParseContext = ParseContext().also { it.arithmetic = ArchitectureConfig.ArithmeticType.bitvector }

@JvmStatic
val data: List<Arguments> = listOf(
Expand Down Expand Up @@ -206,11 +210,16 @@ class PassTests {
},
),
PassTestData(
global = { "x" type FpType(5, 11) init "0.0f"; },
global = {
"y" type BvType(32) init "0"
("x" type FpType(8, 24) init "0.0f").also {
fpParseContext.metadata.create(it.ref, "cType", CFloat(null, fpParseContext))
};
},
passes = listOf(
NormalizePass(parseContext),
DeterministicPass(parseContext),
FpFunctionsToExprsPass(parseContext),
NormalizePass(fpParseContext),
DeterministicPass(fpParseContext),
FpFunctionsToExprsPass(fpParseContext),
),
input = {
(init to final) {
Expand All @@ -237,6 +246,12 @@ class PassTests {
(init to final) {
"ceil".invoke("x", "x")
}
(init to final) {
"isinf".invoke("y", "x")
}
(init to final) {
"isfinite".invoke("y", "x")
}
},
output = {
(init to final) {
Expand All @@ -263,6 +278,14 @@ class PassTests {
(init to final) {
"x".assign("(fproundtoint[RTP] x)")
}
(init to final) {
"y".assign(
"(ite (isinfinite x) #b00000000000000000000000000000001 #b00000000000000000000000000000000)")
}
(init to final) {
"y".assign(
"(ite (isinfinite x) #b00000000000000000000000000000000 #b00000000000000000000000000000001)")
}
},
),
PassTestData(
Expand Down

0 comments on commit d817bb1

Please sign in to comment.