Optimisations in generated code with function pointers

regression/goto-analyzer/fp-removal1/main.c

@@ -0,0 +1,27 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = f2;
+  fp();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f2();
+--
+^warning: ignoring

regression/goto-analyzer/fp-removal10/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+void_fp fp_tbl[] = {f2, f3, f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(void_fp fp, int i){
+  fp_tbl[2] = fp;
+  void_fp fp2 = fp_tbl[2];
+  fp2();
+}
+
+void main(){
+   for(int i=0;i<3;i++){
+     func(fp_all[i+3], i);
+   }
+}

regression/goto-analyzer/fp-removal10/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/fp-removal11/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(){
+  void_fp * const fp_tbl= malloc(sizeof(void_fp) * 3);
+  fp_tbl[0]=f2;
+  fp_tbl[1]=f3;
+  fp_tbl[2]=f4;
+  void_fp fp = fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal11/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/fp-removal12/main.c

@@ -0,0 +1,38 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+typedef struct fp_container
+{
+  const void_fp fp_tbl[3];
+} fp_container;
+
+
+
+void func(){
+  fp_container container = { .fp_tbl = {f2 ,f3, f4} };
+  fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
+  // Illegal:
+  // container = container2;
+  void_fp fp = container.fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal12/test.desc

@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476

regression/goto-analyzer/fp-removal13/main.c

@@ -0,0 +1,40 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+typedef struct fp_container
+{
+  void_fp fp_tbl[3];
+} fp_container;
+
+
+
+void func(){
+  const fp_container container = { .fp_tbl = {f2 ,f3, f4} };
+  fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
+  const void_fp alternatate_fp_tbl[] = {f5 ,f6, f7};
+  // Illegal:
+  // container = container2;
+  // container.fp_tbl = alternatate_fp_tbl;
+  void_fp fp = container.fp_tbl[1];
+  fp();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal13/test.desc

@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476

regression/goto-analyzer/fp-removal14/main.c

@@ -0,0 +1,28 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(){
+  const void_fp fp = f3;
+  const void_fp* p2fp = &fp;
+  (*p2fp)();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal14/test.desc

@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*f3();$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test is marked as a KNOWNBUG as it is possible for the function
+pointer to be optimized away. Currently goto-analyzer falls back to
+assuming it could be any type compatible function.
+
+Issue: https://github.com/diffblue/cbmc/issues/476

regression/goto-analyzer/fp-removal15/main.c

@@ -0,0 +1,28 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  void_fp fp = f2;
+  fp = f3;
+  fp();
+}
+
+void main(){
+  func();
+}

regression/goto-analyzer/fp-removal15/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--show-goto-functions
+
+^Removing function pointers and virtual functions$
+^\s*IF fp == f1 THEN GOTO 1$
+^\s*IF fp == f2 THEN GOTO 2$
+^\s*IF fp == f3 THEN GOTO 3$
+^\s*IF fp == f4 THEN GOTO 4$
+^\s*IF fp == f5 THEN GOTO 5$
+^\s*IF fp == f6 THEN GOTO 6$
+^\s*IF fp == f7 THEN GOTO 7$
+^\s*IF fp == f8 THEN GOTO 8$
+^\s*IF fp == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-analyzer/fp-removal16/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i", 1); }
+void f2 (void) { printf("%i", 2); }
+void f3 (void) { printf("%i", 3); }
+void f4 (void) { printf("%i", 4); }
+void f5 (void) { printf("%i", 5); }
+void f6 (void) { printf("%i", 6); }
+void f7 (void) { printf("%i", 7); }
+void f8 (void) { printf("%i", 8); }
+void f9 (void) { printf("%i", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = f2;
+  const void_fp fp3 = f4;
+  void_fp fp2 = fp;
+  fp2 = fp3;
+  fp2();
+}
+
+void main()
+{
+  func();
+}

regression/goto-analyzer/fp-removal16/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--show-goto-functions
+^Removing function pointers and virtual functions$
+^\s*IF fp2 == f1 THEN GOTO 1$
+^\s*IF fp2 == f2 THEN GOTO 2$
+^\s*IF fp2 == f3 THEN GOTO 3$
+^\s*IF fp2 == f4 THEN GOTO 4$
+^\s*IF fp2 == f5 THEN GOTO 5$
+^\s*IF fp2 == f6 THEN GOTO 6$
+^\s*IF fp2 == f7 THEN GOTO 7$
+^\s*IF fp2 == f8 THEN GOTO 8$
+^\s*IF fp2 == f9 THEN GOTO 9$
+^SIGNAL=0$
+--
+^warning: ignoring