Skip to content

Commit

Permalink
fix test control flow case
Browse files Browse the repository at this point in the history
Addresses #653.
  • Loading branch information
PeiMu committed May 7, 2023
1 parent 91947db commit 037939f
Show file tree
Hide file tree
Showing 6 changed files with 315 additions and 6 deletions.
46 changes: 46 additions & 0 deletions analysis/statistics/5a6215a127c6ae78b0faac6af09988e13b927474.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@

changeset: 1482:5a6215a127c6ae78b0faac6af09988e13b927474
char kNewtonVersion[] = "0.3-alpha-1482 (5a6215a127c6ae78b0faac6af09988e13b927474) (build 05-01-2023-20:[email protected]_64)";
\n./src/noisy/noisy-linux-EN -O0 applications/noisy/helloWorld.n -s
\n./src/newton/newton-linux-EN -v 0 -eP applications/newton/invariants/ViolinWithTemperatureDependence-pigroups.nt

Informational Report:
---------------------
Invariant "ViolinWithTemperatureDependenceForPiGroups" has 2 unique kernels, each with 2 column(s)...

Kernel 0 is a valid kernel:

1 1
-0.5 -0
1 0
0.5 0
0 -1
-0 -1


The ordering of parameters is: P1 P0 P3 P2 P4 P5

Pi group 0, Pi 0 is: P0^(-0.5) P1^( 1) P2^(0.5) P3^( 1) P4^( 0) P5^(-0)

Pi group 0, Pi 1 is: P0^(-0) P1^( 1) P2^( 0) P3^( 0) P4^(-1) P5^(-1)


Kernel 1 is a valid kernel:

1 0
-0.5 1
1 -2
0.5 -1
-0 -2
0 -2


The ordering of parameters is: P1 P0 P3 P2 P4 P5

Pi group 1, Pi 0 is: P0^(-0.5) P1^( 1) P2^(0.5) P3^( 1) P4^(-0) P5^( 0)

Pi group 1, Pi 1 is: P0^( 1) P1^( 0) P2^(-1) P3^(-2) P4^(-2) P5^(-2)




