Skip to content

Commit

Permalink
init implementation of emitAssume
Browse files Browse the repository at this point in the history 
Addresses #653.
  • Loading branch information
@PeiMu
PeiMu committed May 7, 2023
1 parent 037939f commit a12995c
Show file tree
Hide file tree
Showing 6 changed files with 129 additions and 162 deletions.
46 changes: 46 additions & 0 deletions analysis/statistics/91947db0600ad544577a7cf19fe3c77b123a09c6.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@

changeset: 1483:91947db0600ad544577a7cf19fe3c77b123a09c6
char kNewtonVersion[] = "0.3-alpha-1483 (91947db0600ad544577a7cf19fe3c77b123a09c6) (build 05-07-2023-13:[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)




8 changes: 8 additions & 0 deletions src/newton/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ SOURCES =\
newton-irPass-LLVMIR-shrinkTypeByRange.cpp\
newton-irPass-LLVMIR-quantization.cpp\
newton-irPass-LLVMIR-memoryAlignment.cpp\
newton-irPass-LLVMIR-emitAssume.cpp\


#
Expand Down Expand Up @@ -135,6 +136,7 @@ OBJS =\
newton-irPass-LLVMIR-constantSubstitution.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-shrinkTypeByRange.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-quantization.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-emitAssume.$(OBJECTEXTENSION)\
newton-irPass-invariantSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-piGroupsSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-ipsaBackend.$(OBJECTEXTENSION)\
Expand Down Expand Up @@ -183,6 +185,7 @@ CGIOBJS =\
newton-irPass-LLVMIR-constantSubstitution.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-shrinkTypeByRange.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-quantization.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-emitAssume.$(OBJECTEXTENSION)\
newton-irPass-invariantSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-piGroupsSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-estimatorSynthesisBackend/$(OBJECTEXTENSION)\
Expand Down Expand Up @@ -230,6 +233,7 @@ LIBNEWTONOBJS =\
newton-irPass-LLVMIR-constantSubstitution.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-shrinkTypeByRange.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-quantization.$(OBJECTEXTENSION)\
newton-irPass-LLVMIR-emitAssume.$(OBJECTEXTENSION)\
newton-irPass-invariantSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-piGroupsSignalAnnotation.$(OBJECTEXTENSION)\
newton-irPass-ipsaBackend.$(OBJECTEXTENSION)\
Expand Down Expand Up @@ -369,6 +373,10 @@ newton-irPass-LLVMIR-memoryAlignment.$(OBJECTEXTENSION): newton-irPass-LLVMIR-me
$(CXX) $(FLEXFLAGS) $(INCDIRS) $(CXXFLAGS) $(WFLAGS) $(OPTFLAGS) $(LINTFLAGS) $<
$(CXX) $(FLEXFLAGS) $(INCDIRS) $(CXXFLAGS) $(WFLAGS) $(OPTFLAGS) $<

newton-irPass-LLVMIR-emitAssume.$(OBJECTEXTENSION): newton-irPass-LLVMIR-emitAssume.cpp
$(CXX) $(FLEXFLAGS) $(INCDIRS) $(CXXFLAGS) $(WFLAGS) $(OPTFLAGS) $(LINTFLAGS) $<
$(CXX) $(FLEXFLAGS) $(INCDIRS) $(CXXFLAGS) $(WFLAGS) $(OPTFLAGS) $<

version.c: $(HEADERS) Makefile
echo 'char kNewtonVersion[] = "0.3-alpha-'`git rev-list --count HEAD`' ('`git rev-parse HEAD`') (build '`date '+%m-%d-%Y-%H:%M'`-`whoami`@`hostname -s`-`uname -s`-`uname -r`-`uname -m`\)\"\; > version.c

Expand Down
153 changes: 60 additions & 93 deletions src/newton/newton-irPass-LLVMIR-emitAssume.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,43 +29,29 @@
POSSIBILITY OF SUCH DAMAGE.
*/

