From d817bb1958aa92b87c1e327bf9f25f0b922c3b65 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Tue, 25 Jul 2023 13:45:18 +0200 Subject: [PATCH] Adapted isinf and isfinite to match C standard --- .../grammar/src/main/antlr/CommonTokens.g4 | 4 ++ .../common/grammar/src/main/antlr/Expr.g4 | 2 +- .../mit/theta/grammar/dsl/expr/ExprParser.kt | 1 + .../xcfa/passes/FpFunctionsToExprsPass.kt | 42 ++++++++----------- .../hu/bme/mit/theta/xcfa/passes/PassTests.kt | 31 ++++++++++++-- 5 files changed, 50 insertions(+), 30 deletions(-) diff --git a/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 b/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 index 071f564cab..8f93b8d3f4 100644 --- a/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 +++ b/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 @@ -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' ; diff --git a/subprojects/common/grammar/src/main/antlr/Expr.g4 b/subprojects/common/grammar/src/main/antlr/Expr.g4 index 0c127e7a09..6753a55233 100644 --- a/subprojects/common/grammar/src/main/antlr/Expr.g4 +++ b/subprojects/common/grammar/src/main/antlr/Expr.g4 @@ -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 diff --git a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt index 995883113e..ffc7fe07c7 100644 --- a/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt +++ b/subprojects/common/grammar/src/main/java/hu/bme/mit/theta/grammar/dsl/expr/ExprParser.kt @@ -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) + FP_IS_INF -> FpExprs.IsInfinite(op as Expr) FP_IS_NAN -> FpExprs.IsNan(op as Expr) FPROUNDTOINT -> FpExprs.RoundToIntegral(getRoundingMode(ctx.oper.text), op as Expr) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt index 74c581358e..9a05a150e1 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/FpFunctionsToExprsPass.kt @@ -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 @@ -147,18 +147,14 @@ 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( - FpIsInfiniteExpr.of(callStmt.params[1] as Expr), 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( + FpIsInfiniteExpr.of(callStmt.params[1] as Expr), type.unitValue, type.nullValue), + type.smtType)) + parseContext.metadata.create(assign.expr, "cType", type) + return StmtLabel(assign, metadata = callStmt.metadata) } private fun handleIsfinite(builder: XcfaProcedureBuilder, @@ -166,18 +162,14 @@ 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( - BoolExprs.Not(FpIsInfiniteExpr.of(callStmt.params[1] as Expr)), - 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( + FpIsInfiniteExpr.of(callStmt.params[1] as Expr), type.nullValue, type.unitValue), + type.smtType)) + parseContext.metadata.create(assign.expr, "cType", type) + return StmtLabel(assign, metadata = callStmt.metadata) } private fun handleIsnormal(builder: XcfaProcedureBuilder, diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt index c124e9a6c4..1bc7f624e8 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt @@ -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 @@ -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 = listOf( @@ -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) { @@ -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) { @@ -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(