From b7eaa99578037789a337c5061c0ea8ee3150b63c Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Thu, 1 Nov 2012 18:06:13 +1100 Subject: A bunch of fixes to the solver, and moving it in to clang. Also some contribution writing stuff. Basically: lots of work. --- impl/test/1.eqns | 2 +- impl/test/10.soln | 10 +++++----- impl/test/7.soln | 4 ++-- impl/test/8.soln | 2 +- impl/test/9.soln | 4 ++-- impl/test/run | 6 ++++-- 6 files changed, 15 insertions(+), 13 deletions(-) (limited to 'impl/test') diff --git a/impl/test/1.eqns b/impl/test/1.eqns index 0cdfd24..34c51de 100644 --- a/impl/test/1.eqns +++ b/impl/test/1.eqns @@ -1,3 +1,3 @@ -x = max(0, min(-1 + x, y)) y = max(0, 5 + x, x) z = max(0, 1 + z, 0 + x) +x = max(0, min(-1 + x, y)) diff --git a/impl/test/10.soln b/impl/test/10.soln index 20a47ca..238b7d5 100644 --- a/impl/test/10.soln +++ b/impl/test/10.soln @@ -1,9 +1,9 @@ -x = 0 -w = 0 -y = 0 -z = 0 -u = 0 a = 0 b = 0 c = 0 d = 0 +u = 0 +w = 0 +x = 0 +y = 0 +z = 0 diff --git a/impl/test/7.soln b/impl/test/7.soln index 0d85468..2c9b183 100644 --- a/impl/test/7.soln +++ b/impl/test/7.soln @@ -1,8 +1,8 @@ -x = 0 -y = 0 a = 0 b = 0 c = 0 d = 0 e = 0 f = 0 +x = 0 +y = 0 diff --git a/impl/test/8.soln b/impl/test/8.soln index 1945057..73d26df 100644 --- a/impl/test/8.soln +++ b/impl/test/8.soln @@ -1,4 +1,4 @@ -x = 0 w = 0 +x = 0 y = 0 z = 0 diff --git a/impl/test/9.soln b/impl/test/9.soln index 616c5e5..7116cf4 100644 --- a/impl/test/9.soln +++ b/impl/test/9.soln @@ -1,5 +1,5 @@ -x = 0 +u = 0 w = 0 +x = 0 y = 0 z = 0 -u = 0 diff --git a/impl/test/run b/impl/test/run index 169edda..d15fb68 100644 --- a/impl/test/run +++ b/impl/test/run @@ -7,15 +7,17 @@ FAILED=0 echo "Testing binary: $1 in directory $DIR" while [ -f "$DIR/$NUM.eqns" ] do + cat "$DIR/$NUM.soln" | sort > "/tmp/$NUM.soln.tmp" + mv "/tmp/$NUM.soln.tmp" "$DIR/$NUM.soln" 2> /dev/null OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns" 2> /dev/null) if [ $? -eq 124 ]; then OUTPUT="did not terminate" fi - DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln") + DIFF=$(echo "$OUTPUT" | sort | diff - "$DIR/$NUM.soln") if [ ! -z "$DIFF" ]; then echo "==================" echo "Test #$NUM failed:" - echo "$OUTPUT" | sdiff - "$DIR/$NUM.soln" + echo "$OUTPUT" | sort | sdiff - "$DIR/$NUM.soln" echo FAILED=$(($FAILED + 1)) fi -- cgit v1.2.3 From ff5ec13849a69ef4a53bab009eed880456931a14 Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Thu, 1 Nov 2012 20:02:14 +1100 Subject: Fixing up some equation system stuff. Adding function arguments to the system, as well as making it slightly easier to read. --- clang/include/clang/Analysis/Analyses/.#Interval.h | 1 - .../clang/Analysis/Analyses/.#Interval_flymake.h | 1 - clang/include/clang/Analysis/Analyses/Interval.h | 2 +- clang/lib/Analysis/Interval.cpp | 34 ++++++++++++++++++---- .../lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp | 1 - clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp | 2 +- impl/test/14.eqns | 3 ++ impl/test/14.soln | 3 ++ 8 files changed, 36 insertions(+), 11 deletions(-) delete mode 120000 clang/include/clang/Analysis/Analyses/.#Interval.h delete mode 120000 clang/include/clang/Analysis/Analyses/.#Interval_flymake.h delete mode 120000 clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp create mode 100644 impl/test/14.eqns create mode 100644 impl/test/14.soln (limited to 'impl/test') diff --git a/clang/include/clang/Analysis/Analyses/.#Interval.h b/clang/include/clang/Analysis/Analyses/.#Interval.h deleted file mode 120000 index 235903b..0000000 --- a/clang/include/clang/Analysis/Analyses/.#Interval.h +++ /dev/null @@ -1 +0,0 @@ -carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043 \ No newline at end of file diff --git a/clang/include/clang/Analysis/Analyses/.#Interval_flymake.h b/clang/include/clang/Analysis/Analyses/.#Interval_flymake.h deleted file mode 120000 index 235903b..0000000 --- a/clang/include/clang/Analysis/Analyses/.#Interval_flymake.h +++ /dev/null @@ -1 +0,0 @@ -carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043 \ No newline at end of file diff --git a/clang/include/clang/Analysis/Analyses/Interval.h b/clang/include/clang/Analysis/Analyses/Interval.h index 6c0d5cf..8bb8d0f 100644 --- a/clang/include/clang/Analysis/Analyses/Interval.h +++ b/clang/include/clang/Analysis/Analyses/Interval.h @@ -33,7 +33,7 @@ public: IntervalAnalysis(AnalysisDeclContext &analysisContext); virtual ~IntervalAnalysis(); - void runOnAllBlocks(); + void runOnAllBlocks(const Decl&); static IntervalAnalysis *create(AnalysisDeclContext &analysisContext) { return new IntervalAnalysis(analysisContext); diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index 3a82344..7096d75 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -637,10 +637,16 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { std::vector plusArgs; for (int negate = 0; negate < 2; ++negate) { std::string var_name = negate ? negate_string(variables->first) : variables->first; - std::vector minArgs; - minArgs.push_back(vars[var_name]); - minArgs.push_back(&system.constant(cond[var_name])); - plusArgs.push_back(&system.expression(new Minimum(), minArgs)); + if (cond[var_name] == infinity()) { + plusArgs.push_back(vars[var_name]); + } else if (cond[var_name] == -infinity()) { + plusArgs.push_back(&system.constant(-infinity())); + } else { + std::vector minArgs; + minArgs.push_back(vars[var_name]); + minArgs.push_back(&system.constant(cond[var_name])); + plusArgs.push_back(&system.expression(new Minimum(), minArgs)); + } } std::vector guard_args; @@ -667,15 +673,31 @@ IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context) IntervalAnalysis :: ~IntervalAnalysis() { } -void IntervalAnalysis::runOnAllBlocks() { +void IntervalAnalysis::runOnAllBlocks(const Decl& decl) { const CFG *cfg = this->context->getCFG(); cfg->dump(context->getASTContext().getLangOpts(), llvm::sys::Process::StandardErrHasColors()); - EqnSys system; + EqnSys system; BlockVars block_vars; + std::vector infArg; + infArg.push_back(&system.constant(infinity())); + std::set& function_arguments = block_vars[&cfg->getEntry()]; + std::string block_id = toString(cfg->getEntry().getBlockID()); + if (const FunctionDecl* func = dyn_cast(&decl)) { + for (unsigned int i = func->getNumParams(); i > 0; i--) { + std::string name = func->getParamDecl(i-1)->getNameAsString(); + + function_arguments.insert(name); // add it to the first block's vars + function_arguments.insert(negate_string(name)); // add it to the first block's vars + + system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here + system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here + } + } + std::set seen; std::deque todo; todo.push_back(&cfg->getEntry()); diff --git a/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp deleted file mode 120000 index 235903b..0000000 --- a/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp +++ /dev/null @@ -1 +0,0 @@ -carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043 \ No newline at end of file diff --git a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp index 2f3e155..badb671 100644 --- a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp @@ -14,7 +14,7 @@ public: void checkASTCodeBody(const Decl *D, AnalysisManager& mgr, BugReporter &BR) const { if (IntervalAnalysis *a = mgr.getAnalysis(D)) { - a->runOnAllBlocks(); + a->runOnAllBlocks(*D); } } }; diff --git a/impl/test/14.eqns b/impl/test/14.eqns new file mode 100644 index 0000000..6c28481 --- /dev/null +++ b/impl/test/14.eqns @@ -0,0 +1,3 @@ +x = 0 +y = max(x, z) +z = y + 1 diff --git a/impl/test/14.soln b/impl/test/14.soln new file mode 100644 index 0000000..c0301bb --- /dev/null +++ b/impl/test/14.soln @@ -0,0 +1,3 @@ +x = 0 +y = inf +z = inf -- cgit v1.2.3