make arguments to ban constant propagation and assume propagation separately (eb5eb4de) · Commits · Adéla Štěpková / reverser

include/options.hpp

+35 −9

Original line number	Diff line number	Diff line
		#pragma once

		#include <string_view>

		struct Options {
		bool customSimplify = true;
		bool constProp = true;
		bool assumeProp = true;
		bool standardizeFunc = true;
		bool LLVMOptimize = true;
		bool silentMode = true;
		bool silentMode = true; // do not print reversed program to stdout
		bool svComp = false;
		bool printStatus = true;

		Options(bool customSimpl, bool stdFunc, bool LLVMOpt, bool silent, bool svC,
		bool status)
		: customSimplify(customSimpl),
		Options(bool noCustomSimpl, bool noAssumeProp, bool noConstProp, bool stdFunc, bool LLVMOpt,
		bool silent, bool setSvComp, bool status)
		: constProp(!(noCustomSimpl \|\| noConstProp)),
		assumeProp(!(noCustomSimpl \|\| noAssumeProp)),
		standardizeFunc(stdFunc),
		LLVMOptimize(LLVMOpt),
		silentMode(silent),
		svComp(svC),
		svComp(setSvComp),
		printStatus(status)
		{
		if (svComp) {
		@@ -22,8 +26,15 @@ struct Options {
		}

		// override if specified
		if (!customSimpl) {
		customSimplify = false;
		if (noCustomSimpl) {
		assumeProp = false;
		constProp = false;
		}
		if (noAssumeProp) {
		assumeProp = false;
		}
		if (noConstProp) {
		constProp = false;
		}
		if (!stdFunc) {
		standardizeFunc = false;
		@@ -36,11 +47,26 @@ struct Options {
		}
		}

		void printSettings()
		{
		outs() << "Use custom optimization - constant propagation: " << boolToStr(constProp) << "\n";
		outs() << "Use custom optimization - assume propagation: " << boolToStr(assumeProp) << "\n";
		outs() << "Transform inner representation of functions into standard form: "
		<< boolToStr(standardizeFunc) << "\n";
		outs() << "Use LLVM optimizations in postprocessing: " << boolToStr(LLVMOptimize) << "\n";
		outs() << "Print reversed program to output: " << boolToStr(!silentMode) << "\n";
		outs() << "Use SV-COMP settings: " << boolToStr(svComp) << "\n";
		outs() << "Print current status of computation: " << boolToStr(printStatus) << "\n";
		}

		private:
		std::string_view boolToStr(bool value) { return value ? "true" : "false"; }

		void setSVComp()
		{
		silentMode = true;
		customSimplify = true;
		constProp = true;
		assumeProp = true;
		standardizeFunc = true;
		LLVMOptimize = true;
		printStatus = true;

include/passes/passes.hpp

+2 −1

Original line number	Diff line number	Diff line
		@@ -19,6 +19,7 @@ void addReturn(ModuleBundle& mod);
		void makePHIComplete(ModuleBundle& mod);
		void startFromFailedAssert(ModuleBundle& mod);
		void standardizeUtilities(ReversedModule& mod, PassDriver& driver);
		void simplifyAssumes(ReversedModule& mod, PassDriver& driver);
		void simplifyAssumes(ReversedModule& mod, PassDriver& driver, bool propagateConstants,
		bool moveUpAssumes);
		void simplifyMemoryOps(ReversedModule& mod, PassDriver& driver);
		void removeUnusedNondetCalls(llvm::Module& revModule);
		No newline at end of file

main.cpp

+18 −6

Original line number	Diff line number	Diff line
		@@ -16,7 +16,8 @@ using namespace llvm;

		cl::OptionCategory ReverserCategory("Reverser Options");

		static void printReverserVersion(llvm::raw_ostream& out) {
		static void printReverserVersion(llvm::raw_ostream& out)
		{
		out << "reverser version 1.0.3\n";
		out << " using LLVM " << LLVM_VERSION_STRING << "\n";
		}
		@@ -51,6 +52,15 @@ int main(int argc, char** argv)
		"constant propagation, assume propagation)"),
		cl::init(false), cl::cat(ReverserCategory));

		cl::opt<bool> noAssumeProp("no-assume-prop",
		cl::desc("do not run custom optimization: assume propagation"),
		cl::init(false), cl::cat(ReverserCategory));

		cl::opt<bool> noConstantProp("no-const-prop",
		cl::desc("do not run custom optimization: backward "
		"constant propagation"),
		cl::init(false), cl::cat(ReverserCategory));

		cl::opt<bool> noStdFunc("no-std-func",
		cl::desc("keep the inner representation of asserts and nondets"),
		cl::init(false), cl::cat(ReverserCategory));
		@@ -59,8 +69,8 @@ int main(int argc, char** argv)
		cl::desc("do not run LLVM optimizations in postprocessing"),
		cl::init(false), cl::cat(ReverserCategory));

		cl::opt<bool> print("print", cl::desc("print result to stdout"),
		cl::init(false), cl::cat(ReverserCategory));
		cl::opt<bool> print("print", cl::desc("print result to stdout"), cl::init(false),
		cl::cat(ReverserCategory));

		cl::opt<bool> status("status", cl::desc("show the current status during computation"),
		cl::init(false), cl::cat(ReverserCategory));
		@@ -77,7 +87,9 @@ int main(int argc, char** argv)
		return ReturnValue::CANNOT_OPEN_INPUT;
		}

		Options options(!noCustomSimplify, !noStdFunc, !noLLVMOpt, !print, svComp, status);
		Options options(noCustomSimplify, noAssumeProp, noConstantProp, !noStdFunc, !noLLVMOpt, !print,
		svComp, status);
		options.printSettings();

		// Reverse
		auto reverser = ModuleReverser(module.get(), options);

src/moduleReverser.cpp

+17 −13

Original line number	Diff line number	Diff line
		@@ -35,6 +35,9 @@ void ModuleReverser::runPreprocessingPasses()
		void ModuleReverser::runPostprocessLLVMPasses(Module& revModule)
		{
		if (!options.LLVMOptimize) {
		if (options.printStatus) {
		outs() << "INFO: skipping postprocessing\n";
		}
		return;
		}

		@@ -44,6 +47,10 @@ void ModuleReverser::runPostprocessLLVMPasses(Module& revModule)
		// DCEPass does not remove unused calls to __VERIFIER_nondet_...(), because it does not consider
		// them pure (they need to be non-pure so that GVNPass does not merge multiple calls into one)
		removeUnusedNondetCalls(revModule);

		if (options.printStatus) {
		outs() << "INFO: finished postprocessing\n";
		}
		}

		void ModuleReverser::preprocessOrigModule()
		@@ -129,7 +136,7 @@ void ModuleReverser::runCustomSimplifications(ReversedModule& mod)
		{
		PassDriver driver(mod.revModule);

		if (options.customSimplify) {
		if (options.assumeProp \|\| options.constProp) {
		// outs() << mod.revModule << '\n';
		// verifyModule(mod.revModule, &errs()) ? outs() << "broken\n" : outs() << "correct\n";
		driver.preprocessForCustomOpt();
		@@ -139,14 +146,14 @@ void ModuleReverser::runCustomSimplifications(ReversedModule& mod)
		// simplifyMemoryOps(mod, driver);
		driver.mem2Reg();
		if (options.printStatus) {
		outs() << "INFO: finished memory simplification\n";
		outs() << "INFO: finished mem2reg pass before custom optimizations\n";
		}
		// outs() << mod.revModule << '\n';
		simplifyAssumes(mod, driver);
		simplifyAssumes(mod, driver, options.constProp, options.assumeProp);
		// outs() << mod.revModule << '\n';
		if (options.printStatus) {
		outs() << "INFO: finished assume simplification\n";
		}
		else if (options.printStatus) {
		outs() << "INFO: skipping custom optimizations\n";
		}

		if (options.standardizeFunc) {
		@@ -155,8 +162,8 @@ void ModuleReverser::runCustomSimplifications(ReversedModule& mod)

		addNames(mod.revModule, "n");

		if (options.printStatus) {
		outs() << "INFO: finished custom postprocessing\n";
		if ((options.assumeProp \|\| options.constProp) && options.printStatus) {
		outs() << "INFO: finished custom optimizations\n";
		}
		}

		@@ -173,7 +180,8 @@ std::unique_ptr<Module> ModuleReverser::reverseAndCustomSimplify()
		return std::move(revModule);
		}

		void ModuleReverser::cloneModuleHeader(Module* revModule) {
		void ModuleReverser::cloneModuleHeader(Module* revModule)
		{
		revModule->setTargetTriple(origModule->getTargetTriple());
		revModule->setDataLayout(origModule->getDataLayout());
		revModule->setSourceFileName(origModule->getSourceFileName());
		@@ -218,9 +226,5 @@ std::unique_ptr<Module> ModuleReverser::run()

		runPostprocessLLVMPasses(*revModule); // run existing LLVM passes

		if (options.printStatus) {
		outs() << "INFO: finished postprocessing\n";
		}

		return std::move(revModule);
		}

src/passes/simplifyAssumes.cpp

+17 −12

Original line number	Diff line number	Diff line
		@@ -456,7 +456,8 @@ private:
		auto* currentBB = inst->getParent();
		if (assumeHasEffect(origAssume, currentBB, valToReplace)) {
		if (auto* useI = dyn_cast<Instruction>(use)) {
		// outs() << "REPLACING USE " << *use << " DEFINED IN " << useI->getParent()->getName()
		// outs() << "REPLACING USE " << *use << " DEFINED IN " <<
		// useI->getParent()->getName()
		// << " BY " << *replaceWith << " IN " << currentBB->getName()
		// << " WITH ASSUME IN " << origAssume->getParent()->getName() << '\n';
		}
		@@ -989,7 +990,7 @@ void buildVDT(Function* revFunction, const LoopInfo& LI, VirtualDT& VDT)
		}

		void simplifyAssumesInFunction(ReversedModule& mod, Function* revFunction, Function* assumei1,
		PassDriver& driver)
		PassDriver& driver, bool propagateConstants, bool moveUpAssumes)
		{
		DominatorTree& DT = driver.getDominatorTree(*revFunction);
		PostDominatorTree& PDT = driver.getPostDominatorTree(*revFunction);
		@@ -1006,21 +1007,25 @@ void simplifyAssumesInFunction(ReversedModule& mod, Function* revFunction, Funct

		SamePathBlocks samePathBlocks(*revFunction, DT, PDT, LI, VDT);

		if (propagateConstants) {
		SimplifyAssumeVisitor simplifyAssumeVisitor(mod, revFunction, assumei1, DT, PDT, LI,
		samePathBlocks, VDT);
		// outs() << revFunction->getName();
		simplifyAssumeVisitor.visit(revFunction);
		simplifyAssumeVisitor.handle();
		}

		if (moveUpAssumes) {
		MoveUpAssumeVisitor moveUpAssumeVisitor(mod, *revFunction, DT, PDT, LI, samePathBlocks);

		moveUpAssumeVisitor.visit(revFunction);
		moveUpAssumeVisitor.handle();
		}

		driver.invalidateNonCFGAnalyses(*revFunction);
		}

		void simplifyAssumes(ReversedModule& mod, PassDriver& driver)
		void simplifyAssumes(ReversedModule& mod, PassDriver& driver, bool propagateConstants, bool moveUpAssumes)
		{
		auto* assumei1 =
		mod.functionsBuilder.getAssumePlaceholder(Type::getInt1Ty(mod.revModule.getContext()));
		@@ -1030,6 +1035,6 @@ void simplifyAssumes(ReversedModule& mod, PassDriver& driver)
		continue;
		}

		simplifyAssumesInFunction(mod, &F, assumei1, driver);
		simplifyAssumesInFunction(mod, &F, assumei1, driver, propagateConstants, moveUpAssumes);
		}
		}
		No newline at end of file