Merge pull request #262 from danpoe/goto-function-inlining

Goto function inlining

Author: Daniel Kroening

regression/Makefile

@@ -1,4 +1,5 @@
-DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind goto-analyzer
+
+DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind goto-analyzer inlining
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

regression/inlining/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@./test.sh
+
+tests.log: ../test.pl
+	@./test.sh
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find . -name '*.*~' | xargs rm -f
+	find . -name '*.out' | xargs rm -f
+	find . -name '*.o' | xargs rm -f
+	rm -f tests.log	

regression/inlining/chain.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -e
+
+src=../../../src
+goto_cc=$src/goto-cc/goto-cc
+goto_instrument=$src/goto-instrument/goto-instrument
+cbmc=$src/cbmc/cbmc
+
+name=${@:$#}
+name=${name%.c}
+
+args=${@:1:$#-1}
+
+$goto_cc -o $name.o $name.c
+$goto_instrument $args $name.o $name-new.o
+$goto_instrument --show-goto-functions $name-new.o
+$cbmc $name-new.o
+

regression/inlining/inline_01/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int x;
+
+int h() {
+  return 9;
+}
+
+void g(int i) {
+  x += i + h(); // += 12
+}
+
+void f(int i, int j) {
+  g(i);
+  x += i + j; // +=10
+}
+
+int main()
+{
+  x = 0;
+  f(3, 7);
+  assert(x == 22);
+}
+

regression/inlining/inline_01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+f[(].*[)];$
+g[(].*[)];$
+h[(].*[)];$
+^warning: ignoring

regression/inlining/inline_02/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int x;
+
+int h() {
+  return 9;
+}
+
+void g(int i) {
+  x += i + h(); // += 12
+}
+
+void f(int i, int j) {
+  g(i);
+  x += i + j; // +=10
+}
+
+int main()
+{
+  x = 0;
+  f(3, 7);
+  assert(x == 22);
+}
+

regression/inlining/inline_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--partial-inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+f[(].*[)];$
+g[(].*[)];$
+h[(].*[)];$
+--
+^warning: ignoring

regression/inlining/inline_03/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int x;
+
+inline int h() {
+  return 9;
+}
+
+void g(int i) {
+  x += i + h(); // += 12
+}
+
+void f(int i, int j) {
+  g(i);
+  x += i + j; // +=10
+}
+
+int main()
+{
+  x = 0;
+  f(3, 7);
+  assert(x == 22);
+}
+

regression/inlining/inline_03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--partial-inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+f[(].*[)];$
+g[(].*[)];$
+--
+h[(].*[)];$
+^warning: ignoring

regression/inlining/inline_04/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int x;
+
+int h() {
+  return 9;
+}
+
+void g(int i) {
+  x += i + h(); // += 12
+}
+
+void f(int i, int j) {
+  g(i);
+  x += i + j; // +=10
+}
+
+void other_func() {}
+
+int main()
+{
+  x = 0;
+  f(3, 7);
+  other_func();
+  
+  assert(x == 22);
+}
+

regression/inlining/inline_04/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--function-inline main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+g[(].*[)];$
+h[(].*[)];$
+--
+f[(].*[)];$
+other_func[(].*[)];$
+^warning: ignoring

regression/inlining/inline_05/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+
+int x;
+
+void f()
+{
+  x += 1;
+
+  if(x < 10)
+    f();
+}
+
+void h()
+{
+  x += 1;
+  if(x < 20)
+    g();
+}
+
+void g()
+{
+  x += 1;
+  h();
+}
+
+int main()
+{
+  // direct recursion
+  x = 0;
+  f();
+  assert(x == 1);
+
+  // indirect recursion
+  x = 0;
+  g();
+  assert(x == 2);
+}
+

regression/inlining/inline_05/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+recursion.*ignored.*[`]f
+recursion.*ignored.*[`]g
+--
+^warning: ignoring

regression/inlining/inline_06/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+
+int x;
+
+inline void f()
+{
+  x += 1;
+
+  if(x < 10)
+    f();
+}
+
+inline void h()
+{
+  x += 1;
+  if(x < 20)
+    g();
+}
+
+inline void g()
+{
+  x += 1;
+  h();
+}
+
+int main()
+{
+  // direct recursion
+  x = 0;
+  f();
+  assert(x == 10);
+
+  // indirect recursion
+  x = 0;
+  g();
+  assert(x == 20);
+}
+

regression/inlining/inline_06/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--partial-inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+recursion.*ignored.*[`]f
+recursion.*ignored.*[`]g
+--
+^warning: ignoring

regression/inlining/inline_07/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+
+int x;
+
+void f()
+{
+  x += 1;
+
+  if(x < 10)
+    f();
+}
+
+void h()
+{
+  x += 1;
+  if(x < 20)
+    g();
+}
+
+void g()
+{
+  x += 1;
+  h();
+}
+
+int main()
+{
+  // direct recursion
+  x = 0;
+  f();
+  assert(x == 1);
+
+  // indirect recursion
+  x = 0;
+  g();
+  assert(x == 2);
+}
+

regression/inlining/inline_07/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--function-inline main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+recursion.*ignored.*[`]f
+recursion.*ignored.*[`]g
+--
+^warning: ignoring

regression/inlining/inline_08/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int x;
+
+int f()
+{
+  if(x)
+    return 1;
+  else
+    return 2;
+
+  return 3;
+}
+
+int main()
+{
+  int y;
+  y = f(); 
+}
+

regression/inlining/inline_08/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--inline
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+y = 1;
+y = 2;
+y = 3;
+--
+^warning: ignoring