#include "newton-irPass-LLVMIR-constantSubstitution.h"
#include "newton-irPass-LLVMIR-emitAssume.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
* emit a `llvm.assume` after each instruction if its range can be analyzed
* */
void
constantSubstitution(State * N, BoundInfo * boundInfo, llvm::Function & llvmIrFunction)
emitAssume(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())
{
/*
* only emit after the instruction that is not supported by builtin_assume
* */
case Instruction::Call:
break;
case Instruction::Add:
case Instruction::FAdd:
case Instruction::Sub:
Expand Down Expand Up @@ -97,91 +83,72 @@ constantSubstitution(State * N, BoundInfo * boundInfo, llvm::Function & llvmIrFu
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))) {
case Instruction::PHI: {
auto vrIt = boundInfo->virtualRegisterRange.find(llvmIrInstruction);
if (vrIt == boundInfo->virtualRegisterRange.end()) {
break;
}
IRBuilder<> Builder(&llvmIrBasicBlock);
Builder.SetInsertPoint(llvmIrInstruction->getNextNode());

Function* assumeIntrinsic = Intrinsic::getDeclaration(
llvmIrFunction.getParent(), Intrinsic::assume
);
/*
* if it's a pointer, skip it
* 1. get lower/upper bound from map
* 2. check lower bound <= upper bound
* 3. icmp for INT comparison; fcmp for FP comparison
* */
if (llvmIrInstruction->getType()->isPointerTy())
{
auto lowerBound = vrIt->second.first;
auto upperBound = vrIt->second.second;
if (lowerBound > upperBound) {
/*if this happens, there might be a bug*/
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;
/*
* The excepted code is:
* block_a:
* %cmp1 = cmpInst
* br i1 %cmp1, label %block_b, label %block_c
*
* block_b:
* %cmp2 = cmpInst
* br label %block_c
*
* block_c:
* %v = phi i1 [false, %block_a], [%cmp2, %block_b]
* call void @llvm.assume(i1 %v)
* */
Value *assumeLowerCond, *assumeUpperCond;
Type *instType = llvmIrInstruction->getType();
if (instType->isFloatTy() || instType->isDoubleTy()) {
assumeLowerCond = Builder.CreateFCmpOGE(llvmIrInstruction,
ConstantFP::get(instType, lowerBound));
assumeUpperCond = Builder.CreateFCmpOLE(llvmIrInstruction,
ConstantFP::get(instType, upperBound));
} else {
if (lowerBound < 0) {
assumeLowerCond = Builder.CreateICmpSGE(llvmIrInstruction,
ConstantInt::get(instType, (int)lowerBound, true));
assumeUpperCond = Builder.CreateICmpSLE(llvmIrInstruction,
ConstantInt::get(instType, (int)upperBound, true));
} else {
assumeLowerCond = Builder.CreateICmpUGE(llvmIrInstruction,
ConstantInt::get(instType, (int)lowerBound, false));
assumeUpperCond = Builder.CreateICmpULE(llvmIrInstruction,
ConstantInt::get(instType, (int)upperBound, false));
}
}
auto assumeCond = Builder.CreateLogicalAnd(assumeLowerCond, assumeUpperCond);
Value* assumeInst = Builder.CreateCall(assumeIntrinsic, assumeCond);
}
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:
Expand Down
2 changes: 1 addition & 1 deletion src/newton/newton-irPass-LLVMIR-emitAssume.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ extern "C"
#endif /* __cplusplus */

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

#ifdef __cplusplus
} /* extern "C" */
Expand Down
81 changes: 13 additions & 68 deletions src/newton/newton-irPass-LLVMIR-optimizeByRange.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
#include "newton-irPass-LLVMIR-shrinkTypeByRange.h"
#include "newton-irPass-LLVMIR-quantization.h"
#include "newton-irPass-LLVMIR-memoryAlignment.h"
#include "newton-irPass-LLVMIR-emitAssume.h"
#endif /* __cplusplus */

#include <algorithm>
Expand Down Expand Up @@ -378,74 +379,18 @@ irPassLLVMIROptimizeByRange(State * N)
collectCalleeInfo(calleeNames, funcBoundInfo, boundInfo);
}

/*
* simplify the condition of each branch
* */
flexprint(N->Fe, N->Fm, N->Fpinfo, "simplify control flow by range\n");
for (auto & mi : *Mod)
{
auto boundInfoIt = funcBoundInfo.find(mi.getName().str());
if (boundInfoIt != funcBoundInfo.end())
{
simplifyControlFlow(N, boundInfoIt->second, mi);
}
// else
// {
// assert(false);
// }
}

legacy::PassManager passManager;
passManager.add(createCFGSimplificationPass());
passManager.add(createInstSimplifyLegacyPass());
passManager.add(createGlobalDCEPass());
passManager.run(*Mod);

/*
* remove the functions that are optimized by passes.
* */
if (useOverLoad)
cleanFunctionMap(Mod, callerMap);

if (useOverLoad)
overloadFunc(Mod, callerMap);

flexprint(N->Fe, N->Fm, N->Fpinfo, "infer bound\n");
callerMap.clear();
funcBoundInfo.clear();
useOverLoad = false;
for (auto & mi : *Mod)
{
auto boundInfo = new BoundInfo();
mergeBoundInfo(boundInfo, globalBoundInfo);
rangeAnalysis(N, mi, boundInfo, callerMap, typeRange, virtualRegisterVectorRange, useOverLoad);
funcBoundInfo.emplace(mi.getName().str(), boundInfo);
std::vector<std::string> calleeNames;
collectCalleeInfo(calleeNames, funcBoundInfo, boundInfo);
}

flexprint(N->Fe, N->Fm, N->Fpinfo, "constant substitution\n");
for (auto & mi : *Mod)
{
auto boundInfoIt = funcBoundInfo.find(mi.getName().str());
if (boundInfoIt != funcBoundInfo.end())
{
constantSubstitution(N, boundInfoIt->second, mi);
}
// else
// {
// assert(false);
// }
}

/*
* remove the functions that are optimized by passes.
* */
if (useOverLoad)
cleanFunctionMap(Mod, callerMap);

if (useOverLoad)
overloadFunc(Mod, callerMap);
flexprint(N->Fe, N->Fm, N->Fpinfo, "emit builtin_assume intrinsic\n");
for (auto & mi : *Mod)
{
auto boundInfoIt = funcBoundInfo.find(mi.getName().str());
if (boundInfoIt != funcBoundInfo.end()) {
emitAssume(N, boundInfoIt->second, mi);
}
// else
// {
// assert(false);
// }
}

/*
* Dump BC file to a file.
Expand Down
1 change: 1 addition & 0 deletions src/newton/newton-irPass-LLVMIR-rangeAnalysis.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@
#include "llvm/IR/IRBuilder.h"
#include "llvm/IR/Instructions.h"
#include "llvm/IR/InstIterator.h"
#include "llvm/IR/IntrinsicInst.h"
#include "llvm/IR/Value.h"
#include "llvm/IRReader/IRReader.h"
#include "llvm/Support/SourceMgr.h"
Expand Down

0 comments on commit a12995c

Please sign in to comment.