1 change: 0 additions & 1 deletion applications/newton/llvm-ir/c-files/e_acosh.c
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,6 @@ double __ieee754_acosh(x)
bmx055xAcceleration x;
#endif
{
__builtin_assume(x > 3 && x < 10);
double t;
int hx;
hx = __HI(x);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,6 @@ typedef double bmx055xAcceleration; // [-16, 16]
static int
ifStatement(bmx055xAcceleration x)
{
__builtin_assume(x > 3 && x < 10);
int y = 397;
/*
* If statement
Expand Down
8 changes: 4 additions & 4 deletions applications/newton/llvm-ir/performance_test/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -219,15 +219,15 @@ madgwick_non_opt:
madgwick_opt:
cd $(NEWTON_BIN_DIR) && $(call newton_opt_fn,MadgwickAHRSfix)
llvm-dis ../MadgwickAHRSfix_output.bc
$(call max_opt_fn,MadgwickAHRSfix)
$(call max_opt_fn,MadgwickAHRSfix_output)

inferBoundControlFlow_non_opt:
$(call max_opt_fn,inferBoundControlFlow)

inferBoundControlFlow_opt:
cd $(NEWTON_BIN_DIR) && $(call newton_opt_fn,MadgwickAHRSfix)
llvm-dis ../MadgwickAHRSfix_output.bc
$(call max_opt_fn,inferBoundControlFlow)
cd $(NEWTON_BIN_DIR) && $(call newton_opt_fn,inferBoundControlFlow)
llvm-dis ../inferBoundControlFlow_output.bc
$(call max_opt_fn,inferBoundControlFlow_output)

compile_test_madgwick:
$(CC) $(TARGET_FLAG) ../test_madgwick.c -no-pie -L. -lout -O3 -Os -o main_out -lm
Expand Down
221 changes: 221 additions & 0 deletions src/newton/newton-irPass-LLVMIR-emitAssume.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,221 @@
/*
Authored 2022. Pei Mu.
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
* Redistributions of source code must retain the above
copyright notice, this list of conditions and the following
disclaimer.
* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials
provided with the distribution.
* Neither the name of the author nor the names of its
contributors may be used to endorse or promote products
derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.
*/

#include "newton-irPass-LLVMIR-constantSubstitution.h"

using namespace llvm;

extern "C" {
/*
* Steps of constantSubstitution:
* 1. for each instruction (that is the case statement), get the range of current instruction from boundInfo
* 2. check if the lower range and upper range is the same value, then it means this is a constant value instruction
* 3. get the type of current constant value instruction, mainly float/double/integer (with different bits)
* 4. use llvm API to create a new constant value
* 5. substitute current instruction with the constant value
* */
void
constantSubstitution(State * N, BoundInfo * boundInfo, llvm::Function & llvmIrFunction)
{
/*
* Some special instructions that need to pay attention:
* %i = alloca type, the type of this instruction is "type*"
* %i = call retType @func_name (type %p1, ...)
* call void @llvm.dbg.declare/value (metadata type %p, ...)
* %i = load type, type* %op, the type of this instruction is "type"
* %i = gep type, type1* %op1, type2 %op2, (type3 %op3)
* %i = castInst type1 %op1 to type2
* store type %op1, type* %op2
* %.i = phi type [%op1, %bb1], [%op2, %bb2], ...
* %i = binary type %op1, %op2
* %i = unary type %op
* */
for (BasicBlock & llvmIrBasicBlock : llvmIrFunction)
{
for (BasicBlock::iterator itBB = llvmIrBasicBlock.begin(); itBB != llvmIrBasicBlock.end();)
{
Instruction * llvmIrInstruction = &*itBB++;
switch (llvmIrInstruction->getOpcode())
{
case Instruction::Call:
case Instruction::Add:
case Instruction::FAdd:
case Instruction::Sub:
case Instruction::FSub:
case Instruction::Mul:
case Instruction::FMul:
case Instruction::SDiv:
case Instruction::FDiv:
case Instruction::UDiv:
case Instruction::URem:
case Instruction::SRem:
case Instruction::FRem:
case Instruction::Shl:
case Instruction::LShr:
case Instruction::AShr:
case Instruction::And:
case Instruction::Or:
case Instruction::Xor:
case Instruction::FNeg:
case Instruction::FPToUI:
case Instruction::FPToSI:
case Instruction::SIToFP:
case Instruction::UIToFP:
case Instruction::ZExt:
case Instruction::SExt:
case Instruction::FPExt:
case Instruction::Trunc:
case Instruction::FPTrunc:
case Instruction::BitCast:
case Instruction::Load:
case Instruction::GetElementPtr:
case Instruction::PHI:
{
auto vrIt = boundInfo->virtualRegisterRange.find(llvmIrInstruction);
if (vrIt == boundInfo->virtualRegisterRange.end())
{
break;
}

/*
* there's one case the GEP cannot be substituted
* define dso_local i32 @__ieee754_rem_pio2(double %0, double* %1) #0 !dbg !568 {
* ...
* %12 = getelementptr inbounds double, double* %1, i64 1, !dbg !594
* store double 0.000000e+00, double* %12, align 8, !dbg !595
* ...
* */
if (isa<GetElementPtrInst>(llvmIrInstruction) && isa<Argument>(llvmIrInstruction->getOperand(0))) {
break;
}

/*
* if it's a pointer, skip it
* */
if (llvmIrInstruction->getType()->isPointerTy())
{
break;
}

auto lowerBound = vrIt->second.first;
auto upperBound = vrIt->second.second;
/*
* if it's a constant
* */
if (fabs(lowerBound - upperBound) < DBL_EPSILON)
{
/*
* check the type of instruction
* */
Value * newConstant = nullptr;
uint64_t intBitWidth;
auto instType = llvmIrInstruction->getType();
auto typeId = instType->getTypeID();
if (typeId == Type::PointerTyID)
{
instType = instType->getPointerElementType();
typeId = instType->getTypeID();
}
switch (typeId)
{
case Type::IntegerTyID:
newConstant = ConstantInt::get(instType, lowerBound, lowerBound < 0);
break;
case Type::FloatTyID:
case Type::DoubleTyID:
newConstant = ConstantFP::get(instType, lowerBound);
break;
default:
break;
}
if (newConstant != nullptr)
{
llvmIrInstruction->replaceAllUsesWith(newConstant);
llvmIrInstruction->removeFromParent();
}
}
}
break;
case Instruction::Store:
if (auto llvmIrStoreInstruction = dyn_cast<StoreInst>(llvmIrInstruction))
{
/*
* remove the const store inst, e.g.
* store double 0.000000e+00, double 0.000000e+00, align 8
* */
if (isa<llvm::Constant>(llvmIrStoreInstruction->getPointerOperand()))
llvmIrStoreInstruction->removeFromParent();
}
break;
case Instruction::ICmp:
case Instruction::FCmp:
break;
case Instruction::Ret:
break;
case Instruction::Switch:
break;
case Instruction::Br:
case Instruction::Select:
case Instruction::IndirectBr:
case Instruction::Invoke:
case Instruction::Resume:
case Instruction::Unreachable:
case Instruction::CleanupRet:
case Instruction::CatchRet:
case Instruction::CatchSwitch:
case Instruction::CallBr:
case Instruction::Fence:
case Instruction::AtomicCmpXchg:
case Instruction::AtomicRMW:
case Instruction::PtrToInt:
case Instruction::IntToPtr:
case Instruction::AddrSpaceCast:
case Instruction::CleanupPad:
case Instruction::CatchPad:
case Instruction::UserOp1:
case Instruction::UserOp2:
case Instruction::VAArg:
case Instruction::ExtractElement:
case Instruction::InsertElement:
case Instruction::ShuffleVector:
case Instruction::ExtractValue:
case Instruction::InsertValue:
case Instruction::LandingPad:
case Instruction::Freeze:
break;
default:
break;
}
}
}
return;
}
}
44 changes: 44 additions & 0 deletions src/newton/newton-irPass-LLVMIR-emitAssume.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
/*
Authored 2022. Pei Mu.
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
* Redistributions of source code must retain the above
copyright notice, this list of conditions and the following
disclaimer.
* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials
provided with the distribution.
* Neither the name of the author nor the names of its
contributors may be used to endorse or promote products
derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.
*/

#include "newton-irPass-LLVMIR-rangeAnalysis.h"

#ifdef __cplusplus
extern "C"
{
#endif /* __cplusplus */

void
constantSubstitution(State * N, BoundInfo * boundInfo, llvm::Function & llvmIrFunction);

#ifdef __cplusplus
} /* extern "C" */
#endif /* __cplusplus */

0 comments on commit 037939f

Please sign in to comment.