diff --git a/COMPILING b/COMPILING index eb30060b262..46c5c791cdc 100644 --- a/COMPILING +++ b/COMPILING @@ -142,7 +142,7 @@ Follow these instructions: 1) You need a SAT solver (in source). We recommend MiniSat2. Using a browser, download from - http://minisat.se/downloads/minisat-2.2.1.tar.gz + http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz and then unpack with diff --git a/regression/ansi-c/gcc_attributes7/main.i b/regression/ansi-c/gcc_attributes7/main.i new file mode 100644 index 00000000000..ddb730cfd32 --- /dev/null +++ b/regression/ansi-c/gcc_attributes7/main.i @@ -0,0 +1,55 @@ +struct X { + int a; +}; + +struct S { + struct X x __attribute__((aligned( +# 81 "ring.h" 3 4 + 16 +# 81 "ring.h" + ))); + struct X x2 __attribute__((aligned( +# 82 "ring.h" 3 4 + ((( +# 82 "ring.h" + sizeof(struct X) +# 82 "ring.h" 3 4 + )+16 -1)&~(16 -1)) +# 82 "ring.h" + ))); +}; + +typedef int int8_t +# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" +__attribute__( +# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" 3 4 +(__mode__ (__QI__)) +# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" +) +# 194 "/usr/include/x86_64-linux-gnu/sys/types.h" 3 4 + ; + +int extundelete_process_dir_block(int fs, + int b +# 29 "block.h" 3 4 + __attribute__( +# 29 "block.h" + (unused) +# 29 "block.h" 3 4 + ) +# 29 "block.h" + , + int ref_offset +# 30 "block.h" 3 4 + __attribute__( +# 30 "block.h" + (unused) +# 30 "block.h" 3 4 + ) +# 30 "block.h" + , + void *priv_data); + +int main() +{ +} diff --git a/regression/ansi-c/gcc_attributes7/test.desc b/regression/ansi-c/gcc_attributes7/test.desc new file mode 100644 index 00000000000..e5548900ad5 --- /dev/null +++ b/regression/ansi-c/gcc_attributes7/test.desc @@ -0,0 +1,8 @@ +CORE +main.i + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile new file mode 100644 index 00000000000..cbdd3378bac --- /dev/null +++ b/regression/cbmc-cover/Makefile @@ -0,0 +1,20 @@ +default: tests.log + +test: + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +tests.log: ../test.pl + @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; diff --git a/regression/cbmc-cover/assertion1/main.c b/regression/cbmc-cover/assertion1/main.c new file mode 100644 index 00000000000..93871ca260d --- /dev/null +++ b/regression/cbmc-cover/assertion1/main.c @@ -0,0 +1,11 @@ +int main() +{ + int input1, input2; + + __CPROVER_assert(!input1, ""); + + if(input1) + { + __CPROVER_assert(!input1, ""); // will work, we ignore the assertion + } +} diff --git a/regression/cbmc-cover/assertion1/test.desc b/regression/cbmc-cover/assertion1/test.desc new file mode 100644 index 00000000000..c9c30e9753d --- /dev/null +++ b/regression/cbmc-cover/assertion1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--cover assertion +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 5 function main: SATISFIED$ +^\[main.assertion.2\] file main.c line 9 function main: SATISFIED$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/branch1/main.c b/regression/cbmc-cover/branch1/main.c new file mode 100644 index 00000000000..f84c00cd074 --- /dev/null +++ b/regression/cbmc-cover/branch1/main.c @@ -0,0 +1,17 @@ +int main() +{ + int input1, input2; + + if(input1) + { + if(input1) // dependent + { + } + } + else + { + if(input2) // independent + { + } + } +} diff --git a/regression/cbmc-cover/branch1/test.desc b/regression/cbmc-cover/branch1/test.desc new file mode 100644 index 00000000000..379f3be82d0 --- /dev/null +++ b/regression/cbmc-cover/branch1/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover branch +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] file main.c line 5 function main function main block 1 branch false: SATISFIED$ +^\[main.2\] file main.c line 5 function main function main block 1 branch true: SATISFIED$ +^\[main.3\] file main.c line 7 function main function main block 2 branch false: FAILED$ +^\[main.4\] file main.c line 7 function main function main block 2 branch true: SATISFIED$ +^\[main.5\] file main.c line 13 function main function main block 4 branch false: SATISFIED$ +^\[main.6\] file main.c line 13 function main function main block 4 branch true: SATISFIED$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/branch2/main.c b/regression/cbmc-cover/branch2/main.c new file mode 100644 index 00000000000..afda13cd004 --- /dev/null +++ b/regression/cbmc-cover/branch2/main.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + int ch; + while((ch=getc(stdin))!=-1) + { + } +} diff --git a/regression/cbmc-cover/branch2/test.desc b/regression/cbmc-cover/branch2/test.desc new file mode 100644 index 00000000000..79093e780b6 --- /dev/null +++ b/regression/cbmc-cover/branch2/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--cover branch --unwind 2 +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] file main.c line 6 function main function main block 2 branch false: SATISFIED +^\[main.2\] file main.c line 6 function main function main block 2 branch true: SATISFIED +-- +^warning: ignoring diff --git a/regression/cbmc-cover/branch3/main.c b/regression/cbmc-cover/branch3/main.c new file mode 100644 index 00000000000..c4446281161 --- /dev/null +++ b/regression/cbmc-cover/branch3/main.c @@ -0,0 +1,20 @@ +#include +#include + +int main() +{ + char ch; + unsigned state=0; + while((ch=getc(stdin))!=-1) + { + switch(state) + { + case 0: if(ch=='<') state=1; else state=0; break; + case 1: if(ch=='h') state=2; else state=0; break; + case 2: if(ch=='t') state=3; else state=0; break; + case 3: if(ch=='m') state=4; else state=0; break; + case 4: if(ch=='l') state=5; else state=0; break; + default:; + } + } +} diff --git a/regression/cbmc-cover/branch3/test.desc b/regression/cbmc-cover/branch3/test.desc new file mode 100644 index 00000000000..0b36798349f --- /dev/null +++ b/regression/cbmc-cover/branch3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover branch --unwind 6 +^EXIT=0$ +^SIGNAL=0$ +^\*\* 22 of 22 covered (100.0%), using .* iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/condition1/main.c b/regression/cbmc-cover/condition1/main.c new file mode 100644 index 00000000000..5043af9a82b --- /dev/null +++ b/regression/cbmc-cover/condition1/main.c @@ -0,0 +1,17 @@ +int main() +{ + int input1, input2; + + if(input1 && input2) + { + } + else if(input1) + { + } + else if(input2) + { + if(input1) // can't be true + { + } + } +} diff --git a/regression/cbmc-cover/condition1/test.desc b/regression/cbmc-cover/condition1/test.desc new file mode 100644 index 00000000000..ac613048d44 --- /dev/null +++ b/regression/cbmc-cover/condition1/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--cover condition +^EXIT=0$ +^SIGNAL=0$ +^\[main.1] file main.c line 5 function main condition .* false: SATISFIED +^\[main.2] file main.c line 5 function main condition .* true: SATISFIED +^\[main.3] file main.c line 5 function main condition .* false: SATISFIED +^\[main.4] file main.c line 5 function main condition .* true: SATISFIED +^\[main.5] file main.c line 8 function main condition .* false: SATISFIED +^\[main.6] file main.c line 8 function main condition .* true: SATISFIED +^\[main.7] file main.c line 11 function main condition .* false: SATISFIED +^\[main.8] file main.c line 11 function main condition .* true: SATISFIED +^\[main.9] file main.c line 13 function main condition .* false: FAILED +^\[main.10] file main.c line 13 function main condition .* true: SATISFIED +^\*\* 9 of 10 covered (90.0%) +-- +^warning: ignoring diff --git a/regression/cbmc-cover/cover1/main.c b/regression/cbmc-cover/cover1/main.c new file mode 100644 index 00000000000..58e813e34e7 --- /dev/null +++ b/regression/cbmc-cover/cover1/main.c @@ -0,0 +1,15 @@ +int main() +{ + int input1, input2; + + __CPROVER_cover(input1); + __CPROVER_cover(!input1); + + if(input1) + { + __CPROVER_cover(!input1); // won't work + } + + // should not produce a goal + __CPROVER_assert(input1, ""); +} diff --git a/regression/cbmc-cover/cover1/test.desc b/regression/cbmc-cover/cover1/test.desc new file mode 100644 index 00000000000..f0c123955bf --- /dev/null +++ b/regression/cbmc-cover/cover1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover cover +^EXIT=0$ +^SIGNAL=0$ +^\[main.1] file main.c line 5 function main condition .*: SATISFIED$ +^\[main.2] file main.c line 6 function main condition .*: SATISFIED$ +^\[main.3] file main.c line 10 function main condition .*: FAILED$ +^\*\* 2 of 3 covered (66.7%), using .* iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/decision1/main.c b/regression/cbmc-cover/decision1/main.c new file mode 100644 index 00000000000..2a14f5d774d --- /dev/null +++ b/regression/cbmc-cover/decision1/main.c @@ -0,0 +1,11 @@ +int main() +{ + int input1, input2, input3; + + if(input1 && input2 && input3) + { + } + else + { + } +} diff --git a/regression/cbmc-cover/decision1/test.desc b/regression/cbmc-cover/decision1/test.desc new file mode 100644 index 00000000000..d275c08f759 --- /dev/null +++ b/regression/cbmc-cover/decision1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover decision +^EXIT=0$ +^SIGNAL=0$ +^\*\* 2 of 2 covered (100.0%), using 2 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/location1/main.c b/regression/cbmc-cover/location1/main.c new file mode 100644 index 00000000000..5553dbe94bc --- /dev/null +++ b/regression/cbmc-cover/location1/main.c @@ -0,0 +1,15 @@ +int main() +{ + int input1; + int x=0; + + if(input1) + { + x=1; + } + + if(input1 && !x) + { + x=2; // I am dead! + } +} diff --git a/regression/cbmc-cover/location1/test.desc b/regression/cbmc-cover/location1/test.desc new file mode 100644 index 00000000000..6e7e7174e48 --- /dev/null +++ b/regression/cbmc-cover/location1/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] file main.c line 3 function main block 1: SATISFIED$ +^\[main.2\] file main.c line 8 function main block 2: SATISFIED$ +^\[main.3\] file main.c line 11 function main block 3: SATISFIED$ +^\[main.4\] file main.c line 13 function main block 4: FAILED$ +^\[main.5\] file main.c line 15 function main block 5: SATISFIED$ +^\*\* 4 of 5 covered (80.0%) +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc1/main.c b/regression/cbmc-cover/mcdc1/main.c new file mode 100644 index 00000000000..11f46cd74e0 --- /dev/null +++ b/regression/cbmc-cover/mcdc1/main.c @@ -0,0 +1,14 @@ +int main() +{ + // Condition and decision coverage can be had with 2 tests, + // but MC/DC needs six (n+1 for n conditions). + + __CPROVER_bool A, B, C, D, E; + + if ((A || B) && C && D && E) + { + } + else + { + } +} diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc new file mode 100644 index 00000000000..83951c6a6e9 --- /dev/null +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\*\* .* of .* covered (100.0%), using 6 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/enum1/enum1$Name.class b/regression/cbmc-java/enum1/enum1$Name.class new file mode 100644 index 00000000000..620ea04a9fe Binary files /dev/null and b/regression/cbmc-java/enum1/enum1$Name.class differ diff --git a/regression/cbmc-java/enum1/enum1.class b/regression/cbmc-java/enum1/enum1.class new file mode 100644 index 00000000000..f5ea86aff39 Binary files /dev/null and b/regression/cbmc-java/enum1/enum1.class differ diff --git a/regression/cbmc-java/enum1/enum1.java b/regression/cbmc-java/enum1/enum1.java new file mode 100644 index 00000000000..4e35155e29c --- /dev/null +++ b/regression/cbmc-java/enum1/enum1.java @@ -0,0 +1,27 @@ +public class enum1 { + + public enum Name { + ASCII(1, String.class), + BIGINT(2, Long.class), + BOOLEAN(3, Boolean.class), + COUNTER(4, Long.class); + + final int protocolId; + final Class javaType; + + private Name(int protocolId, Class javaType) { + this.protocolId = protocolId; + this.javaType = javaType; + } + + }; + + public static void main(String args[]) { + int i = 0; + for (Name t : Name.values()) { + i += t.protocolId; + } + + } +} + diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc new file mode 100644 index 00000000000..15de63a7ead --- /dev/null +++ b/regression/cbmc-java/enum1/test.desc @@ -0,0 +1,8 @@ +CORE +enum1.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-java/function1/Main.class b/regression/cbmc-java/function1/Main.class new file mode 100644 index 00000000000..4cb1cb6f542 Binary files /dev/null and b/regression/cbmc-java/function1/Main.class differ diff --git a/regression/cbmc-java/function1/Main.java b/regression/cbmc-java/function1/Main.java new file mode 100644 index 00000000000..7152318684e --- /dev/null +++ b/regression/cbmc-java/function1/Main.java @@ -0,0 +1,19 @@ + +class Other +{ + public void fail() + { + assert i == 0; + } + + private int i; +} + +public class Main +{ + public static void main(String[] args) + { + Other o = new Other(); + } +} + diff --git a/regression/cbmc-java/function1/Other.class b/regression/cbmc-java/function1/Other.class new file mode 100644 index 00000000000..2ee3eeda9d7 Binary files /dev/null and b/regression/cbmc-java/function1/Other.class differ diff --git a/regression/cbmc-java/function1/test.desc b/regression/cbmc-java/function1/test.desc new file mode 100644 index 00000000000..3800f47f81a --- /dev/null +++ b/regression/cbmc-java/function1/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function "Other.fail:()V" +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/function2/A.class b/regression/cbmc-java/function2/A.class new file mode 100644 index 00000000000..7af0cd759fb Binary files /dev/null and b/regression/cbmc-java/function2/A.class differ diff --git a/regression/cbmc-java/function2/B.class b/regression/cbmc-java/function2/B.class new file mode 100644 index 00000000000..a47436b1232 Binary files /dev/null and b/regression/cbmc-java/function2/B.class differ diff --git a/regression/cbmc-java/function2/C.class b/regression/cbmc-java/function2/C.class new file mode 100644 index 00000000000..8531053409a Binary files /dev/null and b/regression/cbmc-java/function2/C.class differ diff --git a/regression/cbmc-java/function2/D.class b/regression/cbmc-java/function2/D.class new file mode 100644 index 00000000000..02d4e15c990 Binary files /dev/null and b/regression/cbmc-java/function2/D.class differ diff --git a/regression/cbmc-java/function2/Main.class b/regression/cbmc-java/function2/Main.class new file mode 100644 index 00000000000..7d091ce7584 Binary files /dev/null and b/regression/cbmc-java/function2/Main.class differ diff --git a/regression/cbmc-java/function2/Main.java b/regression/cbmc-java/function2/Main.java new file mode 100644 index 00000000000..7ca39a8e703 --- /dev/null +++ b/regression/cbmc-java/function2/Main.java @@ -0,0 +1,34 @@ + +class A +{ + public int i; +} + +class B extends A +{ + public int j; +} + +class C extends B +{ + public int k; +} + +class D +{ + protected C c; + + public void fail() + { + assert c.i == 0 || c.j == 0 || c.k == 0; + } +} + +public class Main +{ + public static void main(String[] args) + { + D d = new D(); + } +} + diff --git a/regression/cbmc-java/function2/test.desc b/regression/cbmc-java/function2/test.desc new file mode 100644 index 00000000000..423018ec7c8 --- /dev/null +++ b/regression/cbmc-java/function2/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function "D.fail:()V" +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/function3/A.class b/regression/cbmc-java/function3/A.class new file mode 100644 index 00000000000..ed5eaf69452 Binary files /dev/null and b/regression/cbmc-java/function3/A.class differ diff --git a/regression/cbmc-java/function3/B.class b/regression/cbmc-java/function3/B.class new file mode 100644 index 00000000000..61ef44f93b6 Binary files /dev/null and b/regression/cbmc-java/function3/B.class differ diff --git a/regression/cbmc-java/function3/Main.class b/regression/cbmc-java/function3/Main.class new file mode 100644 index 00000000000..c6720541977 Binary files /dev/null and b/regression/cbmc-java/function3/Main.class differ diff --git a/regression/cbmc-java/function3/Main.java b/regression/cbmc-java/function3/Main.java new file mode 100644 index 00000000000..e8aac10625c --- /dev/null +++ b/regression/cbmc-java/function3/Main.java @@ -0,0 +1,22 @@ + +class A +{ + public void dummy() {} + + public B b; +} + +class B +{ + public A a; +} + + +public class Main +{ + public static void main(String[] args) + { + B B = new B(); + } +} + diff --git a/regression/cbmc-java/function3/test.desc b/regression/cbmc-java/function3/test.desc new file mode 100644 index 00000000000..d035fa2e0a8 --- /dev/null +++ b/regression/cbmc-java/function3/test.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function "A.dummy:()V" +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/missing_class1/missing_class1.class b/regression/cbmc-java/missing_class1/missing_class1.class new file mode 100644 index 00000000000..9654a6aad1c Binary files /dev/null and b/regression/cbmc-java/missing_class1/missing_class1.class differ diff --git a/regression/cbmc-java/missing_class1/missing_class1.java b/regression/cbmc-java/missing_class1/missing_class1.java new file mode 100644 index 00000000000..7525cdd2867 --- /dev/null +++ b/regression/cbmc-java/missing_class1/missing_class1.java @@ -0,0 +1,16 @@ +class B { + int j; +} + +class A { + int i; + B b; +} + +public class missing_class1 { + public static void main(String[] args) { + A a = new A(); + B b = a.b; + int j = b.j; // NULL pointer dereference + } +} diff --git a/regression/cbmc-java/missing_class1/test.desc b/regression/cbmc-java/missing_class1/test.desc new file mode 100644 index 00000000000..7f9f1a72c0b --- /dev/null +++ b/regression/cbmc-java/missing_class1/test.desc @@ -0,0 +1,8 @@ +CORE +missing_class1.class +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-java/pointer_check1/A.class b/regression/cbmc-java/pointer_check1/A.class new file mode 100644 index 00000000000..a80b733cb82 Binary files /dev/null and b/regression/cbmc-java/pointer_check1/A.class differ diff --git a/regression/cbmc-java/pointer_check1/B.class b/regression/cbmc-java/pointer_check1/B.class new file mode 100644 index 00000000000..09ba3d25408 Binary files /dev/null and b/regression/cbmc-java/pointer_check1/B.class differ diff --git a/regression/cbmc-java/pointer_check1/pointer_check1.class b/regression/cbmc-java/pointer_check1/pointer_check1.class new file mode 100644 index 00000000000..891a91b81f7 Binary files /dev/null and b/regression/cbmc-java/pointer_check1/pointer_check1.class differ diff --git a/regression/cbmc-java/pointer_check1/pointer_check1.java b/regression/cbmc-java/pointer_check1/pointer_check1.java new file mode 100644 index 00000000000..f3a3c312022 --- /dev/null +++ b/regression/cbmc-java/pointer_check1/pointer_check1.java @@ -0,0 +1,21 @@ +class A +{ + int val; +} + +class B +{ + int getVal(A a) + { + return a.val; + } +} + +class pointer_check1 +{ + public static void main(String[] args) + { + B b = new B(); + int myval = b.getVal(null); + } +} diff --git a/regression/cbmc-java/pointer_check1/test.desc b/regression/cbmc-java/pointer_check1/test.desc new file mode 100644 index 00000000000..03121d320c6 --- /dev/null +++ b/regression/cbmc-java/pointer_check1/test.desc @@ -0,0 +1,8 @@ +CORE +pointer_check1.class +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-java/pointer_check2/pointer_check2.class b/regression/cbmc-java/pointer_check2/pointer_check2.class new file mode 100644 index 00000000000..1428f991767 Binary files /dev/null and b/regression/cbmc-java/pointer_check2/pointer_check2.class differ diff --git a/regression/cbmc-java/pointer_check2/pointer_check2.java b/regression/cbmc-java/pointer_check2/pointer_check2.java new file mode 100644 index 00000000000..029200bee54 --- /dev/null +++ b/regression/cbmc-java/pointer_check2/pointer_check2.java @@ -0,0 +1,24 @@ +import java.util.*; + +class pointer_check2 +{ + public static void main(String[] args) + { + String s = null; + Random rand = new Random(); + int day = rand.nextInt(7); + + if (day == 0) + { + s = "Monday"; + } + else + { + if (day == 1) + { + s = "Tuesday" ; + } + } + System.out.println(s.length()); + } +} diff --git a/regression/cbmc-java/pointer_check2/test.desc b/regression/cbmc-java/pointer_check2/test.desc new file mode 100644 index 00000000000..4dec5bca133 --- /dev/null +++ b/regression/cbmc-java/pointer_check2/test.desc @@ -0,0 +1,8 @@ +CORE +pointer_check2.class +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-java/static_method1/static_method1.class b/regression/cbmc-java/static_method1/static_method1.class new file mode 100644 index 00000000000..06626cd8c91 Binary files /dev/null and b/regression/cbmc-java/static_method1/static_method1.class differ diff --git a/regression/cbmc-java/static_method1/static_method1.java b/regression/cbmc-java/static_method1/static_method1.java new file mode 100644 index 00000000000..3da92fb1c50 --- /dev/null +++ b/regression/cbmc-java/static_method1/static_method1.java @@ -0,0 +1,12 @@ +public class static_method1 +{ + + static public void f(int a, int b) { + int c = b/(a+1); + } + + static public void g(int a, int b) { + int c = a/(b+1); + } + +} diff --git a/regression/cbmc-java/static_method1/test.desc b/regression/cbmc-java/static_method1/test.desc new file mode 100644 index 00000000000..c26f4061d02 --- /dev/null +++ b/regression/cbmc-java/static_method1/test.desc @@ -0,0 +1,8 @@ +CORE +static_method1.class +--function "static_method1.f" --div-by-zero-check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/Local_out_of_scope2/main.c b/regression/cbmc/Local_out_of_scope2/main.c new file mode 100644 index 00000000000..0794c634c53 --- /dev/null +++ b/regression/cbmc/Local_out_of_scope2/main.c @@ -0,0 +1,25 @@ +inline void foo(int x) +{ +} + +void bar() +{ + foo(0); +} + +void foobar() +{ + // different argument values must not cause an inconsistency in the + // equation system + foo(0); + bar(); + foo(1); +} + +int main() +{ + foobar(); + foobar(); + __CPROVER_assert(0, ""); + return 0; +} diff --git a/regression/cbmc/Local_out_of_scope2/test.desc b/regression/cbmc/Local_out_of_scope2/test.desc new file mode 100644 index 00000000000..6de79559914 --- /dev/null +++ b/regression/cbmc/Local_out_of_scope2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/run-datastax.sh b/regression/run-datastax.sh new file mode 100755 index 00000000000..793be5a9097 --- /dev/null +++ b/regression/run-datastax.sh @@ -0,0 +1,13 @@ +#!/bin/bash +test_cases=`find cbmc-java/datastax/ -name *.desc -exec dirname {} \;` +./test.pl -c $1 ${test_cases} + +count=0 +for test_case in ${test_cases}; do + out_file=`find ${test_case} -name '*.out'` + if grep -q "identifier.*not found" ${out_file}; then + echo ${out_file} + count=$((${count}+1)) + fi +done; +echo "Missing symbols: ${count}" diff --git a/regression/test.pl b/regression/test.pl index d8b669c9a91..44d7cf0fbfb 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -59,7 +59,7 @@ ($) sub test($$$$$) { my ($name, $test, $t_level, $cmd, $ign) = @_; - my ($level, $input, $options, @results) = load("$name/$test"); + my ($level, $input, $options, @results) = load("$test"); $options =~ s/$ign//g if(defined($ign)); my $output = $input; @@ -107,7 +107,7 @@ ($$$$$) my $r; $result =~ s/\\/\\\\/g; $result =~ s/([^\\])\$/$1\\r\\\\?\$/; - system("bash", "-c", "grep \$'$result' '$name/$output' >/dev/null"); + system("bash", "-c", "grep \$'$result' \"$name/$output\" >/dev/null"); $r = ($included ? $? != 0 : $? == 0); if($r) { print LOG "$result [FAILED]\n"; @@ -212,7 +212,11 @@ ($$$$) print "Loading\n"; my @tests = @ARGV != 0 ? @ARGV : dirs(); -my $count = @tests; +my $count = 0; +for (@tests){ + my @testfiles = glob "$_/*desc"; + $count += $#testfiles+1; +} print " $count " . (1==$count?"test":"tests") . " found\n\n"; use Cwd qw(getcwd); @@ -225,20 +229,22 @@ ($) { my ($test) = @_; my $failed_skipped = 0; - - defined($pool) or print " Running $test"; - $failed_skipped = test($test, "test.desc", $t_level, $opt_c, $opt_i); - - lock($skips); - defined($pool) and print " Running $test"; - if(2 == $failed_skipped) { - $skips++; - print " [SKIPPED]\n"; - } elsif(0 == $failed_skipped) { - print " [OK]\n"; - } else { - $failures++; - print " [FAILED]\n"; + my @files = glob "$test/*.desc"; + for (0..$#files){ + defined($pool) or print " Running $files[$_]"; + $failed_skipped = test($test, $files[$_], $t_level, $opt_c, $opt_i); + + lock($skips); + defined($pool) and print " Running $test $files[$_]"; + if(2 == $failed_skipped) { + $skips++; + print " [SKIPPED]\n"; + } elsif(0 == $failed_skipped) { + print " [OK]\n"; + } else { + $failures++; + print " [FAILED]\n"; + } } } diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 467ac8df0ef..8cd792f1fd0 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -944,23 +944,34 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(flags.is_unknown() || flags.is_dynamic_heap()) - add_guarded_claim( - not_exprt(deallocated(pointer, ns)), - "dereference failure: deallocated dynamic object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - if(flags.is_unknown() || flags.is_dynamic_local()) - add_guarded_claim( - not_exprt(dead_object(pointer, ns)), - "dereference failure: dead object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); + symbol_tablet symbol_table = ns.get_symbol_table(); + + symbol_tablet::symbolst::iterator s_it= + symbol_table.symbols.find(CPROVER_PREFIX "initialize"); + + // For Java don't check dereference of a deallocated or dead object + if (s_it==symbol_table.symbols.end() || (s_it->second).mode != ID_java) + { + + if(flags.is_unknown() || flags.is_dynamic_heap()) + add_guarded_claim( + not_exprt(deallocated(pointer, ns)), + "dereference failure: deallocated dynamic object", + "pointer dereference", + expr.find_source_location(), + expr, + guard); + + if(flags.is_unknown() || flags.is_dynamic_local()) + add_guarded_claim( + not_exprt(dead_object(pointer, ns)), + "dereference failure: dead object", + "pointer dereference", + expr.find_source_location(), + expr, + guard); + } if(enable_bounds_check) { diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 18de1c5fb8e..0764c137f49 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -1,6 +1,6 @@ SRC = c_typecast.cpp ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_parser.cpp \ expr2c.cpp ansi_c_language.cpp c_sizeof.cpp ansi_c_scope.cpp \ - c_types.cpp trans_unit.cpp ansi_c_typecheck.cpp \ + c_types.cpp ansi_c_typecheck.cpp \ c_preprocess.cpp c_storage_spec.cpp \ c_typecheck_base.cpp c_typecheck_initializer.cpp \ c_typecheck_typecast.cpp c_typecheck_code.cpp \ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 618568bd5da..e6e953ad3b5 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -229,6 +229,10 @@ void ansi_c_convert_typet::read_rec(const typet &type) } else if(type.id()==ID_noreturn) c_qualifiers.is_noreturn=true; + else if(type.id()==ID_constructor) + constructor=true; + else if(type.id()==ID_destructor) + destructor=true; else other.push_back(type); } @@ -274,6 +278,40 @@ void ansi_c_convert_typet::write(typet &type) } type.swap(other.front()); + + if(constructor || destructor) + { + if(constructor && destructor) + { + err_location(source_location); + str << "combining constructor and destructor not supported"; + error_msg(); + throw 0; + } + + typet *type_p=&type; + if(type.id()==ID_code) + type_p=&(to_code_type(type).return_type()); + + else if(type_p->id()!=ID_empty) + { + err_location(source_location); + str << "constructor and destructor required to be type void, " + << "found " << type_p->pretty(); + error_msg(); + throw 0; + } + + type_p->id(constructor ? ID_constructor : ID_destructor); + } + } + else if(constructor || destructor) + { + err_location(source_location); + str << "constructor and destructor required to be type void, " + << "found " << type.pretty(); + error_msg(); + throw 0; } else if(gcc_float128_cnt) { diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index eff7353dffd..a40d3f3549e 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -34,6 +34,7 @@ class ansi_c_convert_typet:public message_streamt bool packed, aligned; exprt vector_size, alignment, bv_width, fraction_width; exprt msc_based; // this is Visual Studio + bool constructor, destructor; // storage spec c_storage_spect c_storage_spec; @@ -67,7 +68,7 @@ class ansi_c_convert_typet:public message_streamt msc_based.make_nil(); gcc_attribute_mode.make_nil(); - packed=aligned=false; + packed=aligned=constructor=destructor=false; other.clear(); c_storage_spec.clear(); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 3a968fc8e2e..1fa90f9a102 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include +#include #include #include @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_typecheck.h" #include "ansi_c_parser.h" #include "expr2c.h" -#include "trans_unit.h" #include "c_preprocess.h" #include "ansi_c_internal_additions.h" #include "type2name.h" @@ -61,7 +60,7 @@ Function: ansi_c_languaget::modules_provided void ansi_c_languaget::modules_provided(std::set &modules) { - modules.insert(translation_unit(parse_path)); + modules.insert(get_base_name(parse_path, true)); } /*******************************************************************\ diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp index 2fa57e55c27..fd8dc27834e 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -24,7 +24,8 @@ Function: c_storage_spect::read void c_storage_spect::read(const typet &type) { - if(type.id()==ID_merged_type) + if(type.id()==ID_merged_type || + type.id()==ID_code) { forall_subtypes(it, type) read(*it); diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 175388b88dd..69938e4960b 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -711,13 +711,6 @@ void c_typecheck_baset::typecheck_declaration( { // get storage spec c_storage_spect c_storage_spec(declaration.type()); - - declaration.set_is_inline(c_storage_spec.is_inline); - declaration.set_is_static(c_storage_spec.is_static); - declaration.set_is_extern(c_storage_spec.is_extern); - declaration.set_is_thread_local(c_storage_spec.is_thread_local); - declaration.set_is_register(c_storage_spec.is_register); - declaration.set_is_typedef(c_storage_spec.is_typedef); // first typecheck the type of the declaration typecheck_type(declaration.type()); @@ -743,6 +736,17 @@ void c_typecheck_baset::typecheck_declaration( d_it!=declaration.declarators().end(); d_it++) { + c_storage_spect full_spec(declaration.full_type(*d_it)); + full_spec|=c_storage_spec; + + declaration.set_is_inline(full_spec.is_inline); + declaration.set_is_static(full_spec.is_static); + declaration.set_is_extern(full_spec.is_extern); + declaration.set_is_thread_local(full_spec.is_thread_local); + declaration.set_is_register(full_spec.is_register); + declaration.set_is_typedef(full_spec.is_typedef); + declaration.set_is_weak(full_spec.is_weak); + symbolt symbol; declaration.to_symbol(*d_it, symbol); irep_idt identifier=symbol.name; diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 3db1c632448..79c4a662c15 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "cprover_library.h" #include "ansi_c_language.h" diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c372206f597..c8797e8c726 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -694,6 +694,11 @@ std::string expr2ct::convert_rec( { return q+"__builtin_va_list"+d; } + else if(src.id()==ID_constructor || + src.id()==ID_destructor) + { + return q+"__attribute__(("+id2string(src.id())+")) void"+d; + } { lispexprt lisp; @@ -1260,10 +1265,7 @@ std::string expr2ct::convert_literal( const exprt &src, unsigned &precedence) { - if(src.operands().size()==1) - return "L("+src.get_string(ID_literal)+")"; - else - return convert_norep(src, precedence); + return "L("+src.get_string(ID_literal)+")"; } /*******************************************************************\ @@ -4501,8 +4503,6 @@ std::string expr2ct::convert( return convert_prob_coin(src, precedence=16); else if(statement=="prob_unif") return convert_prob_uniform(src, precedence=16); - else if(statement==ID_literal) - return convert_literal(src, precedence=16); else if(statement==ID_statement_expression) return convert_statement_expression(src, precedence=15); else if(statement==ID_gcc_builtin_va_arg_next) @@ -4511,6 +4511,9 @@ std::string expr2ct::convert( return convert_norep(src, precedence); } + else if(src.id()==ID_literal) + return convert_literal(src, precedence=16); + else if(src.id()==ID_not) return convert_unary(src, "!", precedence=15); diff --git a/src/ansi-c/library/locale.c b/src/ansi-c/library/locale.c index 8c030d81a44..61d5353457e 100644 --- a/src/ansi-c/library/locale.c +++ b/src/ansi-c/library/locale.c @@ -9,12 +9,16 @@ inline char *setlocale(int category, const char *locale) { __CPROVER_HIDE:; + (void)category; (void)*locale; #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_event("invalidate_pointer", "setlocale_result"); char *setlocale_result; __CPROVER_set_may(setlocale_result, "setlocale_result"); return setlocale_result; + #else + static char setlocale_result[1]; + return setlocale_result; #endif } @@ -33,5 +37,8 @@ inline struct lconv *localeconv(void) struct lconv *localeconv_result; __CPROVER_set_may(localeconv_result, "localeconv_result"); return localeconv_result; + #else + static struct lconv localeconv_result; + return &localeconv_result; #endif } diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 7fdd935a224..48bd24e8d53 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -617,8 +617,8 @@ float sqrtf(float f) if ( f < 0.0f ) return 0.0f/0.0f; // NaN else if (__CPROVER_isinff(f) || // +Inf only - f == 0.0f || // Includes -0 - __CPROVER_isnanf(f)) + f == 0.0f || // Includes -0 + __CPROVER_isnanf(f)) return f; else if (__CPROVER_isnormalf(f)) { @@ -702,8 +702,8 @@ double sqrt(double d) if ( d < 0.0 ) return 0.0/0.0; // NaN else if (__CPROVER_isinfd(d) || // +Inf only - d == 0.0 || // Includes -0 - __CPROVER_isnand(d)) + d == 0.0 || // Includes -0 + __CPROVER_isnand(d)) return d; else if (__CPROVER_isnormald(d)) { @@ -771,8 +771,8 @@ long double sqrtl(long double d) if(d < 0.0l) return 0.0l/0.0l; // NaN else if (__CPROVER_isinfld(d) || // +Inf only - d == 0.0l || // Includes -0 - __CPROVER_isnanld(d)) + d == 0.0l || // Includes -0 + __CPROVER_isnanld(d)) return d; else if (__CPROVER_isnormalld(d)) { diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 2793f9e8bdd..809a7e99a33 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -736,10 +736,14 @@ inline char *strrchr(const char *src, int c) char *strerror(int errnum) { __CPROVER_HIDE:; + (void)errnum; #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_event("invalidate_pointer", "strerror_result"); char *strerror_result; __CPROVER_set_must(strerror_result, "strerror_result"); return strerror_result; + #else + static char strerror_result[1]; + return strerror_result; #endif } diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c index 8bc1272e78d..fadc175cdb6 100644 --- a/src/ansi-c/library/time.c +++ b/src/ansi-c/library/time.c @@ -143,6 +143,9 @@ char *asctime(const struct tm *timeptr) char *asctime_result; __CPROVER_set_must(asctime_result, "asctime_result"); return asctime_result; + #else + static char asctime_result[1]; + return asctime_result; #endif } @@ -161,6 +164,9 @@ char *ctime(const time_t *clock) char *ctime_result; __CPROVER_set_must(ctime_result, "ctime_result"); return ctime_result; + #else + static char ctime_result[1]; + return ctime_result; #endif } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 4e404c94a3a..b827e91bc74 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -133,6 +133,8 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_GNU_INLINE "__gnu_inline__" %token TOK_GCC_ATTRIBUTE_WEAK "weak" %token TOK_GCC_ATTRIBUTE_NORETURN "noreturn" +%token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor" +%token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" %token TOK_GCC_ATTRIBUTE_END ")" %token TOK_GCC_LABEL "__label__" %token TOK_MSC_ASM "__asm" @@ -1566,6 +1568,10 @@ gcc_type_attribute: { $$=$1; set($$, ID_noreturn); } | TOK_GCC_ATTRIBUTE_NORETURN TOK_GCC_ATTRIBUTE_END { $$=$1; set($$, ID_noreturn); } + | TOK_GCC_ATTRIBUTE_CONSTRUCTOR TOK_GCC_ATTRIBUTE_END + { $$=$1; set($$, ID_constructor); } + | TOK_GCC_ATTRIBUTE_DESTRUCTOR TOK_GCC_ATTRIBUTE_END + { $$=$1; set($$, ID_destructor); } | gcc_attribute_specifier ; @@ -1983,7 +1989,7 @@ type_name: initializer_opt: /* nothing */ { - newstack($$); + init($$); stack($$).make_nil(); } | '=' initializer diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 118395385d3..281239a5dd8 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -44,7 +44,7 @@ int make_identifier() // this hashes the identifier irep_idt base_name=yytext; - + if(PARSER.cpp98) { stack(yyansi_clval).id(ID_symbol); @@ -139,43 +139,43 @@ delimiter [ \t\b\r] newline [\n\f\v]|"\\\n" whitespace {delimiter}+ ws {delimiter}* -ucletter [A-Z] -lcletter [a-z] -letter ({ucletter}|{lcletter}) -digit [0-9] -bindigit [01] -octdigit [0-7] -hexdigit [0-9a-fA-F] -identifier (({letter}|"_"|"$")({letter}|{digit}|"_"|"$")*) -integer {digit}+ -binary {bindigit}+ +ucletter [A-Z] +lcletter [a-z] +letter ({ucletter}|{lcletter}) +digit [0-9] +bindigit [01] +octdigit [0-7] +hexdigit [0-9a-fA-F] +identifier (({letter}|"_"|"$")({letter}|{digit}|"_"|"$")*) +integer {digit}+ +binary {bindigit}+ msiw_suffix ([iI]("8"|"16"|"32"|"64"|"128")) int_suffix [uUlLiIjJ]*|[uU]?{msiw_suffix} -bininteger "0"[bB]({bindigit}|"'")+{int_suffix} -decinteger [1-9]({digit}|"'")*{int_suffix} -octinteger "0"({octdigit}|"'")*{int_suffix} -hexinteger "0"[xX]{hexdigit}({hexdigit}|"'")*{int_suffix} +bininteger "0"[bB]({bindigit}|"'")+{int_suffix} +decinteger [1-9]({digit}|"'")*{int_suffix} +octinteger "0"({octdigit}|"'")*{int_suffix} +hexinteger "0"[xX]{hexdigit}({hexdigit}|"'")*{int_suffix} integer_s {decinteger}|{bininteger}|{octinteger}|{hexinteger} -octchar "\\"{octdigit}{1,3} -hexchar "\\x"{hexdigit}+ -exponent [eE][+-]?{integer} -fraction {integer} -float1 {integer}"."{fraction}?({exponent})? -float2 "."{fraction}({exponent})? -float3 {integer}{exponent} +octchar "\\"{octdigit}{1,3} +hexchar "\\x"{hexdigit}+ +exponent [eE][+-]?{integer} +fraction {integer} +float1 {integer}"."{fraction}?({exponent})? +float2 "."{fraction}({exponent})? +float3 {integer}{exponent} hexfloat1 "0"[xX]{hexdigit}+"."{hexdigit}+[pP][+-]?{integer} hexfloat2 "0"[xX]{hexdigit}+"."[pP][+-]?{integer} hexfloat3 "0"[xX]{hexdigit}+[pP][+-]?{integer} float_suffix [fFlLiIjJ]* gcc_ext_float_suffix [wWqQ]|[dD][fFdDlL]? -float {float1}|{float2}|{float3}|{hexfloat1}|{hexfloat2}|{hexfloat3} +float {float1}|{float2}|{float3}|{hexfloat1}|{hexfloat2}|{hexfloat3} float_s {float}{float_suffix}|{integer}[fF] -gcc_ext_float_s {float}{gcc_ext_float_suffix} -bitvector {binary}[bB] -bitvector_u {binary}([uU][bB]|[bB][uU]) -cppstart {ws}"#"{ws} -cpplineno {cppstart}"line"*{ws}{integer}{ws}.*{newline} -cppdirective {cppstart}.* +gcc_ext_float_s {float}{gcc_ext_float_suffix} +bitvector {binary}[bB] +bitvector_u {binary}([uU][bB]|[bB][uU]) +cppstart {ws}"#"{ws} +cpplineno {cppstart}"line"*{ws}{integer}{ws}.*{newline} +cppdirective {cppstart}.* escape_sequence [\\][^\n] c_char [^'\\\n]|{escape_sequence} @@ -195,6 +195,7 @@ string_lit ("L"|"u"|"U"|"u8")?["]{s_char}*["] %x MSC_PRAGMA %x MSC_ANNOTATION %x GCC_ATTRIBUTE1 +%x GCC_ATTRIBUTE1a %x GCC_ATTRIBUTE2 %x GCC_ATTRIBUTE3 %x GCC_ATTRIBUTE4 @@ -214,35 +215,35 @@ void ansi_c_scanner_init() %% .|\n { BEGIN(GRAMMAR); - yyless(0); /* start again with this character */ - } + yyless(0); /* start again with this character */ + } "/*" { BEGIN(COMMENT1); } /* begin C comment state */ { - "*/" { BEGIN(GRAMMAR); } /* end comment state, back to GRAMMAR */ - "/*" { yyansi_cerror("Probably nested comments"); } - <> { yyansi_cerror("Unterminated comment"); return TOK_SCANNER_ERROR; } - [^*/\n]* { /* ignore every char except '*' and NL (performance!) */ } - . { } /* all single characters within comments are ignored */ - \n { } - } + "*/" { BEGIN(GRAMMAR); } /* end comment state, back to GRAMMAR */ + "/*" { yyansi_cerror("Probably nested comments"); } + <> { yyansi_cerror("Unterminated comment"); return TOK_SCANNER_ERROR; } + [^*/\n]* { /* ignore every char except '*' and NL (performance!) */ } + . { } /* all single characters within comments are ignored */ + \n { } +} { - "*/" { BEGIN(STRING_LITERAL); } /* end comment state, back to STRING_LITERAL */ - "/*" { yyansi_cerror("Probably nested comments"); } - <> { yyansi_cerror("Unterminated comment"); return TOK_SCANNER_ERROR; } - [^*/\n]* { /* ignore every char except '*' and NL (performance!) */ } - . { } /* all single characters within comments are ignored */ - \n { } - } + "*/" { BEGIN(STRING_LITERAL); } /* end comment state, back to STRING_LITERAL */ + "/*" { yyansi_cerror("Probably nested comments"); } + <> { yyansi_cerror("Unterminated comment"); return TOK_SCANNER_ERROR; } + [^*/\n]* { /* ignore every char except '*' and NL (performance!) */ } + . { } /* all single characters within comments are ignored */ + \n { } +} -"//" { BEGIN(COMMENT2); } /* begin C++ comment state */ +"//" { BEGIN(COMMENT2); } /* begin C++ comment state */ { - \n { BEGIN(GRAMMAR); } /* end comment state, back GRAMMAR */ - .* { } /* all characters within comments are ignored */ - } + \n { BEGIN(GRAMMAR); } /* end comment state, back GRAMMAR */ + .* { } /* all characters within comments are ignored */ +} {char_lit} { newstack(yyansi_clval); @@ -267,10 +268,10 @@ void ansi_c_scanner_init() {cpplineno} { preprocessor_line(yytext, PARSER); PARSER.set_line_no(PARSER.get_line_no()-1); - } + } {cppdirective} { /* ignore */ } "/*" { BEGIN(STRING_LITERAL_COMMENT); /* C comment, ignore */ } -"//".*\n { /* C++ comment, ignore */ } +"//".*\n { /* C++ comment, ignore */ } . { // anything else: back to normal source_locationt l=stack(yyansi_clval).source_location(); stack(yyansi_clval)=convert_string_literal(PARSER.string_literal); @@ -280,140 +281,140 @@ void ansi_c_scanner_init() return TOK_STRING; } -{newline} { } /* skipped */ -{whitespace} { } /* skipped */ +{newline} { } /* skipped */ +{whitespace} { } /* skipped */ -{cpplineno} { +{cpplineno} { preprocessor_line(yytext, PARSER); PARSER.set_line_no(PARSER.get_line_no()-1); - } + } {cppstart}"pragma"{ws}"pack"{ws}"("{ws}"push"{ws}")"{ws}{newline} { - // Done by Visual Studio and gcc - // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx - // push, pop could also use identifiers - if(PARSER.pragma_pack.empty()) - PARSER.pragma_pack.push_back(convert_integer_literal("0")); - else - PARSER.pragma_pack.push_back(PARSER.pragma_pack.back()); - } + // Done by Visual Studio and gcc + // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx + // push, pop could also use identifiers + if(PARSER.pragma_pack.empty()) + PARSER.pragma_pack.push_back(convert_integer_literal("0")); + else + PARSER.pragma_pack.push_back(PARSER.pragma_pack.back()); + } {cppstart}"pragma"{ws}"pack"{ws}"("{ws}"push"{ws}","{ws}{integer_s}{ws}")"{ws}{newline} { - // Done by Visual Studio and gcc - // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx - // push, pop could also use identifiers - std::string tmp(yytext); - std::string::size_type p=tmp.find(',')+1; - while(tmp[p]==' ' || tmp[p]=='\t') ++p; - std::string value=std::string(tmp, p, tmp.find_last_not_of(") \t\n\r")+1-p); - exprt n=convert_integer_literal(value); - PARSER.pragma_pack.push_back(n); - } + // Done by Visual Studio and gcc + // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx + // push, pop could also use identifiers + std::string tmp(yytext); + std::string::size_type p=tmp.find(',')+1; + while(tmp[p]==' ' || tmp[p]=='\t') ++p; + std::string value=std::string(tmp, p, tmp.find_last_not_of(") \t\n\r")+1-p); + exprt n=convert_integer_literal(value); + PARSER.pragma_pack.push_back(n); + } {cppstart}"pragma"{ws}"pack"{ws}"("{ws}{integer_s}{ws}")"{ws}{newline} { - // Done by Visual Studio and gcc - // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx - std::string tmp(yytext); - std::string::size_type p=tmp.find('(')+1; - while(tmp[p]==' ' || tmp[p]=='\t') ++p; - std::string value=std::string(tmp, p, tmp.find_last_not_of(") \t\n\r")+1-p); - exprt n=convert_integer_literal(value); - PARSER.pragma_pack.push_back(n); - } + // Done by Visual Studio and gcc + // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx + std::string tmp(yytext); + std::string::size_type p=tmp.find('(')+1; + while(tmp[p]==' ' || tmp[p]=='\t') ++p; + std::string value=std::string(tmp, p, tmp.find_last_not_of(") \t\n\r")+1-p); + exprt n=convert_integer_literal(value); + PARSER.pragma_pack.push_back(n); + } {cppstart}"pragma"{ws}"pack"{ws}"("{ws}"pop"{ws}")"{ws}{newline} { - // Done by Visual Studio and gcc - // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx - // push, pop could also use identifiers - if(!PARSER.pragma_pack.empty()) PARSER.pragma_pack.pop_back(); - } + // Done by Visual Studio and gcc + // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx + // push, pop could also use identifiers + if(!PARSER.pragma_pack.empty()) PARSER.pragma_pack.pop_back(); + } {cppstart}"pragma"{ws}"pack"{ws}"("{ws}")"{ws}{newline} { - // Done by Visual Studio and gcc - // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx - // should be equivalent to pop-all - PARSER.pragma_pack.clear(); - } + // Done by Visual Studio and gcc + // http://msdn.microsoft.com/en-us/library/2e70t5y1%28v=vs.80%29.aspx + // should be equivalent to pop-all + PARSER.pragma_pack.clear(); + } {cppstart}"pragma"{ws}.* { - // silently ignore other pragmas - } + // silently ignore other pragmas + } {cppstart}"ident"{ws}.* { /* ignore */ } {cppstart}"define"{ws}.* { /* ignore */ } {cppstart}"undef"{ws}.* { /* ignore */ } -{cppdirective} { - yyansi_cerror("Preprocessor directive found"); - return TOK_SCANNER_ERROR; - } +{cppdirective} { + yyansi_cerror("Preprocessor directive found"); + return TOK_SCANNER_ERROR; + } %{ /*** keywords ***/ %} { -"auto" { loc(); return TOK_AUTO; } -"_Bool" { if(PARSER.cpp98) +"auto" { loc(); return TOK_AUTO; } +"_Bool" { if(PARSER.cpp98) return make_identifier(); else { loc(); return TOK_BOOL; } } -"break" { loc(); return TOK_BREAK; } -"case" { loc(); return TOK_CASE; } -"char" { loc(); return TOK_CHAR; } -"_Complex" { loc(); return TOK_COMPLEX; } -"const" { loc(); return TOK_CONST; } -"continue" { loc(); return TOK_CONTINUE; } -"default" { loc(); return TOK_DEFAULT; } -"do" { loc(); return TOK_DO; } -"double" { loc(); return TOK_DOUBLE; } -"else" { loc(); return TOK_ELSE; } -"enum" { loc(); PARSER.tag_following=true; return TOK_ENUM; } -"extern" { loc(); return TOK_EXTERN; } -"float" { loc(); return TOK_FLOAT; } -"for" { loc(); return TOK_FOR; } -"goto" { loc(); return TOK_GOTO; } -"if" { loc(); return TOK_IF; } -"inline" { loc(); return TOK_INLINE; } -"int" { loc(); return TOK_INT; } -"long" { loc(); return TOK_LONG; } -"register" { loc(); return TOK_REGISTER; } +"break" { loc(); return TOK_BREAK; } +"case" { loc(); return TOK_CASE; } +"char" { loc(); return TOK_CHAR; } +"_Complex" { loc(); return TOK_COMPLEX; } +"const" { loc(); return TOK_CONST; } +"continue" { loc(); return TOK_CONTINUE; } +"default" { loc(); return TOK_DEFAULT; } +"do" { loc(); return TOK_DO; } +"double" { loc(); return TOK_DOUBLE; } +"else" { loc(); return TOK_ELSE; } +"enum" { loc(); PARSER.tag_following=true; return TOK_ENUM; } +"extern" { loc(); return TOK_EXTERN; } +"float" { loc(); return TOK_FLOAT; } +"for" { loc(); return TOK_FOR; } +"goto" { loc(); return TOK_GOTO; } +"if" { loc(); return TOK_IF; } +"inline" { loc(); return TOK_INLINE; } +"int" { loc(); return TOK_INT; } +"long" { loc(); return TOK_LONG; } +"register" { loc(); return TOK_REGISTER; } "restrict" { loc(); return TOK_RESTRICT; } -"return" { loc(); return TOK_RETURN; } -"short" { loc(); return TOK_SHORT; } -"signed" { loc(); return TOK_SIGNED; } -"sizeof" { loc(); return TOK_SIZEOF; } -"static" { loc(); return TOK_STATIC; } -"struct" { loc(); PARSER.tag_following=true; return TOK_STRUCT; } -"switch" { loc(); return TOK_SWITCH; } -"typedef" { loc(); return TOK_TYPEDEF; } -"union" { loc(); PARSER.tag_following=true; return TOK_UNION; } -"unsigned" { loc(); return TOK_UNSIGNED; } -"void" { loc(); return TOK_VOID; } -"volatile" { loc(); return TOK_VOLATILE; } -"while" { loc(); return TOK_WHILE; } +"return" { loc(); return TOK_RETURN; } +"short" { loc(); return TOK_SHORT; } +"signed" { loc(); return TOK_SIGNED; } +"sizeof" { loc(); return TOK_SIZEOF; } +"static" { loc(); return TOK_STATIC; } +"struct" { loc(); PARSER.tag_following=true; return TOK_STRUCT; } +"switch" { loc(); return TOK_SWITCH; } +"typedef" { loc(); return TOK_TYPEDEF; } +"union" { loc(); PARSER.tag_following=true; return TOK_UNION; } +"unsigned" { loc(); return TOK_UNSIGNED; } +"void" { loc(); return TOK_VOID; } +"volatile" { loc(); return TOK_VOLATILE; } +"while" { loc(); return TOK_WHILE; } "__auto_type" { if(PARSER.mode==ansi_c_parsert::GCC && !PARSER.cpp98) - { loc(); return TOK_GCC_AUTO_TYPE; } + { loc(); return TOK_GCC_AUTO_TYPE; } else return make_identifier(); } -"__float80" { if(PARSER.mode==ansi_c_parsert::GCC) - { loc(); return TOK_GCC_FLOAT80; } +"__float80" { if(PARSER.mode==ansi_c_parsert::GCC) + { loc(); return TOK_GCC_FLOAT80; } else return make_identifier(); } -"__float128" { if(PARSER.mode==ansi_c_parsert::GCC) - { loc(); return TOK_GCC_FLOAT128; } +"__float128" { if(PARSER.mode==ansi_c_parsert::GCC) + { loc(); return TOK_GCC_FLOAT128; } else return make_identifier(); } -"__int128" { if(PARSER.mode==ansi_c_parsert::GCC) - { loc(); return TOK_GCC_INT128; } +"__int128" { if(PARSER.mode==ansi_c_parsert::GCC) + { loc(); return TOK_GCC_INT128; } else return make_identifier(); } @@ -467,7 +468,7 @@ void ansi_c_scanner_init() } "__real__" | -"__real" { if(PARSER.mode==ansi_c_parsert::GCC || +"__real" { if(PARSER.mode==ansi_c_parsert::GCC || PARSER.mode==ansi_c_parsert::ARM) { loc(); return TOK_REAL; } else @@ -475,7 +476,7 @@ void ansi_c_scanner_init() } "__imag__" | -"__imag" { if(PARSER.mode==ansi_c_parsert::GCC || +"__imag" { if(PARSER.mode==ansi_c_parsert::GCC || PARSER.mode==ansi_c_parsert::ARM) { loc(); return TOK_IMAG; } else @@ -608,11 +609,11 @@ void ansi_c_scanner_init() return make_identifier(); } -"__wchar_t" { if(PARSER.mode==ansi_c_parsert::MSC) - { loc(); return TOK_WCHAR_T; } +"__wchar_t" { if(PARSER.mode==ansi_c_parsert::MSC) + { loc(); return TOK_WCHAR_T; } else return make_identifier(); - } + } %{ /* C++ Keywords and Operators */ @@ -658,7 +659,7 @@ typeid { return cpp98_keyword(TOK_TYPEID); } typename { return cpp98_keyword(TOK_TYPENAME); } using { return cpp98_keyword(TOK_USING); } virtual { return cpp98_keyword(TOK_VIRTUAL); } -wchar_t { // CodeWarrior doesn't have wchar_t built in, +wchar_t { // CodeWarrior doesn't have wchar_t built in, // and MSC has a command-line option to turn it off if(PARSER.mode==ansi_c_parsert::CW) return make_identifier(); @@ -737,14 +738,14 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) "["{ws}"emitidl" | "["{ws}"module" | "["{ws}"export" { if(PARSER.mode==ansi_c_parsert::MSC) - BEGIN(MSC_ANNOTATION); + BEGIN(MSC_ANNOTATION); else - { - yyless(1); // puts all but [ back into stream - loc(); - PARSER.tag_following=false; - return yytext[0]; // returns the [ - } + { + yyless(1); // puts all but [ back into stream + loc(); + PARSER.tag_following=false; + return yytext[0]; // returns the [ + } } "__char16_t" { if(PARSER.mode==ansi_c_parsert::GCC) @@ -1013,8 +1014,8 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) return make_identifier(); } -"__inline" { loc(); return TOK_INLINE; } -"__inline__" { loc(); return TOK_INLINE; } +"__inline" { loc(); return TOK_INLINE; } +"__inline__" { loc(); return TOK_INLINE; } "__label__" { if(PARSER.mode==ansi_c_parsert::GCC || PARSER.mode==ansi_c_parsert::ARM) @@ -1144,10 +1145,10 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) /* This is a C11 keyword. It can be used as a type qualifier and as a type specifier, which introduces ambiguity into the grammar. We thus have two different tokens. - + 6.7.2.4 - 4: If the _Atomic keyword is immediately followed by a left parenthesis, it is interpreted as a type specifier (with a type name), - not as a type qualifier. + not as a type qualifier. */ "_Atomic"{ws}"(" { // put back all but _Atomic @@ -1224,29 +1225,29 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) /* operators following */ { -"->" { loc(); return TOK_ARROW; } -"++" { loc(); return TOK_INCR; } -"--" { loc(); return TOK_DECR; } -"<<" { loc(); return TOK_SHIFTLEFT; } -">>" { loc(); return TOK_SHIFTRIGHT; } -"<=" { loc(); return TOK_LE; } -">=" { loc(); return TOK_GE; } -"==" { loc(); return TOK_EQ; } -"!=" { loc(); return TOK_NE; } -"&&" { loc(); return TOK_ANDAND; } -"||" { loc(); return TOK_OROR; } -"..." { loc(); return TOK_ELLIPSIS; } - -"*=" { loc(); return TOK_MULTASSIGN; } -"/=" { loc(); return TOK_DIVASSIGN; } -"%=" { loc(); return TOK_MODASSIGN; } -"+=" { loc(); return TOK_PLUSASSIGN; } -"-=" { loc(); return TOK_MINUSASSIGN; } -"<<=" { loc(); return TOK_SHLASSIGN; } -">>=" { loc(); return TOK_SHRASSIGN; } -"&=" { loc(); return TOK_ANDASSIGN; } -"^=" { loc(); return TOK_XORASSIGN; } -"|=" { loc(); return TOK_ORASSIGN; } +"->" { loc(); return TOK_ARROW; } +"++" { loc(); return TOK_INCR; } +"--" { loc(); return TOK_DECR; } +"<<" { loc(); return TOK_SHIFTLEFT; } +">>" { loc(); return TOK_SHIFTRIGHT; } +"<=" { loc(); return TOK_LE; } +">=" { loc(); return TOK_GE; } +"==" { loc(); return TOK_EQ; } +"!=" { loc(); return TOK_NE; } +"&&" { loc(); return TOK_ANDAND; } +"||" { loc(); return TOK_OROR; } +"..." { loc(); return TOK_ELLIPSIS; } + +"*=" { loc(); return TOK_MULTASSIGN; } +"/=" { loc(); return TOK_DIVASSIGN; } +"%=" { loc(); return TOK_MODASSIGN; } +"+=" { loc(); return TOK_PLUSASSIGN; } +"-=" { loc(); return TOK_MINUSASSIGN; } +"<<=" { loc(); return TOK_SHLASSIGN; } +">>=" { loc(); return TOK_SHRASSIGN; } +"&=" { loc(); return TOK_ANDASSIGN; } +"^=" { loc(); return TOK_XORASSIGN; } +"|=" { loc(); return TOK_ORASSIGN; } /* digraphs */ "<:" { loc(); return '['; } @@ -1257,7 +1258,7 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) { -{identifier} { return make_identifier(); } +{identifier} { return make_identifier(); } {integer_s} { newstack(yyansi_clval); stack(yyansi_clval)=convert_integer_literal(yytext); @@ -1265,24 +1266,24 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) return TOK_INTEGER; } -{gcc_ext_float_s} { if(PARSER.mode!=ansi_c_parsert::GCC) +{gcc_ext_float_s} { if(PARSER.mode!=ansi_c_parsert::GCC) { - yyansi_cerror("Preprocessor directive found"); - return TOK_SCANNER_ERROR; + yyansi_cerror("Preprocessor directive found"); + return TOK_SCANNER_ERROR; } - newstack(yyansi_clval); - stack(yyansi_clval)=convert_float_literal(yytext); - PARSER.set_source_location(stack(yyansi_clval)); - return TOK_FLOATING; - } + newstack(yyansi_clval); + stack(yyansi_clval)=convert_float_literal(yytext); + PARSER.set_source_location(stack(yyansi_clval)); + return TOK_FLOATING; + } -{float_s} { newstack(yyansi_clval); +{float_s} { newstack(yyansi_clval); stack(yyansi_clval)=convert_float_literal(yytext); PARSER.set_source_location(stack(yyansi_clval)); - return TOK_FLOATING; - } + return TOK_FLOATING; + } -"{" { +"{" { PARSER.tag_following=false; if(PARSER.asm_block_following) { BEGIN(ASM_BLOCK); } loc(); @@ -1296,7 +1297,7 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) } /* This catches all one-character operators */ -. { loc(); PARSER.tag_following=false; return yytext[0]; } +. { loc(); PARSER.tag_following=false; return yytext[0]; } } "]" { BEGIN(GRAMMAR); } @@ -1346,8 +1347,22 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) } { -"("{ws}"(" | -"("{newline}"(" { BEGIN(GCC_ATTRIBUTE2); PARSER.parenthesis_counter=0; } +{cpplineno} { + preprocessor_line(yytext, PARSER); + PARSER.set_line_no(PARSER.get_line_no()-1); + } +{ws} { /* ignore */ } +{newline} { /* ignore */ } +"(" { BEGIN(GCC_ATTRIBUTE1a); } +. { BEGIN(GRAMMAR); loc(); return yytext[0]; } +} + +{ +{cpplineno} { + preprocessor_line(yytext, PARSER); + PARSER.set_line_no(PARSER.get_line_no()-1); + } +"(" { BEGIN(GCC_ATTRIBUTE2); PARSER.parenthesis_counter=0; } {ws} { /* ignore */ } {newline} { /* ignore */ } . { BEGIN(GRAMMAR); loc(); return yytext[0]; } @@ -1378,6 +1393,12 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) "noreturn" | "__noreturn__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_NORETURN; } +"constructor" | +"__constructor__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_CONSTRUCTOR; } + +"destructor" | +"__destructor__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_DESTRUCTOR; } + {ws} { /* ignore */ } {newline} { /* ignore */ } {identifier} { BEGIN(GCC_ATTRIBUTE4); } @@ -1386,6 +1407,10 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) } { // an attribute we do process +{cpplineno} { + preprocessor_line(yytext, PARSER); + PARSER.set_line_no(PARSER.get_line_no()-1); + } "(" { PARSER.parenthesis_counter++; loc(); return '('; } ")" { if(PARSER.parenthesis_counter==0) { @@ -1419,7 +1444,7 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) } {ws} { /* ignore */ } {newline} { /* ignore */ } -{identifier} { return make_identifier(); } +{identifier} { return make_identifier(); } . { loc(); return yytext[0]; } } @@ -1436,13 +1461,17 @@ __decltype { if(PARSER.cpp98 && PARSER.mode==ansi_c_parsert::GCC) } { // end bit: the closing parenthesis +{cpplineno} { + preprocessor_line(yytext, PARSER); + PARSER.set_line_no(PARSER.get_line_no()-1); + } ")" { BEGIN(GRAMMAR); } {ws} { /* Throw away */ } {newline} { /* Throw away */ } . { BEGIN(GRAMMAR); loc(); return yytext[0]; } } -<> { yyterminate(); /* done! */ } +<> { yyterminate(); /* done! */ } %% diff --git a/src/ansi-c/trans_unit.cpp b/src/ansi-c/trans_unit.cpp deleted file mode 100644 index b57fbeed216..00000000000 --- a/src/ansi-c/trans_unit.cpp +++ /dev/null @@ -1,41 +0,0 @@ -/*******************************************************************\ - -Module: Translation Unit - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "trans_unit.h" - -/*******************************************************************\ - -Function: translation_unit - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -std::string translation_unit(const std::string &path) -{ - // convert path into a suggestion for a translation unit name - - std::string unit=path; - - std::string::size_type pos; - - pos=unit.find_last_of("/\\"); - if(pos!=std::string::npos) - unit=std::string(unit, pos+1); - - pos=unit.find_last_of('.'); - if(pos!=std::string::npos) - unit=std::string(unit, 0, pos); - - return unit; -} - diff --git a/src/ansi-c/trans_unit.h b/src/ansi-c/trans_unit.h deleted file mode 100644 index ba1665d948c..00000000000 --- a/src/ansi-c/trans_unit.h +++ /dev/null @@ -1,11 +0,0 @@ -/*******************************************************************\ - -Module: Translation Unit - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include - -std::string translation_unit(const std::string &path); diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 77533b7b7a4..af24fd311ef 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -187,10 +187,10 @@ static std::string type2name( { const array_typet &t=to_array_type(type); mp_integer size; - if(to_integer(t.size(), size)) - result+="ARR?"; - else if(t.size().id()==ID_symbol) + if(t.size().id()==ID_symbol) result+="ARR"+t.size().get_string(ID_identifier); + else if(to_integer(t.size(), size)) + result+="ARR?"; else result+="ARR"+integer2string(size); } diff --git a/src/assembler/scanner.l b/src/assembler/scanner.l index 55a10ad142c..1ae46542e02 100644 --- a/src/assembler/scanner.l +++ b/src/assembler/scanner.l @@ -23,23 +23,23 @@ newline [\n\f\v]|"\\\n" whitespace {delimiter}+ ws {delimiter}* ws_or_newline ({delimiter}|{newline})* -ucletter [A-Z] -lcletter [a-z] -letter ({ucletter}|{lcletter}) -digit [0-9] -bindigit [01] -octdigit [0-7] -hexdigit [0-9a-fA-F] -identifier (({letter}|"_"|"$"|".")({letter}|{digit}|"_"|"$"|".")*) -integer {digit}+ -binary {bindigit}+ -bininteger "0"[bB]{bindigit}+{int_suffix} -decinteger [1-9]{digit}*{int_suffix} -octinteger "0"{octdigit}*{int_suffix} -hexinteger "0"[xX]{hexdigit}+{int_suffix} +ucletter [A-Z] +lcletter [a-z] +letter ({ucletter}|{lcletter}) +digit [0-9] +bindigit [01] +octdigit [0-7] +hexdigit [0-9a-fA-F] +identifier (({letter}|"_"|"$"|".")({letter}|{digit}|"_"|"$"|".")*) +integer {digit}+ +binary {bindigit}+ +bininteger "0"[bB]{bindigit}+{int_suffix} +decinteger [1-9]{digit}*{int_suffix} +octinteger "0"{octdigit}*{int_suffix} +hexinteger "0"[xX]{hexdigit}+{int_suffix} integer_s {decinteger}|{bininteger}|{octinteger}|{hexinteger} -octchar "\\"{octdigit}{1,3} -hexchar "\\x"{hexdigit}+ +octchar "\\"{octdigit}{1,3} +hexchar "\\x"{hexdigit}+ escape_sequence [\\][^\n] c_char [^'\\\n]|{escape_sequence} @@ -62,46 +62,44 @@ void assemlber_scanner_init() %% .|\n { BEGIN(GRAMMAR); - yyless(0); /* start again with this character */ - } + yyless(0); /* start again with this character */ + } -"#" { PARSER.new_instruction(); BEGIN(LINE_COMMENT); } /* begin comment state */ +"#" { PARSER.new_instruction(); BEGIN(LINE_COMMENT); } /* begin comment state */ { - \n { BEGIN(GRAMMAR); } /* end comment state, back GRAMMAR */ - .* { } /* all characters within comments are ignored */ - } + \n { BEGIN(GRAMMAR); } /* end comment state, back GRAMMAR */ + .* { } /* all characters within comments are ignored */ +} -{newline} { PARSER.new_instruction(); } -";" { PARSER.new_instruction(); } -{whitespace} { } /* skipped */ +{newline} { PARSER.new_instruction(); } +";" { PARSER.new_instruction(); } +{whitespace} { } /* skipped */ -%{ -/*** keywords ***/ -%} + /*** keywords ***/ { -".data" { } +".data" { } } -%{ -/*** rest ***/ -%} + /*** rest ***/ { -{ws} { /* ignore */ } -{identifier} { irept identifier(ID_symbol); - identifier.set(ID_identifier, yytext); - PARSER.add_token(identifier); } +{ws} { /* ignore */ } +{identifier} { irept identifier(ID_symbol); + identifier.set(ID_identifier, yytext); + PARSER.add_token(identifier); + } ">>" { PARSER.add_token(irept(ID_shr)); } "<<" { PARSER.add_token(irept(ID_shl)); } . { std::string s; s+=yytext[0]; - PARSER.add_token(irept(s)); } + PARSER.add_token(irept(s)); + } } -<> { yyterminate(); /* done! */ } +<> { yyterminate(); /* done! */ } %% diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 85a37e87d69..c5fc0469ff1 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -69,12 +69,9 @@ class bmc_covert: void output(std::ostream &out) { - for(block_mapt::const_iterator - b_it=block_map.begin(); - b_it!=block_map.end(); - b_it++) - out << b_it->first->source_location - << " -> " << b_it->second + for(const auto &b_it : block_map) + out << b_it.first->source_location + << " -> " << b_it.second << '\n'; } }; @@ -136,23 +133,16 @@ class bmc_covert: { std::vector tmp; - for(instancest::const_iterator - it=instances.begin(); - it!=instances.end(); - it++) - tmp.push_back(literal_exprt(it->condition)); + for(const auto &it : instances) + tmp.push_back(literal_exprt(it.condition)); - return conjunction(tmp); + return disjunction(tmp); } }; - inline irep_idt id( - goto_programt::const_targett loc, - const std::string suffix="") + inline irep_idt id(goto_programt::const_targett loc) { - return id2string(loc->function)+ - "#"+i2string(loc->location_number)+ - suffix; + return loc->source_location.get_property_id(); } typedef std::map goal_mapt; @@ -180,29 +170,23 @@ Function: bmc_covert::goal_covered void bmc_covert::goal_covered(const cover_goalst::goalt &) { - for(goal_mapt::iterator - g_it=goal_map.begin(); - g_it!=goal_map.end(); - g_it++) + for(auto &g_it : goal_map) { - goalt &g=g_it->second; + goalt &g=g_it.second; // covered already? if(g.satisfied) continue; // check whether satisfied - for(goalt::instancest::const_iterator - c_it=g.instances.begin(); - c_it!=g.instances.end(); - c_it++) + for(const auto &c_it : g.instances) { - literalt cond=c_it->condition; + literalt cond=c_it.condition; if(solver.l_get(cond).is_true()) { status() << "Covered " << g.description << messaget::eom; g.satisfied=true; - symex_target_equationt::SSA_stepst::iterator next=c_it->step; + symex_target_equationt::SSA_stepst::iterator next=c_it.step; next++; // include the instruction itself build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace); break; @@ -261,20 +245,6 @@ bool bmc_covert::operator()() // stop the time absolute_timet sat_start=current_time(); - // we don't want the assertions to become constraints - for(symex_target_equationt::SSA_stepst::iterator - it=bmc.equation.SSA_steps.begin(); - it!=bmc.equation.SSA_steps.end(); - it++) - if(it->type==goto_trace_stept::ASSERT) - it->type=goto_trace_stept::LOCATION; - - bmc.do_conversion(); - - //bmc.equation.output(std::cout); - - std::map location_map; - // Collect _all_ goals in `goal_map'. // This maps property IDs to 'goalt' forall_goto_functions(f_it, goto_functions) @@ -290,40 +260,43 @@ bool bmc_covert::operator()() i_it->source_location); } } - - // collects assumptions - and_exprt::operandst assumptions; + for(auto & it : bmc.equation.SSA_steps) + it.cond_literal=literalt(0, 0); + + // Do conversion to next solver layer + + bmc.do_conversion(); + + //bmc.equation.output(std::cout); + // get the conditions for these goals from formula // collect all 'instances' of the goals - for(symex_target_equationt::SSA_stepst::iterator - it=bmc.equation.SSA_steps.begin(); + for(auto it = bmc.equation.SSA_steps.begin(); it!=bmc.equation.SSA_steps.end(); it++) { - if(it->is_assume()) - assumptions.push_back(literal_exprt(it->cond_literal)); - - if(it->source.pc->is_assert()) + if(it->is_assert()) { - and_exprt c_expr(conjunction(assumptions), literal_exprt(it->guard_literal)); - literalt c=solver.convert(c_expr); - goal_map[id(it->source.pc)].add_instance(it, c); + assert(it->source.pc->is_assert()); + exprt c= + conjunction({ + literal_exprt(it->guard_literal), + literal_exprt(!it->cond_literal) }); + literalt l_c=solver.convert(c); + goal_map[id(it->source.pc)].add_instance(it, l_c); } } - status() << "Aiming to cover " << goal_map.size() << " goals" << eom; + status() << "Aiming to cover " << goal_map.size() << " goal(s)" << eom; cover_goalst cover_goals(solver); cover_goals.register_observer(*this); - for(goal_mapt::const_iterator - it=goal_map.begin(); - it!=goal_map.end(); - it++) + for(const auto &it : goal_map) { - literalt l=solver.convert(it->second.as_expr()); + literalt l=solver.convert(it.second.as_expr()); cover_goals.add(l); } @@ -350,19 +323,16 @@ bool bmc_covert::operator()() unsigned goals_covered=0; - for(goal_mapt::const_iterator - it=goal_map.begin(); - it!=goal_map.end(); - it++) + for(const auto & it : goal_map) { - const goalt &goal=it->second; + const goalt &goal=it.second; if(goal.satisfied) goals_covered++; if(bmc.ui==ui_message_handlert::XML_UI) { xmlt xml_result("result"); - xml_result.set_attribute("goal", id2string(it->first)); + xml_result.set_attribute("goal", id2string(it.first)); xml_result.set_attribute("description", goal.description); xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED"); @@ -376,8 +346,13 @@ bool bmc_covert::operator()() } else { - status() << "[" << it->first << "]"; + status() << "[" << it.first << "]"; + + if(goal.source_location.is_not_nil()) + status() << ' ' << goal.source_location; + if(!goal.description.empty()) status() << ' ' << goal.description; + status() << ": " << (goal.satisfied?"SATISFIED":"FAILED") << eom; } @@ -387,9 +362,12 @@ bool bmc_covert::operator()() status() << "** " << goals_covered << " of " << goal_map.size() << " covered (" + << std::fixed << std::setw(1) << std::setprecision(1) + << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size()) + << "%), using " << cover_goals.iterations() << " iteration" << (cover_goals.iterations()==1?"":"s") - << ")" << eom; + << eom; return false; } diff --git a/src/cbmc/cbmc.plist b/src/cbmc/cbmc.plist deleted file mode 100644 index c0663f45de5..00000000000 --- a/src/cbmc/cbmc.plist +++ /dev/null @@ -1,18 +0,0 @@ - - - - - - BundleHasStrictIdentifier - - BundleIsRelocatable - - BundleIsVersionChecked - - BundleOverwriteAction - upgrade - RootRelativeBundlePath - usr/bin/cbmc - - - diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b996f09d54c..bdec0116408 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -937,10 +937,12 @@ bool cbmc_parse_optionst::process_goto_program( c=coverage_criteriont::CONDITION; else if(criterion=="mcdc") c=coverage_criteriont::MCDC; + else if(criterion=="cover") + c=coverage_criteriont::COVER; else { error() << "unknown coverage criterion" << eom; - return false; + return true; } status() << "Instrumenting coverge goals" << eom; diff --git a/src/cbmc/dist-macos b/src/cbmc/dist-macos index 7d324cbacc5..bbf54cc8c20 100755 --- a/src/cbmc/dist-macos +++ b/src/cbmc/dist-macos @@ -17,35 +17,38 @@ echo $VERSION_FILE mkdir /tmp/cbmc-dist mkdir /tmp/cbmc-dist/package-root mkdir /tmp/cbmc-dist/package-root/usr -mkdir /tmp/cbmc-dist/package-root/usr/bin +mkdir /tmp/cbmc-dist/package-root/usr/local +mkdir /tmp/cbmc-dist/package-root/usr/local/bin mkdir /tmp/cbmc-dist/resources mkdir /tmp/cbmc-dist/resources/en.lproj cp ../cbmc/cbmc ../goto-cc/goto-cc \ - ../goto-instrument/goto-instrument /tmp/cbmc-dist/package-root/usr/bin -cp ../../LICENSE /tmp/cbmc-dist/resources/License.txt + ../goto-instrument/goto-instrument /tmp/cbmc-dist/package-root/usr/local/bin/ +cp ../../LICENSE /tmp/cbmc-dist/resources/license.html +cp distribution.xml /tmp/cbmc-dist/ echo "Building cbmc-${VERSION_FILE}.pkg (${BITS} bits)" -#/Applications/PackageMaker.app/Contents/MacOS/PackageMaker \ -# --root /tmp/cbmc-dist/package-root/ \ -# -o /tmp/cbmc-dist/cbmc-${VERSION_FILE}.pkg \ -# --version $VERSION \ -# --title "CBMC ${VERSION}" \ -# --resources /tmp/cbmc-dist/resources/ \ -# --target 10.5 \ -# --id org.cprover.cbmc +# Do the 'component package' pkgbuild \ --root /tmp/cbmc-dist/package-root/ \ --identifier org.cprover.cbmc \ --version $VERSION \ - --verbose \ - /tmp/cbmc-dist/cbmc-${VERSION_FILE}.pkg + /tmp/cbmc-dist/cbmc-component.pkg + +# Now do the 'product archive' + +productbuild \ + --distribution /tmp/cbmc-dist/distribution.xml \ + --resources /tmp/cbmc-dist/resources/ \ + --package-path /tmp/cbmc-dist \ + --version $VERSION \ + /tmp/cbmc-dist/cbmc-${VERSION_FILE}.pkg -#echo Copying. -#scp /tmp/cbmc-dist/cbmc-${VERSION_FILE}.pkg \ -# kroening@dkr-srv.cs.ox.ac.uk:/srv/www/cprover.org/cbmc/download/ +echo Copying. +scp /tmp/cbmc-dist/cbmc-${VERSION_FILE}.pkg \ + kroening@dkr-srv.cs.ox.ac.uk:/srv/www/cprover.org/cbmc/download/ #cd /tmp #rm -R /tmp/cbmc-dist diff --git a/src/cbmc/distribution.xml b/src/cbmc/distribution.xml new file mode 100644 index 00000000000..d87174232dd --- /dev/null +++ b/src/cbmc/distribution.xml @@ -0,0 +1,29 @@ + + + The CBMC Bounded Model Checker + org.cprover.cbmc + + + + + + + + cbmc-component.pkg + + + + + + + + + diff --git a/src/common b/src/common index 3c2659db467..1fab097b524 100644 --- a/src/common +++ b/src/common @@ -100,7 +100,7 @@ else ifeq ($(BUILD_ENV_),Cygwin) CP_CXXFLAGS = -MMD -MP -std=c++11 -U__STRICT_ANSI__ LINKFLAGS = -static -std=c++11 LINKLIB = ar rcT $@ $^ - LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -static + LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -static LINKNATIVE = $(HOSTCXX) -std=c++11 -o $@ $^ -static ifeq ($(origin CC),default) #CC = gcc @@ -127,7 +127,7 @@ else ifeq ($(BUILD_ENV_),MSVC) CFLAGS ?= /W3 /O2 /GF CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF CP_CFLAGS = - CP_CXXFLAGS = + CP_CXXFLAGS = LINKLIB = lib /NOLOGO /OUT:$@ $^ LINKBIN = $(CXX) $(LINKFLAGS) /Fe$@ $^ $(LIBS) LINKNATIVE = $(HOSTCXX) /Fe$@ $^ @@ -161,7 +161,7 @@ CP_CXXFLAGS += $(CXXFLAGS) $(INCLUDES) OBJ += $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) -.SUFFIXES: .cc .d .cpp +.SUFFIXES: .cc .d .cpp %.o:%.cpp $(CXX) -c $(CP_CXXFLAGS) -o $@ $< diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index a09952407fc..115f9270b87 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -12,12 +12,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include #include -#include #include "cpp_internal_additions.h" #include "cpp_language.h" @@ -70,7 +70,7 @@ Function: cpp_languaget::modules_provided void cpp_languaget::modules_provided(std::set &modules) { - modules.insert(translation_unit(parse_path)); + modules.insert(get_base_name(parse_path, true)); } /*******************************************************************\ diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 232b494849b..73230c0723a 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -301,8 +301,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() init_symbol.mode=ID_cpp; init_symbol.module=module; init_symbol.type=code_typet(); - init_symbol.type.add(ID_return_type)=typet(ID_empty); - init_symbol.type.set("initialization", true); + init_symbol.type.add(ID_return_type)=typet(ID_constructor); init_symbol.is_type=false; init_symbol.is_macro=false; diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index bf510f6e210..ed6f626b0df 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -7,6 +7,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../analyses/analyses$(LIBEXT) \ + ../pointer-analysis/pointer-analysis$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../json/json$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 22ece7b9950..444624851df 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -134,7 +134,8 @@ void taint_analysist::instrument( { bool match=false; for(const auto & i : identifiers) - if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":")) + if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":") || + id2string(i)==id2string(rule.function_identifier)) { match=true; break; diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 60b36f865f9..3219e74a88b 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -11,6 +11,7 @@ Date: April 2016 #include #include +#include #include @@ -46,12 +47,6 @@ static void unreachable_instructions( it!=dominators.cfg.entry_map.end(); ++it) { - if(it->first->is_dead() || - (it->first->is_assign() && - to_code_assign(it->first->code).lhs().get(ID_identifier)== - "__CPROVER_dead_object")) - continue; - const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second]; if(n.dominators.empty()) dest.insert(std::make_pair(it->first->location_number, @@ -77,11 +72,7 @@ static void all_unreachable( dead_mapt &dest) { forall_goto_program_instructions(it, goto_program) - if(!it->is_end_function() && - !it->is_dead() && - !(it->is_assign() && - to_code_assign(it->code).lhs().get(ID_identifier)== - "__CPROVER_dead_object")) + if(!it->is_end_function()) dest.insert(std::make_pair(it->location_number, it)); } @@ -145,7 +136,9 @@ static void add_to_json( entry["function"]=json_stringt(id2string(end_function->function)); entry["file name"]= - json_stringt(id2string(end_function->source_location.get_file())); + json_stringt(concat_dir_file( + id2string(end_function->source_location.get_working_directory()), + id2string(end_function->source_location.get_file()))); json_arrayt &dead_ins=entry["unreachable instructions"].make_array(); diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 9bbf51eee5c..0f9c7a85701 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -214,12 +214,7 @@ bool compilet::add_input_file(const std::string &file_name) if(file_name[0]!='/') #endif { - cmd << "ar x " << - #ifdef _WIN32 - working_directory << "\\" << file_name; - #else - working_directory << "/" << file_name; - #endif + cmd << "ar x " << concat_dir_file(working_directory, file_name); } else { @@ -463,7 +458,7 @@ bool compilet::compile() std::string cfn; if(output_file_object=="") - cfn=get_base_name(file_name) + "." + object_file_extension; + cfn=get_base_name(file_name, true)+"."+object_file_extension; else cfn=output_file_object; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index 2a4eb3a0c7b..73a38a2d603 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -75,6 +75,4 @@ class compilet:public language_uit void convert_symbols(goto_functionst &dest); }; -std::string get_base_name(const std::string &); - #endif /*COMPILE_H_*/ diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp index e89a24cd984..9ebb0e2d94a 100644 --- a/src/goto-cc/gcc_cmdline.cpp +++ b/src/goto-cc/gcc_cmdline.cpp @@ -74,6 +74,7 @@ const char *gcc_options_with_separated_argument[]= "--include", // undocumented "-current_version", // on the Mac "-compatibility_version", // on the Mac + "-z", NULL }; diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index c08eddb59fc..3991aa823bc 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -15,6 +15,7 @@ Author: CM Wintersteiger, 2006 #include #include #include +#include #include @@ -64,8 +65,8 @@ Function: gcc_modet::doit bool gcc_modet::doit() { act_as_ld= - has_prefix(base_name, "ld") || - has_prefix(base_name, "goto-ld"); + base_name=="ld" || + base_name.find("goto-ld")!=std::string::npos; if(cmdline.isset('?') || cmdline.isset("help")) @@ -156,9 +157,10 @@ bool gcc_modet::doit() config.set(cmdline); // Intel-specific - if(cmdline.isset("m16")) - config.ansi_c.set_16(); - else if(cmdline.isset("m32") || cmdline.isset("mx32")) + // in GCC, m16 is 32-bit (!), as documented here: + // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59672 + if(cmdline.isset("m16") || + cmdline.isset("m32") || cmdline.isset("mx32")) { config.ansi_c.arch="i386"; config.ansi_c.set_arch_spec_i386(); @@ -342,7 +344,8 @@ bool gcc_modet::doit() else new_suffix=has_suffix(arg_it->arg, ".c")?".i":".ii"; - std::string new_name=get_base_name(arg_it->arg)+new_suffix; + std::string new_name= + get_base_name(arg_it->arg, true)+new_suffix; std::string dest=temp_dir(new_name); int exit_code=preprocess(language, arg_it->arg, dest); @@ -392,7 +395,7 @@ bool gcc_modet::doit() // We can generate hybrid ELF and Mach-O binaries // containing both executable machine code and the goto-binary. - if(produce_hybrid_binary) + if(!result && produce_hybrid_binary) { if(gcc_hybrid_binary()) result=true; @@ -477,9 +480,11 @@ int gcc_modet::preprocess( // source file new_argv.push_back(src); + const char *compiler=compiler_name(); + // overwrite argv[0] assert(new_argv.size()>=1); - new_argv[0]=compiler_name(); + new_argv[0]=compiler; #if 0 std::cout << "RUN:"; @@ -488,7 +493,7 @@ int gcc_modet::preprocess( std::cout << std::endl; #endif - return run(compiler_name(), new_argv); + return run(compiler, new_argv, cmdline.stdin_file); } /*******************************************************************\ @@ -518,11 +523,13 @@ int gcc_modet::run_gcc() new_argv.push_back(it->arg); } - const char *compiler=compiler_name(); - // overwrite argv[0] assert(new_argv.size()>=1); - new_argv[0]=compiler; + + if(act_as_ld) + new_argv[0]=linker_name(); + else + new_argv[0]=compiler_name(); #if 0 std::cout << "RUN:"; @@ -531,7 +538,7 @@ int gcc_modet::run_gcc() std::cout << std::endl; #endif - return run(compiler, new_argv); + return run(new_argv[0], new_argv, cmdline.stdin_file); } /*******************************************************************\ @@ -577,11 +584,9 @@ int gcc_modet::gcc_hybrid_binary() i_it=cmdline.parsed_argv.begin(); i_it!=cmdline.parsed_argv.end(); i_it++) - if(i_it->is_infile_name) - { - if(needs_preprocessing(i_it->arg)) - output_files.push_back(get_base_name(i_it->arg)+".o"); - } + if(i_it->is_infile_name && + needs_preprocessing(i_it->arg)) + output_files.push_back(get_base_name(i_it->arg, true)+".o"); } } else @@ -593,7 +598,9 @@ int gcc_modet::gcc_hybrid_binary() output_files.push_back("a.out"); } - if(output_files.empty()) return 0; + if(output_files.empty() || + (output_files.size()==1 && + output_files.front()=="/dev/null")) return 0; if(act_as_ld) debug() << "Running ld to generate hybrid binary" << eom; @@ -639,7 +646,7 @@ int gcc_modet::gcc_hybrid_binary() assert(new_argv.size()>=1); if(act_as_ld) - new_argv[0]="ld"; + new_argv[0]=linker_name(); else new_argv[0]=compiler_name(); @@ -650,10 +657,10 @@ int gcc_modet::gcc_hybrid_binary() std::cout << std::endl; #endif - int result=run(new_argv[0], new_argv); + int result=run(new_argv[0], new_argv, ""); // merge output from gcc with goto-binaries - // using objcopy + // using objcopy, or do cleanup if an earlier call failed for(std::list::const_iterator it=output_files.begin(); it!=output_files.end(); @@ -663,7 +670,7 @@ int gcc_modet::gcc_hybrid_binary() std::string saved=*it+".goto-cc-saved"; #ifdef __linux__ - if(!cmdline.isset('c')) + if(result==0 && !cmdline.isset('c')) { // remove any existing goto-cc section std::vector objcopy_argv; @@ -672,35 +679,41 @@ int gcc_modet::gcc_hybrid_binary() objcopy_argv.push_back("--remove-section=goto-cc"); objcopy_argv.push_back(*it); - run(objcopy_argv[0], objcopy_argv); + result=run(objcopy_argv[0], objcopy_argv, ""); } - // now add goto-binary as goto-cc section - std::vector objcopy_argv; - - objcopy_argv.push_back("objcopy"); - objcopy_argv.push_back("--add-section"); - objcopy_argv.push_back("goto-cc="+saved); - objcopy_argv.push_back(*it); - - run(objcopy_argv[0], objcopy_argv); + if(result==0) + { + // now add goto-binary as goto-cc section + std::vector objcopy_argv; + + objcopy_argv.push_back("objcopy"); + objcopy_argv.push_back("--add-section"); + objcopy_argv.push_back("goto-cc="+saved); + objcopy_argv.push_back(*it); + + result=run(objcopy_argv[0], objcopy_argv, ""); + } remove(saved.c_str()); #elif defined(__APPLE__) // Mac - std::vector lipo_argv; - - // now add goto-binary as hppa7100LC section - lipo_argv.push_back("lipo"); - lipo_argv.push_back(*it); - lipo_argv.push_back("-create"); - lipo_argv.push_back("-arch"); - lipo_argv.push_back("hppa7100LC"); - lipo_argv.push_back(saved); - lipo_argv.push_back("-output"); - lipo_argv.push_back(*it); - - run(lipo_argv[0], lipo_argv); + if(result==0) + { + std::vector lipo_argv; + + // now add goto-binary as hppa7100LC section + lipo_argv.push_back("lipo"); + lipo_argv.push_back(*it); + lipo_argv.push_back("-create"); + lipo_argv.push_back("-arch"); + lipo_argv.push_back("hppa7100LC"); + lipo_argv.push_back(saved); + lipo_argv.push_back("-output"); + lipo_argv.push_back(*it); + + result=run(lipo_argv[0], lipo_argv, ""); + } remove(saved.c_str()); diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h index a1df04cf6eb..0e3b21a9667 100644 --- a/src/goto-cc/gcc_mode.h +++ b/src/goto-cc/gcc_mode.h @@ -31,6 +31,7 @@ class gcc_modet:public goto_cc_modet protected: bool act_as_ld; + std::string native_compiler_name; int preprocess( const std::string &language, @@ -43,13 +44,52 @@ class gcc_modet:public goto_cc_modet static bool needs_preprocessing(const std::string &); - static inline const char *compiler_name() + inline const char *compiler_name() { - #ifdef __FreeBSD__ - return "clang"; - #else - return "gcc"; - #endif + if(native_compiler_name.empty()) + { + std::string::size_type pos=base_name.find("goto-gcc"); + + if(pos==std::string::npos || + base_name=="goto-gcc" || + base_name=="goto-ld") + { + #ifdef __FreeBSD__ + native_compiler_name="clang"; + #else + native_compiler_name="gcc"; + #endif + } + else + { + native_compiler_name=base_name; + native_compiler_name.replace(pos, 8, "gcc"); + } + } + + return native_compiler_name.c_str(); + } + + inline const char *linker_name() + { + if(native_compiler_name.empty()) + { + std::string::size_type pos=base_name.find("goto-ld"); + + if(pos==std::string::npos || + base_name=="goto-gcc" || + base_name=="goto-ld") + { + native_compiler_name="ld"; + } + else + { + native_compiler_name=base_name; + native_compiler_name.replace(pos, 7, "ld"); + } + } + + return native_compiler_name.c_str(); } }; diff --git a/src/goto-cc/goto_cc_cmdline.cpp b/src/goto-cc/goto_cc_cmdline.cpp index 005b74d20cd..7d170d00b3d 100644 --- a/src/goto-cc/goto_cc_cmdline.cpp +++ b/src/goto-cc/goto_cc_cmdline.cpp @@ -10,13 +10,33 @@ Date: April 2010 #include #include +#include #include +#include #include "goto_cc_cmdline.h" /*******************************************************************\ +Function: goto_cc_cmdlinet::~goto_cc_cmdlinet + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +goto_cc_cmdlinet::~goto_cc_cmdlinet() +{ + if(!stdin_file.empty()) + remove(stdin_file.c_str()); +} + +/*******************************************************************\ + Function: goto_cc_cmdlinet::in_list Inputs: @@ -131,3 +151,34 @@ std::size_t goto_cc_cmdlinet::get_optnr(const std::string &opt_string) return optnr; } + +/*******************************************************************\ + +Function: goto_cc_cmdlinet::add_infile_arg + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_cc_cmdlinet::add_infile_arg(const std::string &arg) +{ + parsed_argv.push_back(argt(arg)); + parsed_argv.back().is_infile_name=true; + + if(arg=="-") + { + stdin_file=get_temporary_file("goto-cc", "stdin"); + + FILE *tmp=fopen(stdin_file.c_str(), "wt"); + + char ch; + while(std::cin.read(&ch, 1)) + fputc(ch, tmp); + + fclose(tmp); + } +} diff --git a/src/goto-cc/goto_cc_cmdline.h b/src/goto-cc/goto_cc_cmdline.h index d8e2c474cb6..3115ee4c99c 100644 --- a/src/goto-cc/goto_cc_cmdline.h +++ b/src/goto-cc/goto_cc_cmdline.h @@ -16,6 +16,8 @@ Date: April 2010 class goto_cc_cmdlinet:public cmdlinet { public: + ~goto_cc_cmdlinet(); + using cmdlinet::parse; virtual bool parse(int argc, const char **argv)=0; @@ -65,17 +67,15 @@ class goto_cc_cmdlinet:public cmdlinet return false; } + std::string stdin_file; + protected: void add_arg(const std::string &arg) { parsed_argv.push_back(argt(arg)); } - void add_infile_arg(const std::string &arg) - { - parsed_argv.push_back(argt(arg)); - parsed_argv.back().is_infile_name=true; - } + void add_infile_arg(const std::string &arg); }; #endif /* GOTO_CC_CMDLINE_H */ diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-cc/goto_cc_main.cpp index 59bb21ba74d..4e20b24165e 100644 --- a/src/goto-cc/goto_cc_main.cpp +++ b/src/goto-cc/goto_cc_main.cpp @@ -72,9 +72,13 @@ int main(int argc, const char **argv) return 1; } + #ifdef _MSC_VER // we do 'to_lower_string' because of Windows std::string base_name= - to_lower_string(get_base_name(argv[0])); + to_lower_string(get_base_name(argv[0], true)); + #else + std::string base_name=get_base_name(argv[0], false); + #endif if(base_name=="goto-link" || base_name=="link" || base_name=="goto-cl" || base_name=="cl") @@ -105,7 +109,10 @@ int main(int argc, const char **argv) armcc_mode.base_name=base_name; return armcc_mode.main(argc, argv); } - else if(base_name=="goto-gcc") + // handle GCC names like x86_64-apple-darwin14-llvm-gcc-4.2 + // via x86_64-apple-darwin14-llvm-goto-gcc-4.2 + else if(base_name=="goto-clang" || + base_name.find("goto-gcc")!=std::string::npos) { // this produces ELF/Mach-O "hybrid binaries", // with a GCC-style command-line interface, @@ -116,7 +123,7 @@ int main(int argc, const char **argv) gcc_mode.produce_hybrid_binary=true; return gcc_mode.main(argc, argv); } - else if(base_name=="goto-ld") + else if(base_name.find("goto-ld")!=std::string::npos) { // this simulates "ld" for linking ld_cmdlinet cmdline; diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 5f1acca8ab1..067b28d069d 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -12,6 +12,7 @@ Author: CM Wintersteiger, 2006 #include #include #include +#include #include @@ -87,11 +88,10 @@ bool ms_cl_modet::doit() compiler.output_file_object=cmdline.get_value("Fo"); // this could be a directory - if(is_directory(compiler.output_file_object)) - { - if(cmdline.args.size()>=1) - compiler.output_file_object+=get_base_name(cmdline.args[0])+".obj"; - } + if(is_directory(compiler.output_file_object) && + cmdline.args.size()>=1) + compiler.output_file_object+= + get_base_name(cmdline.args[0], true)+".obj"; } if(cmdline.isset("Fe")) @@ -99,18 +99,18 @@ bool ms_cl_modet::doit() compiler.output_file_executable=cmdline.get_value("Fe"); // this could be a directory - if(is_directory(compiler.output_file_executable)) - { - if(cmdline.args.size()>=1) - compiler.output_file_executable+=get_base_name(cmdline.args[0])+".exe"; - } + if(is_directory(compiler.output_file_executable) && + cmdline.args.size()>=1) + compiler.output_file_executable+= + get_base_name(cmdline.args[0], true)+".exe"; } else { // We need at least one argument. // CL uses the first file name it gets! if(cmdline.args.size()>=1) - compiler.output_file_executable=get_base_name(cmdline.args[0])+".exe"; + compiler.output_file_executable= + get_base_name(cmdline.args[0], true)+".exe"; } if(cmdline.isset('J')) diff --git a/src/goto-cc/run.cpp b/src/goto-cc/run.cpp index f689b6f45f3..e566026ec32 100644 --- a/src/goto-cc/run.cpp +++ b/src/goto-cc/run.cpp @@ -8,6 +8,8 @@ Date: August 2012 \*******************************************************************/ +#include + #ifdef _WIN32 #include #else @@ -20,6 +22,7 @@ Date: August 2012 #include #include +#include #endif @@ -41,9 +44,13 @@ Function: run int run( const std::string &what, - const std::vector &argv) + const std::vector &argv, + const std::string &std_input) { #ifdef _WIN32 + // we don't support stdin on Windows + assert(std_input.empty()); + // unicode version of the arguments std::vector wargv; @@ -70,6 +77,18 @@ int run( return status; #else + int stdin_fd=STDIN_FILENO; + + if(!std_input.empty()) + { + stdin_fd=open(std_input.c_str(), O_RDONLY); + if(stdin_fd==-1) + { + perror("Failed to open stdin copy"); + return 1; + } + } + pid_t childpid; /* variable to store the child's pid */ /* now create new process */ @@ -85,6 +104,8 @@ int run( _argv[argv.size()]=NULL; + if(stdin_fd!=STDIN_FILENO) + dup2(stdin_fd, STDIN_FILENO); execvp(what.c_str(), _argv); /* usually no return */ return 1; @@ -99,13 +120,23 @@ int run( else { perror("Waiting for child process failed"); + if(stdin_fd!=STDIN_FILENO) + close(stdin_fd); return 1; } + if(stdin_fd!=STDIN_FILENO) + close(stdin_fd); + return WEXITSTATUS(status); } } else /* fork returns -1 on failure */ + { + if(stdin_fd!=STDIN_FILENO) + close(stdin_fd); + return 1; + } #endif } diff --git a/src/goto-cc/run.h b/src/goto-cc/run.h index b1cca1c156e..9e2c88473dd 100644 --- a/src/goto-cc/run.h +++ b/src/goto-cc/run.h @@ -16,6 +16,7 @@ Date: August 2012 int run( const std::string &what, - const std::vector &argv); + const std::vector &argv, + const std::string &std_input); #endif /* GOTO_CC_RUN_H */ diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 5bf5ee276a4..5a92186fda7 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -11,12 +11,17 @@ Date: December 2012 #include #include +#include #include "count_eloc.h" +typedef hash_set_cont linest; +typedef hash_map_cont filest; +typedef hash_map_cont working_dirst; + /*******************************************************************\ -Function: count_eloc +Function: collect_eloc Inputs: @@ -26,16 +31,22 @@ Function: count_eloc \*******************************************************************/ -std::size_t count_eloc(const goto_programt &goto_program) +static void collect_eloc( + const goto_functionst &goto_functions, + working_dirst &dest) { - hash_set_cont lines; - - forall_goto_program_instructions(it, goto_program) - if(it->source_location.is_not_nil() && - !has_prefix(id2string(it->source_location.get_file()), "source_location.get_line()); - - return lines.size(); + forall_goto_functions(f_it, goto_functions) + { + forall_goto_program_instructions(it, f_it->second.body) + { + filest &files=dest[it->source_location.get_working_directory()]; + const irep_idt &file=it->source_location.get_file(); + + if(!file.empty() && + !has_prefix(id2string(file), "source_location.get_line()); + } + } } /*******************************************************************\ @@ -53,10 +64,42 @@ Function: count_eloc void count_eloc(const goto_functionst &goto_functions) { std::size_t eloc=0; - - forall_goto_functions(f_it, goto_functions) - eloc+=count_eloc(f_it->second.body); + + working_dirst eloc_map; + collect_eloc(goto_functions, eloc_map); + + for(const std::pair &files : eloc_map) + for(const std::pair &lines : files.second) + eloc+=lines.second.size(); std::cout << "Effective lines of code: " << eloc << '\n'; } +/*******************************************************************\ + +Function: list_eloc + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void list_eloc(const goto_functionst &goto_functions) +{ + working_dirst eloc_map; + collect_eloc(goto_functions, eloc_map); + + for(const std::pair &files : eloc_map) + for(const std::pair &lines : files.second) + { + std::string file=id2string(lines.first); + if(!files.first.empty()) + file=concat_dir_file(id2string(files.first), file); + + for(const irep_idt &line : lines.second) + std::cout << file << ':' << line << '\n'; + } +} diff --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index 1228e035f49..f3417606f5b 100644 --- a/src/goto-instrument/count_eloc.h +++ b/src/goto-instrument/count_eloc.h @@ -15,4 +15,6 @@ Date: December 2012 void count_eloc(const goto_functionst &goto_functions); +void list_eloc(const goto_functionst &goto_functions); + #endif diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index ed252966d9e..c0fa79158f8 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -8,7 +8,10 @@ Date: May 2016 \*******************************************************************/ +#include + #include +#include #include "cover.h" @@ -27,15 +30,23 @@ class basic_blockst block_map[it]=block_count; + if(!it->source_location.is_nil() && + source_location_map.find(block_count)==source_location_map.end()) + source_location_map[block_count]=it->source_location; + next_is_target= - it->is_goto() || it->is_return() || - it->is_function_call() || it->is_assume(); + it->is_goto() || it->is_function_call(); } } - + + // map program locations to block numbers typedef std::map block_mapt; block_mapt block_map; + // map block numbers to source code locations + typedef std::map source_location_mapt; + source_location_mapt source_location_map; + inline unsigned operator[](goto_programt::const_targett t) { return block_map[t]; @@ -53,6 +64,18 @@ class basic_blockst } }; +/*******************************************************************\ + +Function: as_string + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + const char *as_string(coverage_criteriont c) { switch(c) @@ -64,13 +87,14 @@ const char *as_string(coverage_criteriont c) case coverage_criteriont::PATH: return "path"; case coverage_criteriont::MCDC: return "MC/DC"; case coverage_criteriont::ASSERTION: return "assertion"; + case coverage_criteriont::COVER: return "cover instructions"; default: return ""; } } /*******************************************************************\ -Function: collect_conditions +Function: is_condition Inputs: @@ -80,25 +104,308 @@ Function: collect_conditions \*******************************************************************/ -void collect_conditions(const exprt &src, std::set &dest) +bool is_condition(const exprt &src) { + if(src.type().id()!=ID_bool) return false; + + // conditions are 'atomic predicates' if(src.id()==ID_and || src.id()==ID_or || src.id()==ID_not || src.id()==ID_implies) + return false; + + return true; +} + +/*******************************************************************\ + +Function: collect_conditions_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void collect_conditions_rec(const exprt &src, std::set &dest) +{ + if(src.id()==ID_address_of) + { + return; + } + + for(const auto & op : src.operands()) + collect_conditions_rec(op, dest); + + if(is_condition(src) && !src.is_constant()) + dest.insert(src); +} + +/*******************************************************************\ + +Function: collect_conditions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set collect_conditions(const exprt &src) +{ + std::set result; + collect_conditions_rec(src, result); + return result; +} + +/*******************************************************************\ + +Function: collect_conditions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set collect_conditions(const goto_programt::const_targett t) +{ + switch(t->type) { - forall_operands(it, src) - collect_conditions(*it, dest); + case GOTO: + case ASSERT: + return collect_conditions(t->guard); + + case ASSIGN: + case FUNCTION_CALL: + return collect_conditions(t->code); + + default:; } - else if(src.is_true()) + + return std::set(); +} + +/*******************************************************************\ + +Function: collect_operands + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void collect_operands(const exprt &src, std::vector &dest) +{ + for(const exprt &op : src.operands()) { + if(op.id()==src.id()) + collect_operands(op, dest); + else + dest.push_back(op); + } +} + +/*******************************************************************\ + +Function: collect_mcdc_controlling_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void collect_mcdc_controlling_rec( + const exprt &src, + const std::vector &conditions, + std::set &result) +{ + if(src.id()==ID_and || + src.id()==ID_or) + { + std::vector operands; + collect_operands(src, operands); + + if(operands.size()==1) + { + exprt e=*operands.begin(); + collect_mcdc_controlling_rec(e, conditions, result); + } + else if(!operands.empty()) + { + for(unsigned i=0; i o=operands; + + // 'o[i]' needs to be true and false + std::vector new_conditions=conditions; + new_conditions.push_back(conjunction(o)); + result.insert(conjunction(new_conditions)); + + o[i].make_not(); + new_conditions.back()=conjunction(o); + result.insert(conjunction(new_conditions)); + } + else + { + std::vector others; + others.reserve(operands.size()-1); + + for(unsigned j=0; j new_conditions=conditions; + new_conditions.push_back(c); + + collect_mcdc_controlling_rec(op, new_conditions, result); + } + } + } + } + else if(src.id()==ID_not) + { + exprt e=to_not_expr(src).op(); + collect_mcdc_controlling_rec(e, conditions, result); + } +} + +/*******************************************************************\ + +Function: collect_mcdc_controlling + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set collect_mcdc_controlling( + const std::set &decisions) +{ + std::set result; + + for(const auto &d : decisions) + collect_mcdc_controlling_rec(d, { }, result); + + return result; +} + +/*******************************************************************\ + +Function: collect_decisions_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void collect_decisions_rec(const exprt &src, std::set &dest) +{ + if(src.id()==ID_address_of) + { + return; + } + + if(src.type().id()==ID_bool) + { + if(src.is_constant()) + { + // ignore me + } + else if(src.id()==ID_not) + { + collect_decisions_rec(src.op0(), dest); + } + else + { + dest.insert(src); + } } else { - dest.insert(src); + for(const auto & op : src.operands()) + collect_decisions_rec(op, dest); } } /*******************************************************************\ +Function: collect_decisions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set collect_decisions(const exprt &src) +{ + std::set result; + collect_decisions_rec(src, result); + return result; +} + +/*******************************************************************\ + +Function: collect_decisions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set collect_decisions(const goto_programt::const_targett t) +{ + switch(t->type) + { + case GOTO: + case ASSERT: + return collect_decisions(t->guard); + + case ASSIGN: + case FUNCTION_CALL: + return collect_decisions(t->code); + + default:; + } + + return std::set(); +} + +/*******************************************************************\ + Function: instrument_cover_goals Inputs: @@ -124,22 +431,50 @@ void instrument_cover_goals( { case coverage_criteriont::ASSERTION: // turn into 'assert(false)' to avoid simplification - i_it->guard=false_exprt(); + if(i_it->is_assert()) + i_it->guard=false_exprt(); + break; + + case coverage_criteriont::COVER: + // turn __CPROVER_cover(x) into 'assert(!x)' + if(i_it->is_function_call()) + { + const code_function_callt &code_function_call= + to_code_function_call(i_it->code); + if(code_function_call.function().id()==ID_symbol && + to_symbol_expr(code_function_call.function()).get_identifier()== + "__CPROVER_cover" && + code_function_call.arguments().size()==1) + { + const exprt c=code_function_call.arguments()[0]; + std::string comment="condition `"+from_expr(ns, "", c)+"'"; + i_it->guard=not_exprt(c); + i_it->type=ASSERT; + i_it->code.clear(); + i_it->source_location.set_comment(comment); + } + } + else if(i_it->is_assert()) + i_it->make_skip(); break; case coverage_criteriont::LOCATION: + if(i_it->is_assert()) + i_it->make_skip(); + { unsigned block_nr=basic_blocks[i_it]; if(blocks_done.insert(block_nr).second) { std::string b=i2string(block_nr); std::string id=id2string(i_it->function)+"#"+b; - if(i_it->source_location.get_file()!="") + source_locationt source_location= + basic_blocks.source_location_map[block_nr]; + + if(!source_location.get_file().empty() && + source_location.get_file()[0]!='<') { - std::string comment= - "block "+i_it->source_location.as_string()+" "+i2string(i_it->location_number); - - source_locationt source_location=i_it->source_location; + std::string comment="block "+b; goto_program.insert_before_swap(i_it); i_it->make_assertion(false_exprt()); i_it->source_location=source_location; @@ -164,46 +499,156 @@ void instrument_cover_goals( source_locationt source_location=i_it->source_location; goto_program.insert_before_swap(i_it); - i_it->make_assertion(guard); + i_it->make_assertion(not_exprt(guard)); i_it->source_location=source_location; i_it->source_location.set_comment(true_comment); goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(guard)); + i_it->make_assertion(guard); i_it->source_location=source_location; i_it->source_location.set_comment(false_comment); i_it++; i_it++; } + else if(i_it->is_assert()) + i_it->make_skip(); + break; case coverage_criteriont::CONDITION: - if(i_it->is_goto()) + if(i_it->is_assert()) + i_it->make_skip(); + + // Conditions are all atomic predicates in the programs. { - std::set conditions; + const std::set conditions=collect_conditions(i_it); - collect_conditions(i_it->guard, conditions); - unsigned i=0; + const source_locationt source_location=i_it->source_location; - exprt guard=i_it->guard; - source_locationt source_location=i_it->source_location; + for(const auto & c : conditions) + { + const std::string c_string=from_expr(ns, "", c); + + const std::string comment_t="condition `"+c_string+"' true"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(c); + i_it->source_location=source_location; + i_it->source_location.set_comment(comment_t); + + const std::string comment_f="condition `"+c_string+"' false"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(c)); + i_it->source_location=source_location; + i_it->source_location.set_comment(comment_f); + } + + for(unsigned i=0; iis_assert()) + i_it->make_skip(); + + // Decisions are maximal Boolean combinations of conditions. + { + const std::set decisions=collect_decisions(i_it); + + const source_locationt source_location=i_it->source_location; + + for(const auto & d : decisions) + { + const std::string d_string=from_expr(ns, "", d); + + const std::string comment_t="decision `"+d_string+"' true"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(d); + i_it->source_location=source_location; + i_it->source_location.set_comment(comment_t); + + const std::string comment_f="decision `"+d_string+"' false"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(d)); + i_it->source_location=source_location; + i_it->source_location.set_comment(comment_f); + } + + for(unsigned i=0; iis_assert()) + i_it->make_skip(); + + // 1. Each entry and exit point is invoked + // 2. Each decision takes every possible outcome + // 3. Each condition in a decision takes every possible outcome + // 4. Each condition in a decision is shown to independently + // affect the outcome of the decision. + { + const std::set conditions=collect_conditions(i_it); + const std::set decisions=collect_decisions(i_it); + + std::set both; + std::set_union(conditions.begin(), conditions.end(), + decisions.begin(), decisions.end(), + inserter(both, both.end())); + + const source_locationt source_location=i_it->source_location; - for(std::set::const_iterator it=conditions.begin(); - it!=conditions.end(); - it++, i++) + for(const auto & p : both) { - std::string comment="condition "+from_expr(ns, "", *it); + bool is_decision=decisions.find(p)!=decisions.end(); + bool is_condition=conditions.find(p)!=conditions.end(); + + std::string description= + (is_decision && is_condition)?"decision/condition": + is_decision?"decision":"condition"; + + std::string p_string=from_expr(ns, "", p); + + std::string comment_t=description+" `"+p_string+"' true"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(*it); + i_it->make_assertion(p); i_it->source_location=source_location; - i_it->source_location.set_comment(comment); + i_it->source_location.set_comment(comment_t); + + std::string comment_f=description+" `"+p_string+"' false"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(p)); + i_it->source_location=source_location; + i_it->source_location.set_comment(comment_f); + } + + std::set controlling; + controlling=collect_mcdc_controlling(decisions); + + for(const auto & p : controlling) + { + std::string p_string=from_expr(ns, "", p); + + std::string description= + "MC/DC independence condition `"+p_string+"'"; + + goto_program.insert_before_swap(i_it); + i_it->make_assertion(p); + i_it->source_location=source_location; + i_it->source_location.set_comment(description); } - for(unsigned i=0; iis_assert()) + i_it->make_skip(); + break; default:; } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 962965ed598..cf51972f6e6 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -15,7 +15,7 @@ Date: May 2016 enum class coverage_criteriont { LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, ASSERTION }; + PATH, MCDC, ASSERTION, COVER }; void instrument_cover_goals( const symbol_tablet &symbol_table, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6e1c04075a9..14759d53a58 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -407,6 +407,12 @@ int goto_instrument_parse_optionst::doit() return 0; } + if(cmdline.isset("list-eloc")) + { + list_eloc(goto_functions); + return 0; + } + if(cmdline.isset("list-symbols")) { show_symbol_table(true); @@ -1271,6 +1277,7 @@ void goto_instrument_parse_optionst::help() " --dot generate CFG graph in DOT format\n" " --interpreter do concrete execution\n" " --count-eloc count effective lines of code\n" + " --list-eloc list full path names of lines containing code\n" "\n" "Diagnosis:\n" " --show-loops show the loops in the program\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index abd41931081..7348e44c3c9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -58,7 +58,7 @@ Author: Daniel Kroening, kroening@kroening.com "(accelerate)(constant-propagator)" \ "(k-induction):(step-case)(base-case)" \ "(show-call-sequences)(check-call-sequence)" \ - "(interpreter)(show-reaching-definitions)(count-eloc)" \ + "(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ "(horn)(skip-loops):(apply-code-contracts)" diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 4bb8ef4cbd0..4d27d31c388 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -270,53 +270,6 @@ void goto_convertt::do_input( /*******************************************************************\ -Function: goto_convertt::do_cover - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_convertt::do_cover( - const exprt &lhs, - const exprt &function, - const exprt::operandst &arguments, - goto_programt &dest) -{ - codet output_code; - output_code.set_statement(ID_output); - output_code.add_source_location()=function.source_location(); - - if(arguments.size()!=1) - { - err_location(function); - throw "cover takes one argument"; - } - - // build string constant - exprt string_constant(ID_string_constant); - string_constant.type()=array_typet(); - string_constant.type().subtype()=char_type(); - string_constant.set(ID_value, ID_cover); - - index_exprt index_expr; - index_expr.type()=char_type(); - index_expr.array()=string_constant; - index_expr.index()=gen_zero(index_type()); - - output_code.copy_to_operands(address_of_exprt(index_expr)); - - forall_expr(it, arguments) - output_code.copy_to_operands(*it); - - copy(output_code, OTHER, dest); -} - -/*******************************************************************\ - Function: goto_convertt::do_output Inputs: @@ -1154,11 +1107,6 @@ void goto_convertt::do_function_call_symbol( { do_input(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "cover" || - identifier=="__CPROVER::cover") - { - do_cover(lhs, function, arguments, dest); - } else if(identifier==CPROVER_PREFIX "output" || identifier=="__CPROVER::output") { @@ -1250,60 +1198,31 @@ void goto_convertt::do_function_call_symbol( { do_printf(lhs, function, arguments, dest); } - else if(identifier=="__assert_fail") + else if(identifier=="__assert_fail" || + identifier=="_assert" || + identifier=="__assert_c99" || + identifier=="_wassert") { // __assert_fail is Linux // These take four arguments: // "expression", "file.c", line, __func__ + // klibc has __assert_fail with 3 arguments + // "expression", "file.c", line - if(arguments.size()!=4) - { - err_location(function); - throw "`"+id2string(identifier)+"' expected to have four arguments"; - } - - const irep_idt description= - "assertion "+id2string(get_string_constant(arguments[0])); - - goto_programt::targett t=dest.add_instruction(ASSERT); - t->guard=false_exprt(); - t->source_location=function.source_location(); - t->source_location.set("user-provided", true); - t->source_location.set_property_class(ID_assertion); - t->source_location.set_comment(description); - // we ignore any LHS - } - else if(identifier=="_assert") - { // MingW has // void _assert (const char*, const char*, int); // with three arguments: // "expression", "file.c", line - if(arguments.size()!=3) - { - err_location(function); - throw "`"+id2string(identifier)+"' expected to have three arguments"; - } - - const irep_idt description= - "assertion "+id2string(get_string_constant(arguments[0])); - - goto_programt::targett t=dest.add_instruction(ASSERT); - t->guard=false_exprt(); - t->source_location=function.source_location(); - t->source_location.set("user-provided", true); - t->source_location.set_property_class(ID_assertion); - t->source_location.set_comment(description); - // we ignore any LHS - } - else if(identifier=="__assert_c99") - { // This has been seen in Solaris 11. // Signature: // void __assert_c99(const char *desc, const char *file, int line, const char *func); - if(arguments.size()!=4) + // _wassert is Windows. The arguments are + // L"expression", L"file.c", line + + if(arguments.size()!=4 && + arguments.size()!=3) { err_location(function); throw "`"+id2string(identifier)+"' expected to have four arguments"; @@ -1369,28 +1288,6 @@ void goto_convertt::do_function_call_symbol( const irep_idt description= "assertion "+id2string(get_string_constant(arguments[3])); - goto_programt::targett t=dest.add_instruction(ASSERT); - - t->guard=false_exprt(); - t->source_location=function.source_location(); - t->source_location.set("user-provided", true); - t->source_location.set_property_class(ID_assertion); - t->source_location.set_comment(description); - // we ignore any LHS - } - else if(identifier=="_wassert") - { - // This is Windows. The arguments are - // L"expression", L"file.c", line - - if(arguments.size()!=3) - { - err_location(function); - throw "`"+id2string(identifier)+"' expected to have three arguments"; - } - - const irep_idt description= - "assertion "+id2string(get_string_constant(arguments[0])); goto_programt::targett t=dest.add_instruction(ASSERT); t->guard=false_exprt(); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 2033f974837..4afea029858 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -419,8 +419,6 @@ void goto_convertt::convert( const codet &code, goto_programt &dest) { - std::size_t old_tmp_symbols_size=tmp_symbols.size(); - const irep_idt &statement=code.get_statement(); if(statement==ID_block) @@ -542,8 +540,6 @@ void goto_convertt::convert( else copy(code, OTHER, dest); - kill_tmp_symbols(old_tmp_symbols_size, dest); - // make sure dest is never empty if(dest.instructions.empty()) { @@ -555,31 +551,6 @@ void goto_convertt::convert( /*******************************************************************\ -Function: goto_convertt::kill_tmp_symbols - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_convertt::kill_tmp_symbols( - std::size_t final_size, - goto_programt &dest) -{ - while(tmp_symbols.size()>final_size) - { - symbol_exprt symbol=tmp_symbols.back(); - tmp_symbols.pop_back(); - dest.add_instruction(DEAD); - dest.instructions.back().code=code_deadt(symbol); - } -} - -/*******************************************************************\ - Function: goto_convertt::convert_block Inputs: @@ -606,8 +577,16 @@ void goto_convertt::convert_block( convert(b_code, dest); } - // see if we need to do any destructors - unwind_destructor_stack(end_location, old_stack_size, dest); + // see if we need to do any destructors -- may have been processed + // in a prior break/continue/return already, don't create dead code + if(!dest.empty() && + dest.instructions.back().is_goto() && + dest.instructions.back().guard.is_true()) + { + // don't do destructors when we are unreachable + } + else + unwind_destructor_stack(end_location, old_stack_size, dest); // remove those destructors targets.destructor_stack.resize(old_stack_size); @@ -1577,7 +1556,7 @@ void goto_convertt::convert_return( // Need to process _entire_ destructor stack. unwind_destructor_stack(code.source_location(), 0, dest); - + // add goto to end-of-function goto_programt::targett t=dest.add_instruction(); t->make_goto(targets.return_target, true_exprt()); @@ -2151,7 +2130,17 @@ void goto_convertt::generate_ifthenelse( { if(is_empty(true_case) && is_empty(false_case)) + { + // hmpf. Useless branch. + goto_programt tmp_z; + goto_programt::targett z=tmp_z.add_instruction(); + z->make_skip(); + goto_programt::targett v=dest.add_instruction(); + v->make_goto(z, guard); + v->source_location=source_location; + dest.destructive_append(tmp_z); return; + } // do guarded gotos directly if(is_empty(false_case) && @@ -2224,7 +2213,8 @@ void goto_convertt::generate_ifthenelse( goto_programt tmp_z; goto_programt::targett z=tmp_z.add_instruction(); z->make_skip(); - z->source_location=source_location; + // We deliberately don't set a location for 'z', it's a dummy + // target. // y: Q; goto_programt tmp_y; @@ -2535,11 +2525,10 @@ symbolt &goto_convertt::new_tmp_symbol( new_symbol.location=source_location; } while(symbol_table.move(new_symbol, symbol_ptr)); - tmp_symbols.push_back(symbol_ptr->symbol_expr()); - - goto_programt::targett t=dest.add_instruction(DECL); - t->code=code_declt(symbol_ptr->symbol_expr()); - t->source_location=source_location; + code_declt decl; + decl.symbol()=symbol_ptr->symbol_expr(); + decl.add_source_location()=source_location; + convert_decl(decl, dest); return *symbol_ptr; } diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 098fd2ede5a..fe9115530f8 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -63,9 +63,6 @@ class goto_convertt:public message_streamt symbol_exprt make_compound_literal( const exprt &expr, goto_programt &dest); - - typedef std::list tmp_symbolst; - tmp_symbolst tmp_symbols; // // translation of C expressions (with side effects) @@ -87,8 +84,6 @@ class goto_convertt:public message_streamt exprt &expr, const std::string &suffix, goto_programt &); - - void kill_tmp_symbols(std::size_t, goto_programt &); void rewrite_boolean(exprt &dest); @@ -466,7 +461,6 @@ class goto_convertt:public message_streamt void do_printf (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); void do_input (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); void do_output (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); - void do_cover (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); void do_prob_coin (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); void do_prob_uniform (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest); diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 128c125b649..85d85ecc5d1 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -80,7 +80,8 @@ void goto_convert_functionst::goto_convert() it->second.type.id()==ID_code && (it->second.mode==ID_C || it->second.mode==ID_cpp || - it->second.mode==ID_java)) + it->second.mode==ID_java || + it->second.mode=="jsil")) symbol_list.push_back(it->first); } diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 1a0909bdc82..0d6da6daa09 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -417,8 +417,6 @@ void goto_convertt::remove_function_call( new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); - { code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -488,7 +486,11 @@ void goto_convertt::remove_cpp_new( new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); + + code_declt decl; + decl.symbol()=new_symbol.symbol_expr(); + decl.add_source_location()=new_symbol.location; + convert_decl(decl, dest); call=code_assignt(new_symbol.symbol_expr(), expr); @@ -560,7 +562,6 @@ void goto_convertt::remove_malloc( new_symbol.location=expr.source_location(); new_name(new_symbol); - tmp_symbols.push_back(new_symbol.symbol_expr()); code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -703,15 +704,9 @@ void goto_convertt::remove_statement_expression( id2string(last.get(ID_statement))+"'"; { - // this likely needs to be a proper stack - tmp_symbolst old_tmp_symbols; - old_tmp_symbols.swap(tmp_symbols); - goto_programt tmp; convert(code, tmp); dest.destructive_append(tmp); - - old_tmp_symbols.swap(tmp_symbols); } static_cast(expr)=tmp_symbol_expr; diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 1509ef146c2..85ccf4006de 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -414,7 +414,8 @@ void goto_inlinet::expand_function_call( identifier=="__CPROVER_set_must" || identifier=="__CPROVER_set_may" || identifier=="__CPROVER_clear_must" || - identifier=="__CPROVER_clear_may") + identifier=="__CPROVER_clear_may" || + identifier=="__CPROVER_cover") { target++; return; // ignore diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 74d1827b441..4abede465ae 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -281,11 +281,13 @@ Function: link_functions static bool link_functions( symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, - symbol_tablet &src_symbol_table, + const symbol_tablet &src_symbol_table, goto_functionst &src_functions, - const rename_symbolt &rename_symbol) + const rename_symbolt &rename_symbol, + const hash_set_cont &weak_symbols) { namespacet ns(dest_symbol_table); + namespacet src_ns(src_symbol_table); // merge functions Forall_goto_functions(src_it, src_functions) @@ -320,7 +322,8 @@ static bool link_functions( goto_functionst::goto_functiont &src_func=src_it->second; - if(in_dest_symbol_table.body.instructions.empty()) + if(in_dest_symbol_table.body.instructions.empty() || + weak_symbols.find(final_id)!=weak_symbols.end()) { // the one with body wins! rename_symbols_in_function(src_func, rename_symbol); @@ -328,7 +331,8 @@ static bool link_functions( in_dest_symbol_table.body.swap(src_func.body); in_dest_symbol_table.type=src_func.type; } - else if(src_func.body.instructions.empty()) + else if(src_func.body.instructions.empty() || + src_ns.lookup(src_it->first).is_weak) { // just keep the old one in dest } @@ -377,6 +381,12 @@ bool read_object_and_link( message_handler)) return true; + typedef hash_set_cont id_sett; + id_sett weak_symbols; + forall_symbols(it, symbol_table.symbols) + if(it->second.is_weak) + weak_symbols.insert(it->first); + linkingt linking(symbol_table, temp_model.symbol_table, message_handler); @@ -386,7 +396,7 @@ bool read_object_and_link( if(link_functions(symbol_table, functions, temp_model.symbol_table, temp_model.goto_functions, - linking.rename_symbol)) + linking.rename_symbol, weak_symbols)) return true; return false; diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 8ce2d378f2d..869a9193806 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include @@ -121,23 +122,30 @@ void goto_symext::parameter_assignments( f_parameter_type.id()==ID_unsignedbv || f_parameter_type.id()==ID_c_enum_tag || f_parameter_type.id()==ID_bool || - f_parameter_type.id()==ID_pointer) && + f_parameter_type.id()==ID_pointer || + f_parameter_type.id()==ID_union) && (f_rhs_type.id()==ID_signedbv || f_rhs_type.id()==ID_unsignedbv || f_rhs_type.id()==ID_c_bit_field || f_rhs_type.id()==ID_c_enum_tag || f_rhs_type.id()==ID_bool || - f_rhs_type.id()==ID_pointer)) + f_rhs_type.id()==ID_pointer || + f_rhs_type.id()==ID_union)) { - rhs.make_typecast(parameter_type); + rhs= + byte_extract_exprt( + byte_extract_id(), + rhs, + gen_zero(index_type()), + parameter_type); } else { - std::string error="function call: parameter \""+ - id2string(identifier)+"\" type mismatch: got "+ - rhs.type().to_string()+", expected "+ - parameter_type.to_string(); - throw error; + std::ostringstream error; + error << "function call: parameter \"" << identifier + << "\" type mismatch: got " << rhs.type().pretty() + << ", expected " << parameter_type.pretty(); + throw error.str(); } } @@ -493,9 +501,9 @@ void goto_symext::locality( while(state.l1_history.find(l1_name)!=state.l1_history.end()) { state.level1.increase_counter(l0_name); + ++offset; ssa.set_level_1(frame_nr+offset); l1_name=ssa.get_identifier(); - ++offset; } // now unique -- store diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 13499e87f8b..1169f0c8b4f 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -223,11 +223,13 @@ class symex_target_equationt:public symex_targett type(goto_trace_stept::NONE), hidden(false), guard(static_cast(get_nil_irep())), + guard_literal(const_literal(false)), ssa_lhs(static_cast(get_nil_irep())), ssa_full_lhs(static_cast(get_nil_irep())), original_full_lhs(static_cast(get_nil_irep())), ssa_rhs(static_cast(get_nil_irep())), cond_expr(static_cast(get_nil_irep())), + cond_literal(const_literal(false)), formatted(false), atomic_section_id(0), ignore(false) diff --git a/src/java_bytecode/java_bytecode_convert.cpp b/src/java_bytecode/java_bytecode_convert.cpp index 99eae9fd294..1debdd54e6e 100644 --- a/src/java_bytecode/java_bytecode_convert.cpp +++ b/src/java_bytecode/java_bytecode_convert.cpp @@ -599,6 +599,7 @@ codet java_bytecode_convertt::convert_instructions( instructionst::const_iterator source; std::list successors; + std::set predecessors; codet code; stackt stack; bool done; @@ -624,7 +625,8 @@ codet java_bytecode_convertt::convert_instructions( if(i_it->statement!="goto" && i_it->statement!="return" && - !(i_it->statement==patternt("?return"))) + !(i_it->statement==patternt("?return")) && + i_it->statement!="athrow") { instructionst::const_iterator next=i_it; if(++next!=instructions.end()) @@ -665,6 +667,20 @@ codet java_bytecode_convertt::convert_instructions( } } + for(address_mapt::iterator + it=address_map.begin(); + it!=address_map.end(); + ++it) + { + for(unsigned s : it->second.successors) + { + address_mapt::iterator a_it=address_map.find(s); + assert(a_it!=address_map.end()); + + a_it->second.predecessors.insert(it->first); + } + } + std::set working_set; if(!instructions.empty()) working_set.insert(instructions.front().address); @@ -685,6 +701,11 @@ codet java_bytecode_convertt::convert_instructions( a_it->second.stack.clear(); codet &c=a_it->second.code; + assert(stack.empty() || + a_it->second.predecessors.size()<=1 || + has_prefix(stack.front().get_string(ID_C_base_name), + "$stack")); + irep_idt statement=i_it->statement; exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt(); exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt(); @@ -1423,11 +1444,64 @@ codet java_bytecode_convertt::convert_instructions( address_mapt::iterator a_it2=address_map.find(*it); assert(a_it2!=address_map.end()); + if(!stack.empty() && a_it2->second.predecessors.size()>1) + { + // copy into temporaries + code_blockt more_code; + + // introduce temporaries when successor is seen for the first + // time + if(a_it2->second.stack.empty()) + { + for(stackt::iterator s_it=stack.begin(); + s_it!=stack.end(); + ++s_it) + { + symbol_exprt lhs=tmp_variable("$stack", s_it->type()); + code_assignt a(lhs, *s_it); + more_code.copy_to_operands(a); + + s_it->swap(lhs); + } + } + else + { + assert(a_it2->second.stack.size()==stack.size()); + stackt::const_iterator os_it=a_it2->second.stack.begin(); + for(stackt::iterator s_it=stack.begin(); + s_it!=stack.end(); + ++s_it) + { + assert(has_prefix(os_it->get_string(ID_C_base_name), + "$stack")); + symbol_exprt lhs=to_symbol_expr(*os_it); + code_assignt a(lhs, *s_it); + more_code.copy_to_operands(a); + + s_it->swap(lhs); + ++os_it; + } + } + + if(results.empty()) + { + more_code.copy_to_operands(c); + c.swap(more_code); + } + else + { + c.make_block(); + forall_operands(o_it, more_code) + c.copy_to_operands(*o_it); + } + } + a_it2->second.stack=stack; } } // TODO: add exception handlers from exception table + // review successor computation of athrow! code_blockt code; // temporaries diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index ecacf2ab751..1d76529be19 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -552,6 +552,7 @@ void java_bytecode_parsert::rconstant_pool() { symbol_typet string_type("java::java.lang.String"); exprt result(ID_java_string_literal, pointer_typet(string_type)); + result.set(ID_value, pool_entry(it->ref1).s); it->expr=result; } break; diff --git a/src/java_bytecode/java_bytecode_typecheck.h b/src/java_bytecode/java_bytecode_typecheck.h index b88d7d5f3e1..aae798ef280 100644 --- a/src/java_bytecode/java_bytecode_typecheck.h +++ b/src/java_bytecode/java_bytecode_typecheck.h @@ -27,13 +27,13 @@ bool java_bytecode_typecheck( message_handlert &message_handler, const namespacet &ns); -class java_bytecode_typecheckt:public legacy_typecheckt +class java_bytecode_typecheckt:public typecheckt { public: java_bytecode_typecheckt( symbol_tablet &_symbol_table, message_handlert &_message_handler): - legacy_typecheckt(_message_handler), + typecheckt(_message_handler), symbol_table(_symbol_table), ns(symbol_table) { diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index de42b23b2cc..e1e00ce817a 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -191,14 +191,9 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr) expr.struct_op()=m; } - #if 0 warning().source_location=expr.source_location(); warning() << "failed to find field `" << component_name << "` in class hierarchy" << eom; - #else - warning_msg("failed to find field `"+ - id2string(component_name)+"` in class hierarchy"); - #endif // We replace by a non-det of same type side_effect_expr_nondett nondet(expr.type()); diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 21676f3dd6f..ba471f009b4 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -16,6 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include +#include +#include +#include #include @@ -96,6 +102,191 @@ exprt gen_argument(const typet &type) /*******************************************************************\ +Function: gen_nondet_init + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +namespace { +void gen_nondet_init( + const exprt &expr, + code_blockt &init_code, + const namespacet &ns, + std::set &recursion_set, + bool is_sub, + irep_idt class_identifier) +{ + const typet &type=ns.follow(expr.type()); + + if(type.id()==ID_struct) + { + typedef struct_typet::componentt componentt; + typedef struct_typet::componentst componentst; + + const struct_typet &struct_type=to_struct_type(type); + const irep_idt struct_tag=struct_type.get_tag(); + + componentst components=struct_type.components(); + + if(!is_sub) + class_identifier=struct_tag; + + recursion_set.insert(struct_tag); + assert(!recursion_set.empty()); + + for(componentst::const_iterator it=components.begin(); + it!=components.end(); it++) + { + const componentt &component=*it; + const typet &component_type=component.type(); + irep_idt name=component.get_name(); + + member_exprt me(expr, name, component_type); + + if(name=="@class_identifier") + { + constant_exprt ci(class_identifier, string_typet()); + + code_assignt code(me, ci); + init_code.copy_to_operands(code); + } + else + { + irep_idt new_class_identifier; + assert(!name.empty()); + + is_sub = name[0]=='@'; + + gen_nondet_init( + me, init_code, ns, recursion_set, is_sub, class_identifier); + } + } + + recursion_set.erase(struct_tag); + } + else if(type.id()!=ID_pointer) + { + assert(type.id()!= ID_struct); + + side_effect_expr_nondett se=side_effect_expr_nondett(type); + + code_assignt code(expr, se); + init_code.copy_to_operands(code); + } + else + { + assert(type.id()==ID_pointer); + + // dereferenced type + const pointer_typet &pointer_type=to_pointer_type(type); + const typet &subtype=ns.follow(pointer_type.subtype()); + + if(subtype.id()==ID_struct) + { + const struct_typet &struct_type=to_struct_type(subtype); + const irep_idt struct_tag=struct_type.get_tag(); + + if(recursion_set.find(struct_tag)!=recursion_set.end()) + { + // make null + null_pointer_exprt null_pointer_expr(pointer_type); + code_assignt code(expr, null_pointer_expr); + init_code.copy_to_operands(code); + + return; + } + } + + // build size expression + exprt object_size=size_of_expr(subtype, ns); + + if(subtype.id()!=ID_empty && !object_size.is_nil()) + { + // malloc expression + side_effect_exprt malloc_expr(ID_malloc); + malloc_expr.copy_to_operands(object_size); + malloc_expr.type()=pointer_type; + + code_assignt code(expr, malloc_expr); + init_code.copy_to_operands(code); + + // dereference expression + dereference_exprt deref_expr(expr, subtype); + + gen_nondet_init(deref_expr, init_code, ns, recursion_set, false, ""); + } + else + { + // make null + null_pointer_exprt null_pointer_expr(pointer_type); + code_assignt code(expr, null_pointer_expr); + init_code.copy_to_operands(code); + } + } +} +} + +/*******************************************************************\ + +Function: gen_nondet_init + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +namespace { +void gen_nondet_init( + const exprt &expr, + code_blockt &init_code, + const namespacet &ns) +{ + std::set recursion_set; + gen_nondet_init(expr, init_code, ns, recursion_set, false, ""); +} +} + +/*******************************************************************\ + +Function: gen_nondet_init + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +namespace { +symbolt &new_tmp_symbol(symbol_tablet &symbol_table) +{ + static int temporary_counter=0; + + auxiliary_symbolt new_symbol; + symbolt *symbol_ptr; + + do + { + new_symbol.name="tmp_struct_init$"+i2string(++temporary_counter); + new_symbol.base_name=new_symbol.name; + new_symbol.mode=ID_java; + } while(symbol_table.move(new_symbol, symbol_ptr)); + + return *symbol_ptr; +} +} + +/*******************************************************************\ + Function: java_static_lifetime_init Inputs: @@ -176,54 +367,173 @@ bool java_entry_point( symbol_table.symbols.end()) return false; // silently ignore - // are we given a main class? - if(main_class.empty()) - return false; // silently ignore - - std::string entry_method= - id2string(main_class)+".main"; + messaget message(message_handler); - std::string prefix="java::"+entry_method+":"; + code_blockt struct_init_code; // struct init code if needed + bool have_struct=false; + symbol_exprt struct_ptr; - // look it up - std::set matches; + symbolt symbol; // main function symbol - for(symbol_tablet::symbolst::const_iterator - s_it=symbol_table.symbols.begin(); - s_it!=symbol_table.symbols.end(); - s_it++) + // find main symbol + if(config.main!="") { - if(s_it->second.type.id()==ID_code && - has_prefix(id2string(s_it->first), prefix)) - matches.insert(s_it->first); - } + // Add java:: prefix + std::string main_identifier="java::"+config.main; + + symbol_tablet::symbolst::const_iterator s_it; + + // Does it have a type signature? (':' suffix) + if(config.main.rfind(':')==std::string::npos) + { + std::string prefix=main_identifier+':'; + std::set matches; + + for(const auto & s : symbol_table.symbols) + if(has_prefix(id2string(s.first), prefix) && + s.second.type.id()==ID_code) + matches.insert(s.first); + + if(matches.empty()) + { + message.error() << "main symbol `" << config.main + << "' not found" << messaget::eom; + return true; + } + else if(matches.size()==1) + { + s_it=symbol_table.symbols.find(*matches.begin()); + assert(s_it!=symbol_table.symbols.end()); + } + else + { + message.error() << "main symbol `" << config.main + << "' is ambiguous:\n"; + + for(const auto & s : matches) + message.error() << " " << s << '\n'; + + message.error() << messaget::eom; + + return true; + } + } + else + { + // just look it up + s_it=symbol_table.symbols.find(main_identifier); + + if(s_it==symbol_table.symbols.end()) + { + message.error() << "main symbol `" << config.main + << "' not found" << messaget::eom; + return true; + } + } - if(matches.empty()) - { - // Not found, silently ignore - return false; - } + // function symbol + symbol=s_it->second; - if(matches.size()>=2) - { - messaget message(message_handler); - message.error() << "main method in `" << main_class - << "' is ambiguous" << messaget::eom; - return true; // give up with error, no main - } + if(symbol.type.id()!=ID_code) + { + message.error() << "main symbol `" << config.main + << "' not a function" << messaget::eom; + return true; + } + + // check if it has a body + if(symbol.value.is_nil()) + { + message.error() << "main method `" << main_class + << "' has no body" << messaget::eom; + return true; + } + + // get name of associated struct + size_t idx=config.main.rfind('.'); + assert(idx!=std::string::npos); + assert(idxsecond.type.id()==ID_struct) + { + const symbolt &struct_symbol=st_it->second; + assert(struct_symbol.type.id()==ID_struct); + const struct_typet &struct_type=to_struct_type(struct_symbol.type); + const pointer_typet pointer_type(struct_type); + + symbolt &aux_symbol=new_tmp_symbol(symbol_table); + aux_symbol.type=pointer_type; + aux_symbol.is_static_lifetime=true; + + struct_ptr=aux_symbol.symbol_expr(); - const symbolt &symbol= - symbol_table.symbols.find(*matches.begin())->second; + namespacet ns(symbol_table); + gen_nondet_init(struct_ptr, struct_init_code, ns); - // check if it has a body - if(symbol.value.is_nil()) + have_struct=true; + } + } + else { - messaget message(message_handler); - message.error() << "main method `" << main_class - << "' has no body" << messaget::eom; - return true; // give up with error + // no function given, we look for the main class + assert(config.main==""); + + // are we given a main class? + if(main_class.empty()) + return false; // silently ignore + + std::string entry_method= + id2string(main_class)+".main"; + + std::string prefix="java::"+entry_method+":"; + + // look it up + std::set matches; + + for(symbol_tablet::symbolst::const_iterator + s_it=symbol_table.symbols.begin(); + s_it!=symbol_table.symbols.end(); + s_it++) + { + if(s_it->second.type.id()==ID_code && + has_prefix(id2string(s_it->first), prefix)) + matches.insert(s_it->first); + } + + if(matches.empty()) + { + // Not found, silently ignore + return false; + } + + if(matches.size()>=2) + { + message.error() << "main method in `" << main_class + << "' is ambiguous" << messaget::eom; + return true; // give up with error, no main + } + + // function symbol + symbol=symbol_table.symbols.find(*matches.begin())->second; + + // check if it has a body + if(symbol.value.is_nil()) + { + message.error() << "main method `" << main_class + << "' has no body" << messaget::eom; + return true; // give up with error + } } + assert(!symbol.value.is_nil()); + assert(symbol.type.id()==ID_code); + create_initialize(symbol_table); if(java_static_lifetime_init(symbol_table, symbol.location, message_handler)) @@ -238,7 +548,6 @@ bool java_entry_point( if(init_it==symbol_table.symbols.end()) { - messaget message(message_handler); message.error() << "failed to find " INITIALIZE " symbol" << messaget::eom; return true; // give up with error @@ -246,12 +555,25 @@ bool java_entry_point( code_function_callt call_init; call_init.lhs().make_nil(); - call_init.add_source_location() = symbol.location; + call_init.add_source_location()=symbol.location; call_init.function()=init_it->second.symbol_expr(); init_code.move_to_operands(call_init); } + // add struct init code + + if(have_struct) + { + typedef code_blockt::operandst operandst; + const operandst &operands=struct_init_code.operands(); + + for(operandst::const_iterator it=operands.begin(); it!=operands.end(); it++) + { + init_code.add((const codet&)*it); + } + } + // build call to main method code_function_callt call_main; @@ -264,7 +586,15 @@ bool java_entry_point( exprt::operandst main_arguments; main_arguments.resize(parameters.size()); - for(unsigned i=0; i=1) + { + main_arguments[0]=struct_ptr; + i++; + } + + for(; i +#include "jsil_types.h" + #include "jsil_internal_additions.h" /*******************************************************************\ @@ -39,6 +41,8 @@ void jsil_internal_additions(symbol_tablet &dest) symbol.is_lvalue=true; symbol.is_state_var=true; symbol.is_thread_local=true; + // mark as already typechecked + symbol.is_extern=true; dest.add(symbol); } @@ -53,6 +57,8 @@ void jsil_internal_additions(symbol_tablet &dest) symbol.is_lvalue=true; symbol.is_state_var=true; symbol.is_thread_local=true; + // mark as already typechecked + symbol.is_extern=true; dest.add(symbol); } @@ -70,4 +76,58 @@ void jsil_internal_additions(symbol_tablet &dest) symbol.mode="jsil"; dest.add(symbol); } + + // add nan + + { + symbolt symbol; + symbol.base_name="nan"; + symbol.name="nan"; + symbol.type=floatbv_typet(); + symbol.mode="jsil"; + // mark as already typechecked + symbol.is_extern=true; + dest.add(symbol); + } + + // add empty symbol used for decl statemements + + { + symbolt symbol; + symbol.base_name="decl_symbol"; + symbol.name="decl_symbol"; + symbol.type=empty_typet(); + symbol.mode="jsil"; + // mark as already typechecked + symbol.is_extern=true; + dest.add(symbol); + } + + // add builtin objects + const std::vector builtin_objects= + { + "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString", + "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp", + "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror", + "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp", + "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp", + "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp", + "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp", + "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp", + "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson" + }; + + for(const auto &identifier : builtin_objects) + { + symbolt new_symbol; + new_symbol.name=identifier; + new_symbol.type=jsil_builtin_object_type(); + new_symbol.base_name=identifier; + new_symbol.mode="jsil"; + new_symbol.is_type=false; + new_symbol.is_lvalue=false; + // mark as already typechecked + new_symbol.is_extern=true; + dest.add(new_symbol); + } } diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 58a9b315ef1..0bcb5612bfd 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -51,7 +51,28 @@ Function: jsil_languaget::modules_provided void jsil_languaget::modules_provided(std::set &modules) { - modules.insert(get_base_name(parse_path)); + modules.insert(get_base_name(parse_path, true)); +} + +/*******************************************************************\ + +Function: jsil_languaget::interfaces + + Inputs: + + Outputs: + + Purpose: Adding symbols for all procedure declarations + +\*******************************************************************/ + +bool jsil_languaget::interfaces(symbol_tablet &symbol_table) +{ + if(jsil_convert(parse_tree, symbol_table, get_message_handler())) + return true; + + jsil_internal_additions(symbol_table); + return false; } /*******************************************************************\ @@ -120,7 +141,7 @@ Function: jsil_languaget::typecheck Outputs: - Purpose: + Purpose: Converting from parse tree and type checking. \*******************************************************************/ @@ -128,10 +149,6 @@ bool jsil_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { - if(jsil_convert(parse_tree, symbol_table, get_message_handler())) - return true; - - // now typecheck if(jsil_typecheck(symbol_table, get_message_handler())) return true; @@ -152,7 +169,6 @@ Function: jsil_languaget::final bool jsil_languaget::final(symbol_tablet &symbol_table) { - jsil_internal_additions(symbol_table); if(jsil_entry_point( symbol_table, diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 9604777a2c2..3b9f154fb4b 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -62,6 +62,7 @@ class jsil_languaget:public languaget virtual std::set extensions() const; virtual void modules_provided(std::set &modules); + virtual bool interfaces(symbol_tablet &symbol_table); protected: jsil_parse_treet parse_tree; diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp index 2f394e31abf..874e36ccef6 100644 --- a/src/jsil/jsil_parse_tree.cpp +++ b/src/jsil/jsil_parse_tree.cpp @@ -8,6 +8,8 @@ Author: Michael Tautschnig, tautschn@amazon.com #include +#include "jsil_types.h" + #include "jsil_parse_tree.h" /*******************************************************************\ @@ -66,10 +68,19 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const symbol_exprt s(to_symbol_expr( static_cast(find(ID_declarator)))); + code_typet symbol_type=to_code_type(s.type()); + + irep_idt proc_type=s.get("proc_type"); + + if(proc_type=="builtin") + symbol_type=jsil_builtin_code_typet(symbol_type); + else if(proc_type=="spec") + symbol_type=jsil_spec_code_typet(symbol_type); + symbol.name=s.get_identifier(); symbol.base_name=s.get_identifier(); symbol.mode="jsil"; - symbol.type=s.type(); + symbol.type=symbol_type; symbol.location=s.source_location(); code_blockt code(to_code_block( @@ -133,4 +144,3 @@ void jsil_parse_treet::output(std::ostream &out) const out << "\n"; } } - diff --git a/src/jsil/jsil_parse_tree.h b/src/jsil/jsil_parse_tree.h index 11ac901ab44..201ffb15542 100644 --- a/src/jsil/jsil_parse_tree.h +++ b/src/jsil/jsil_parse_tree.h @@ -29,6 +29,16 @@ class jsil_declarationt:public exprt add(ID_declarator, expr); } + const symbol_exprt &declarator() const + { + return static_cast(find(ID_declarator)); + } + + symbol_exprt &declarator() + { + return static_cast(add(ID_declarator)); + } + void add_returns( const irep_idt &value, const irep_idt &label) @@ -37,6 +47,16 @@ class jsil_declarationt:public exprt add(ID_return).set(ID_label, label); } + const irep_idt &returns_value() const + { + return find(ID_return).get(ID_value); + } + + const irep_idt &returns_label() const + { + return find(ID_return).get(ID_label); + } + void add_throws( const irep_idt &value, const irep_idt &label) @@ -45,11 +65,31 @@ class jsil_declarationt:public exprt add(ID_throw).set(ID_label, label); } + const irep_idt &throws_value() const + { + return find(ID_throw).get(ID_value); + } + + const irep_idt &throws_label() const + { + return find(ID_throw).get(ID_label); + } + void add_value(const code_blockt &code) { add(ID_value, code); } + const code_blockt &value() const + { + return static_cast(find(ID_value)); + } + + code_blockt &value() + { + return static_cast(add(ID_value)); + } + void to_symbol(symbolt &symbol) const; void output(std::ostream &) const; diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index f0a26a988ec..5f19edf5358 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -7,8 +7,11 @@ Author: Michael Tautschnig, tautschn@amazon.com \*******************************************************************/ #include +#include +#include #include "expr2jsil.h" +#include "jsil_types.h" #include "jsil_typecheck.h" @@ -48,7 +51,719 @@ std::string jsil_typecheckt::to_string(const typet &type) /*******************************************************************\ -Function: java_bytecode_typecheckt::typecheck_non_type_symbol +Function: jsil_typecheckt::add_prefix + + Inputs: + + Outputs: + + Purpose: Prefix parameters and variables with a procedure name + +\*******************************************************************/ + +irep_idt jsil_typecheckt::add_prefix(const irep_idt &ds) +{ + return id2string(proc_name) + "::" + id2string(ds); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::update_expr_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) +{ + expr.type()=type; + + if(expr.id()==ID_symbol) + { + const irep_idt &id=to_symbol_expr(expr).get_identifier(); + + if(!symbol_table.has_symbol(id)) + throw "Unexpected symbol: "+id2string(id); + + symbolt &s=symbol_table.lookup(id); + if(s.type.id().empty() || s.type.is_nil()) + s.type=type; + else + s.type=jsil_union(s.type, type); + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::make_type_compatible + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::make_type_compatible( + exprt &expr, + const typet &type, + bool must) +{ + if(type.id().empty() || type.is_nil()) + { + err_location(expr); + error() << "make_type_compatible got empty type: " << expr.pretty() << eom; + throw 0; + } + + if(expr.type().id().empty() || expr.type().is_nil()) + { + // Type is not yet set + update_expr_type(expr, type); + return; + } + + if(must) + { + if(jsil_incompatible_types(expr.type(), type)) + { + err_location(expr); + error() << "failed to typecheck expr " + << expr.pretty() << " with type " + << expr.type().pretty() + << "; required type " << type.pretty() << eom; + throw 0; + } + } + else if(!jsil_is_subtype(type, expr.type())) + { + // Types are not compatible + typet upper=jsil_union(expr.type(), type); + update_expr_type(expr, upper); + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_type(typet &type) +{ + if(type.id()==ID_code) + { + code_typet ¶meters=to_code_type(type); + + for(code_typet::parametert &p : parameters.parameters()) + { + // create new symbol + parameter_symbolt new_symbol; + new_symbol.base_name=p.get_identifier(); + + // append procedure name to parameters + p.set_identifier(add_prefix(p.get_identifier())); + new_symbol.name=p.get_identifier(); + + if(is_jsil_builtin_code_type(type)) + new_symbol.type=jsil_value_or_empty_type(); + else if(is_jsil_spec_code_type(type)) + new_symbol.type=jsil_value_or_reference_type(); + else + new_symbol.type=jsil_value_type(); // User defined function + + new_symbol.mode="jsil"; + + // mark as already typechecked + new_symbol.is_extern=true; + + if(symbol_table.add(new_symbol)) + { + error() << "failed to add parameter symbol `" + << new_symbol.name << "' in the symbol table" << eom; + throw 0; + } + } + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr(exprt &expr) +{ + // first do sub-nodes + typecheck_expr_operands(expr); + + // now do case-split + typecheck_expr_main(expr); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_expr_operands + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_operands(exprt &expr) +{ + Forall_operands(it, expr) + typecheck_expr(*it); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_expr_main + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_main(exprt &expr) +{ + if(expr.id()==ID_code) + { + err_location(expr); + error() << "typecheck_expr_main got code: " << expr.pretty() << eom; + throw 0; + } + else if(expr.id()==ID_symbol) + typecheck_symbol_expr(to_symbol_expr (expr)); + else if(expr.id()==ID_constant) + { + } + else + { + // expressions are expected not to have type set just yet + assert(expr.type().is_nil()||expr.type().id().empty()); + + if (expr.id()==ID_null || + expr.id()=="undefined" || + expr.id()==ID_empty) + typecheck_expr_constant(expr); + else if(expr.id()=="null_type" || + expr.id()=="undefined_type" || + expr.id()==ID_boolean || + expr.id()==ID_string || + expr.id()=="number" || + expr.id()=="builtin_object" || + expr.id()=="user_object" || + expr.id()=="object" || + expr.id()==ID_reference || + expr.id()==ID_member || + expr.id()=="variable") + expr.type()=jsil_kind(); + else if(expr.id()=="proto" || + expr.id()=="fid" || + expr.id()=="scope" || + expr.id()=="constructid" || + expr.id()=="primvalue" || + expr.id()=="targetfunction" || + expr.id()==ID_class) + { + // TODO: have a special type for builtin fields + expr.type()=string_typet(); + } + else if(expr.id()==ID_not) + typecheck_expr_unary_boolean(expr); + else if(expr.id()=="string_to_num") + typecheck_expr_unary_string(expr); + else if(expr.id()==ID_unary_minus || + expr.id()=="num_to_int32" || + expr.id()=="num_to_uint32" || + expr.id()==ID_bitnot) + { + typecheck_expr_unary_num(expr); + expr.type()=floatbv_typet(); + } + else if(expr.id()=="num_to_string") { + typecheck_expr_unary_num(expr); + expr.type()=string_typet(); + } + else if(expr.id()==ID_equal) + typecheck_exp_binary_equal(expr); + else if(expr.id()==ID_lt || + expr.id()==ID_le) + typecheck_expr_binary_compare(expr); + else if(expr.id()==ID_plus || + expr.id()==ID_minus || + expr.id()==ID_mult || + expr.id()==ID_div || + expr.id()==ID_mod || + expr.id()==ID_bitand || + expr.id()==ID_bitor || + expr.id()==ID_bitxor || + expr.id()==ID_shl || + expr.id()==ID_shr || + expr.id()==ID_lshr) + typecheck_expr_binary_arith(expr); + else if(expr.id()==ID_and || + expr.id()==ID_or) + typecheck_expr_binary_boolean(expr); + else if(expr.id()=="subtype_of") + typecheck_expr_subtype(expr); + else if(expr.id()==ID_concatenation) + typecheck_expr_concatenation(expr); + else if(expr.id()=="ref") + typecheck_expr_ref(expr); + else if(expr.id()=="field") + typecheck_expr_field(expr); + else if(expr.id()==ID_base) + typecheck_expr_base(expr); + else if(expr.id()==ID_typeof) + expr.type()=jsil_kind(); + else if(expr.id()=="new") + expr.type()=jsil_user_object_type(); + else if(expr.id()=="hasField") + typecheck_expr_has_field(expr); + else if(expr.id()==ID_index) + typecheck_expr_index(expr); + else if(expr.id()=="delete") + typecheck_expr_delete(expr); + else if(expr.id()=="protoField") + typecheck_expr_proto_field(expr); + else if(expr.id()=="protoObj") + typecheck_expr_proto_obj(expr); + else if(expr.id()==ID_side_effect) + typecheck_expr_side_effect_throw(to_side_effect_expr_throw(expr)); + else + { + err_location(expr); + error() << "unexpected expression: " << expr.pretty() << eom; + throw 0; + } + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_expr_side_effect_throw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_side_effect_throw( + side_effect_expr_throwt &expr) +{ + irept &excep_list=expr.add(ID_exception_list); + assert(excep_list.id()==ID_symbol); + symbol_exprt &s=static_cast(excep_list); + typecheck_symbol_expr(s); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_expr_constant + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_constant(exprt &expr) +{ + if(expr.id()==ID_null) + expr.type()=jsil_null_type(); + else if(expr.id()=="undefined") + expr.type()=jsil_undefined_type(); + else if(expr.id()==ID_empty) + expr.type()=jsil_empty_type(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_proto_field + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_proto_field(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_object_type(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + expr.type()=jsil_value_or_empty_type(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_proto_field + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_proto_obj(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands"; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_object_type(), true); + make_type_compatible(expr.op1(), jsil_object_type(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_delete + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_delete(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_object_type(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_hasfield + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_index(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_object_type(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + // special case for function identifiers + if (expr.op1().id()=="fid" || expr.op1().id()=="constructid") + expr.type()=code_typet(); + else + expr.type()=jsil_value_type(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_hasfield + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_has_field(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_object_type(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_field + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_field(exprt &expr) +{ + if(expr.operands().size()!=1) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects single operand" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_reference_type(), true); + + expr.type()=string_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_base + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_base(exprt &expr) +{ + if(expr.operands().size()!=1) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects single operand" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_reference_type(), true); + + expr.type()=jsil_value_type(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_ref + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_ref(exprt &expr) +{ + if(expr.operands().size()!=3) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects three operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_value_type(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + exprt &operand3=expr.op2(); + make_type_compatible(operand3, jsil_kind(), true); + + if(operand3.id()==ID_member) + expr.type()=jsil_member_reference_type(); + else if(operand3.id()=="variable") + expr.type()=jsil_variable_reference_type(); + else + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects reference type in the third parameter. Got:" + << operand3.pretty() << eom; + throw 0; + } +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_concatenation + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_concatenation(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), string_typet(), true); + make_type_compatible(expr.op1(), string_typet(), true); + + expr.type()=string_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_subtype + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_subtype(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), jsil_kind(), true); + make_type_compatible(expr.op1(), jsil_kind(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_binary_boolean + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_binary_boolean(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), bool_typet(), true); + make_type_compatible(expr.op1(), bool_typet(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_binary_arith + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_binary_arith(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + + make_type_compatible(expr.op0(), floatbv_typet(), true); + make_type_compatible(expr.op1(), floatbv_typet(), true); + + expr.type()=floatbv_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_exp_binary_equal Inputs: @@ -58,11 +773,520 @@ Function: java_bytecode_typecheckt::typecheck_non_type_symbol \*******************************************************************/ +void jsil_typecheckt::typecheck_exp_binary_equal(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + // operands can be of any types + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_binary_compare + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_binary_compare(exprt &expr) +{ + if(expr.operands().size()!=2) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects two operands" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), floatbv_typet(), true); + make_type_compatible(expr.op1(), floatbv_typet(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_unary_boolean + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_unary_boolean(exprt &expr) +{ + if(expr.operands().size()!=1) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects one operand" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), bool_typet(), true); + + expr.type()=bool_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_unary_string + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_unary_string(exprt &expr) +{ + if(expr.operands().size()!=1) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects one operand" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), string_typet(), true); + + expr.type()=floatbv_typet(); +} + +/*******************************************************************\ + +Function: jsil_typecheck_baset::typecheck_expr_unary_num + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_expr_unary_num(exprt &expr) +{ + if(expr.operands().size()!=1) + { + err_location(expr); + error() << "operator `" << expr.id() + << "' expects one operand" << eom; + throw 0; + } + + make_type_compatible(expr.op0(), floatbv_typet(), true); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_symbol_expr + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr) +{ + irep_idt identifier=symbol_expr.get_identifier(); + + // if this is a built-in identifier, check if it exists in the + // symbol table and retrieve it's type + // TODO: add a flag for not needing to prefix internal symbols + // that do not start with hash + if(has_prefix(id2string(identifier), "#") || + identifier=="eval" || + identifier=="nan") + { + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); + + if(s_it==symbol_table.symbols.end()) + throw "unexpected internal symbol: "+id2string(identifier); + else + { + // symbol already exists + const symbolt &symbol=s_it->second; + + // type the expression + symbol_expr.type()=symbol.type; + } + } + else + { + // if this is a variable, we need to check if we already + // prefixed it and add to the symbol table if it is not there already + irep_idt identifier_base = identifier; + if(!has_prefix(id2string(identifier), id2string(proc_name))) + { + identifier = add_prefix(identifier); + symbol_expr.set_identifier(identifier); + } + + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(identifier); + + if(s_it==symbol_table.symbols.end()) + { + // create new symbol + symbolt new_symbol; + new_symbol.name=identifier; + new_symbol.type=symbol_expr.type(); + new_symbol.base_name=identifier_base; + new_symbol.mode="jsil"; + new_symbol.is_type=false; + new_symbol.is_lvalue=new_symbol.type.id()!=ID_code; + + // mark as already typechecked + new_symbol.is_extern=true; + + if(symbol_table.add(new_symbol)) + { + error() << "failed to add symbol `" + << new_symbol.name << "' in the symbol table" + << eom; + throw 0; + } + } + else + { + // symbol already exists + assert(!s_it->second.is_type); + + const symbolt &symbol=s_it->second; + + // type the expression + symbol_expr.type()=symbol.type; + } + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_code + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_code(codet &code) +{ + const irep_idt &statement=code.get_statement(); + + if(statement==ID_function_call) + typecheck_function_call(to_code_function_call(code)); + else if(statement==ID_return) + typecheck_return(to_code_return(code)); + else if(statement==ID_expression) + { + if(code.operands().size()!=1) + throw "expression statement expected to have one operand"; + + typecheck_expr(code.op0()); + } + else if(statement==ID_label) + { + typecheck_code(to_code_label(code).code()); + // TODO: produce defined label set + } + else if(statement==ID_block) + typecheck_block(code); + else if(statement==ID_ifthenelse) + typecheck_ifthenelse(to_code_ifthenelse(code)); + else if(statement==ID_goto) + { + // TODO: produce used label set + } + else if(statement==ID_assign) + typecheck_assign(to_code_assign(code)); + else if(statement==ID_try_catch) + typecheck_try_catch(to_code_try_catch(code)); + else if(statement==ID_skip) + { + } + else + { + err_location(code); + error() << "unexpected statement: " << statement << eom; + throw 0; + } +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_return + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_return(code_returnt &code) +{ + if(code.has_return_value()) + typecheck_expr(code.return_value()); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_block + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_block(codet &code) +{ + Forall_operands(it, code) + typecheck_code(to_code(*it)); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_try_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_try_catch(code_try_catcht &code) +{ + // A special case of try catch with one catch clause + if(code.operands().size()!=3) + throw "try_catch expected to have three operands"; + + // function call + typecheck_function_call(to_code_function_call(code.try_code())); + + // catch decl is not used, but is required by goto-programs + + typecheck_code(code.get_catch_code(0)); +} + +/*******************************************************************\ + +Function: jsil_typecheckt::typecheck_function_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void jsil_typecheckt::typecheck_function_call( + code_function_callt &call) +{ + if(call.operands().size()!=3) + throw "function call expected to have three operands"; + + exprt &lhs=call.lhs(); + typecheck_expr(lhs); + + exprt &f=call.function(); + typecheck_expr(f); + + for(auto &arg : call.arguments()) + typecheck_expr(arg); + + // Look for a function declaration symbol in the symbol table + if(f.id()==ID_symbol) + { + const irep_idt &id=to_symbol_expr(f).get_identifier(); + + if(symbol_table.has_symbol(id)) + { + symbolt &s=symbol_table.lookup(id); + + if(s.type.id()==ID_code) + { + code_typet &codet=to_code_type(s.type); + + for (int i=0; i=call.arguments().size()) break; + + const typet ¶m_type=codet.parameters()[i].type(); + + if(!param_type.id().empty() && param_type.is_not_nil()) + { + // check argument's type if parameter's type is given + make_type_compatible(call.arguments()[i], param_type, true); + } + } + + // if there are too few arguments, add undefined + if(codet.parameters().size()>call.arguments().size()) + { + for(int i=call.arguments().size(); + i #include +#include + class codet; @@ -23,37 +25,65 @@ bool jsil_typecheck( message_handlert &message_handler, const namespacet &ns); -class jsil_typecheckt:public legacy_typecheckt +class jsil_typecheckt:public typecheckt { public: jsil_typecheckt( symbol_tablet &_symbol_table, message_handlert &_message_handler): - legacy_typecheckt(_message_handler), + typecheckt(_message_handler), symbol_table(_symbol_table), - ns(symbol_table) + ns(symbol_table), + proc_name() { } virtual ~jsil_typecheckt() { } virtual void typecheck(); - virtual void typecheck_expr(exprt &expr) {}; + virtual void typecheck_expr(exprt &expr); protected: symbol_tablet &symbol_table; const namespacet ns; + // prefix to variables which is set in typecheck_declaration + irep_idt proc_name; + void update_expr_type (exprt &expr, const typet &type); + void make_type_compatible(exprt &expr, const typet &type, bool must); void typecheck_type_symbol(symbolt &symbol) {}; void typecheck_non_type_symbol(symbolt &symbol); + void typecheck_symbol_expr(symbol_exprt &symbol_expr); + void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr); + void typecheck_expr_delete(exprt &expr); + void typecheck_expr_index(exprt &expr); + void typecheck_expr_proto_field(exprt &expr); + void typecheck_expr_proto_obj(exprt &expr); + void typecheck_expr_has_field(exprt &expr); + void typecheck_expr_ref(exprt &expr); + void typecheck_expr_field(exprt &expr); + void typecheck_expr_base(exprt &expr); + void typecheck_expr_constant(exprt &expr); + void typecheck_expr_concatenation(exprt &expr); + void typecheck_expr_subtype(exprt &expr); + void typecheck_expr_binary_boolean(exprt &expr); + void typecheck_expr_binary_arith(exprt &expr); + void typecheck_exp_binary_equal(exprt &expr); + void typecheck_expr_binary_compare(exprt &expr); + void typecheck_expr_unary_boolean(exprt &expr); + void typecheck_expr_unary_string(exprt &expr); + void typecheck_expr_unary_num(exprt &expr); + void typecheck_expr_operands(exprt &expr); + void typecheck_expr_main(exprt &expr); void typecheck_code(codet &code); - void typecheck_type(typet &type) {}; -#if 0 - void typecheck_expr_symbol(symbol_exprt &expr); - void typecheck_expr_member(member_exprt &expr); - void typecheck_expr_java_new(side_effect_exprt &expr); - void typecheck_expr_java_new_array(side_effect_exprt &expr); -#endif + void typecheck_function_call(code_function_callt &function_call); + void typecheck_return(code_returnt &code); + void typecheck_block(codet &code); + void typecheck_ifthenelse(code_ifthenelset &code); + void typecheck_assign(code_assignt &code); + void typecheck_try_catch (code_try_catcht &code); + void typecheck_type(typet &type); + irep_idt add_prefix(const irep_idt &ds); // overload to use language-specific syntax virtual std::string to_string(const exprt &expr); @@ -63,4 +93,3 @@ class jsil_typecheckt:public legacy_typecheckt }; #endif - diff --git a/src/jsil/jsil_types.cpp b/src/jsil/jsil_types.cpp new file mode 100644 index 00000000000..c9d96f4d64b --- /dev/null +++ b/src/jsil/jsil_types.cpp @@ -0,0 +1,526 @@ +/*******************************************************************\ + +Module: Jsil Language + +Author: Daiva Naudziuniene, daivan@amazon.com + +\*******************************************************************/ + +#include + +#include "jsil_types.h" + +/*******************************************************************\ + +Function: jsil_any_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_any_type() +{ + return jsil_union_typet({ + jsil_empty_type(), + jsil_reference_type(), + jsil_value_type() + }); +} + +/*******************************************************************\ + +Function: jsil_value_or_empty_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_value_or_empty_type() +{ + return jsil_union_typet({ + jsil_value_type(), + jsil_empty_type() + }); +} + +/*******************************************************************\ + +Function: jsil_value_or_reference_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_value_or_reference_type() +{ + return jsil_union_typet({ + jsil_value_type(), + jsil_reference_type() + }); +} + +/*******************************************************************\ + +Function: jsil_value_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_value_type() +{ + return jsil_union_typet({ + jsil_undefined_type(), + jsil_null_type(), + jsil_prim_type(), + jsil_object_type() + }); +} + +/*******************************************************************\ + +Function: jsil_prim_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_prim_type() +{ + return jsil_union_typet({ + floatbv_typet(), + string_typet(), + bool_typet() + }); +} + +/*******************************************************************\ + +Function: jsil_reference_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_reference_type() +{ + return jsil_union_typet({ + jsil_member_reference_type(), + jsil_variable_reference_type() + }); +} + +/*******************************************************************\ + +Function: jsil_member_reference_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_member_reference_type() +{ + return typet("jsil_member_reference_type"); +} + +/*******************************************************************\ + +Function: jsil_variable_reference_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_variable_reference_type() +{ + return typet("jsil_variable_reference_type"); +} + +/*******************************************************************\ + +Function: jsil_object_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_object_type() +{ + return jsil_union_typet({ + jsil_user_object_type(), + jsil_builtin_object_type() + }); +} + +/*******************************************************************\ + +Function: jsil_user_object_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_user_object_type() +{ + return typet("jsil_user_object_type"); +} + +/*******************************************************************\ + +Function: jsil_builtin_object_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_builtin_object_type() +{ + return typet("jsil_builtin_object_type"); +} + +/*******************************************************************\ + +Function: jsil_null_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_null_type() +{ + return typet("jsil_null_type"); +} + +/*******************************************************************\ + +Function: jsil_undefined_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_undefined_type() +{ + return typet("jsil_undefined_type"); +} + +/*******************************************************************\ + +Function: jsil_kind + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_kind() +{ + return typet("jsil_kind"); +} + +/*******************************************************************\ + +Function: jsil_empty_type + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_empty_type() +{ + return typet("jsil_empty_type"); +} + +/*******************************************************************\ + +Function: jsil_is_subtype + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool jsil_is_subtype(const typet &type1, const typet &type2) +{ + if(type2.id()==ID_union) + { + const jsil_union_typet &type2_union=to_jsil_union_type(type2); + + if(type1.id()==ID_union) + return to_jsil_union_type(type1).is_subtype(type2_union); + else + return jsil_union_typet(type1).is_subtype(type2_union); + } + else + return type1.id()==type2.id(); +} + +/*******************************************************************\ + +Function: jsil_incompatible_types + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool jsil_incompatible_types(const typet &type1, const typet &type2) +{ + return jsil_union_typet(type1).intersect_with( + jsil_union_typet(type2)).components().empty(); +} + +/*******************************************************************\ + +Function: jsil_union + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +typet jsil_union(const typet &type1, const typet &type2) +{ + return jsil_union_typet(type1) + .union_with(jsil_union_typet(type2)).to_type(); +} + +/*******************************************************************\ + +Function: compare_components + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool compare_components( + const union_typet::componentt &comp1, + const union_typet::componentt &comp2) +{ + return comp1.type().id() &types): + union_typet() +{ + auto &elements=components(); + for(const auto &type : types) + { + if(type.id()==ID_union) + { + for(const auto &component : to_union_type(type).components()) + elements.push_back(component); + } + else + elements.push_back(componentt(ID_anonymous, type)); + } + + std::sort(elements.begin(), elements.end(), compare_components); +} + +/*******************************************************************\ + +Function: jsil_union_typet::union_with + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +jsil_union_typet jsil_union_typet::union_with( + const jsil_union_typet &other) const +{ + auto &elements1=components(); + auto &elements2=other.components(); + jsil_union_typet result; + auto &elements=result.components(); + elements.resize(elements1.size()+elements2.size()); + std::vector::iterator it=std::set_union( + elements1.begin(), elements1.end(), + elements2.begin(), elements2.end(), + elements.begin(), compare_components); + elements.resize(it-elements.begin()); + + return result; +} + +/*******************************************************************\ + +Function: jsil_union_typet::intersect_with + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ +jsil_union_typet jsil_union_typet::intersect_with( + const jsil_union_typet &other) const +{ + auto &elements1=components(); + auto &elements2=other.components(); + jsil_union_typet result; + auto &elements=result.components(); + elements.resize(std::min(elements1.size(),elements2.size())); + std::vector::iterator it=std::set_intersection( + elements1.begin(), elements1.end(), + elements2.begin(), elements2.end(), + elements.begin(), compare_components); + elements.resize(it-elements.begin()); + + return result; +} + +/*******************************************************************\ + +Function: jsil_union_typet::is_subtype + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool jsil_union_typet::is_subtype(const jsil_union_typet &other) const +{ + auto it=components().begin(); + auto it2=other.components().begin(); + while(it=other.components().end()) + { + // We haven't found all types, but the second array finishes + return false; + } + + if(it->type().id()==it2->type().id()) + { + // Found the type + it++; + it2++; + } + else if(it->type().id()type().id()) + { + // Missing type + return false; + } + else // it->type().id()>it2->type().id() + { + // Skip one element in the second array + it2++; + } + } + + return true; +} + +/*******************************************************************\ + +Function: jsil_union_typet::to_type() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +const typet& jsil_union_typet::to_type() const +{ + auto &elements=components(); + if(elements.size()==1) + return elements[0].type(); + + return *this; +} diff --git a/src/jsil/jsil_types.h b/src/jsil/jsil_types.h new file mode 100644 index 00000000000..57950ef340e --- /dev/null +++ b/src/jsil/jsil_types.h @@ -0,0 +1,113 @@ +/*******************************************************************\ + +Module: Jsil Language + +Author: Daiva Naudziuniene, daivan@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_JSIL_TYPES_H +#define CPROVER_JSIL_TYPES_H + +#include +#include + +typet jsil_kind(); +typet jsil_any_type(); +typet jsil_value_or_empty_type(); +typet jsil_value_or_reference_type(); +typet jsil_value_type(); +typet jsil_prim_type(); +typet jsil_reference_type(); +typet jsil_member_reference_type(); +typet jsil_variable_reference_type(); +typet jsil_object_type(); +typet jsil_user_object_type(); +typet jsil_builtin_object_type(); +typet jsil_null_type(); +typet jsil_undefined_type(); +typet jsil_empty_type(); + +bool jsil_is_subtype(const typet &type1, const typet &type2); +bool jsil_incompatible_types(const typet &type1, const typet &type2); +typet jsil_union(const typet &type1, const typet &type2); + +class jsil_builtin_code_typet:public code_typet +{ +public: + explicit inline jsil_builtin_code_typet(code_typet &code): + code_typet(code) + { + set("jsil_builtin_proceduret", true); + } +}; + +extern inline jsil_builtin_code_typet &to_jsil_builtin_code_type( + code_typet &code) +{ + assert(code.get_bool("jsil_builtin_proceduret")); + return static_cast(code); +} + +extern inline bool is_jsil_builtin_code_type(const typet &type) +{ + return type.id()==ID_code && + type.get_bool("jsil_builtin_proceduret"); +} + +class jsil_spec_code_typet:public code_typet +{ +public: + explicit inline jsil_spec_code_typet(code_typet &code): + code_typet(code) + { + set("jsil_spec_proceduret", true); + } +}; + +extern inline jsil_spec_code_typet &to_jsil_spec_code_type( + code_typet &code) +{ + assert(code.get_bool("jsil_spec_proceduret")); + return static_cast(code); +} + +extern inline bool is_jsil_spec_code_type(const typet &type) +{ + return type.id()==ID_code && + type.get_bool("jsil_spec_proceduret"); +} + +class jsil_union_typet:public union_typet +{ +public: + inline jsil_union_typet():union_typet() { } + + explicit inline jsil_union_typet(const typet &type) + :jsil_union_typet(std::vector({type})) { } + + explicit jsil_union_typet(const std::vector &types); + + jsil_union_typet union_with(const jsil_union_typet &other) const; + + jsil_union_typet intersect_with(const jsil_union_typet &other) const; + + bool is_subtype(const jsil_union_typet &other) const; + + const typet& to_type() const; +}; + +extern inline jsil_union_typet &to_jsil_union_type(typet &type) +{ + assert(type.id()==ID_union); + return static_cast(type); +} + +extern inline const jsil_union_typet &to_jsil_union_type( + const typet &type) +{ + assert(type.id()==ID_union); + return static_cast(type); +} + +#endif diff --git a/src/jsil/parser.y b/src/jsil/parser.y index dd6c6901be8..9581c944e9d 100644 --- a/src/jsil/parser.y +++ b/src/jsil/parser.y @@ -153,7 +153,13 @@ proc_ident: TOK_IDENTIFIER newstack($$).swap(e); } | TOK_BUILTIN_IDENTIFIER + { + stack($$).set("proc_type", "builtin"); + } | TOK_SPEC_IDENTIFIER + { + stack($$).set("proc_type", "spec"); + } ; proc_ident_expr: proc_ident @@ -417,6 +423,11 @@ literal: TOK_IDENTIFIER } | TOK_FLOATING | TOK_STRING + { + constant_exprt c(to_string_constant(stack($$)) + .get_value(), string_typet()); + stack($$).swap(c); + } | TOK_BUILTIN_LOC | jsil_type | builtin_field @@ -518,11 +529,11 @@ bitwise_op: '&' } | '|' { - newstack($$).id(ID_or); + newstack($$).id(ID_bitor); } | '^' { - newstack($$).id(ID_xor); + newstack($$).id(ID_bitxor); } | TOK_LEFT_SHIFT { @@ -570,11 +581,11 @@ unary_op: TOK_NOT jsil_type: TOK_T_NULL { - newstack($$).id(ID_null); + newstack($$).id("null_type"); } | TOK_T_UNDEFINED { - newstack($$).id("undefined"); + newstack($$).id("undefined_type"); } | TOK_T_BOOLEAN { diff --git a/src/json/parser.y b/src/json/parser.y index e08345f40a9..1273c5cf087 100644 --- a/src/json/parser.y +++ b/src/json/parser.y @@ -58,11 +58,11 @@ int yyjsonerror(const std::string &error) %} -%token TOK_STRING -%token TOK_NUMBER -%token TOK_TRUE -%token TOK_FALSE -%token TOK_NULL +%token TOK_STRING +%token TOK_NUMBER +%token TOK_TRUE +%token TOK_FALSE +%token TOK_NULL %% diff --git a/src/json/scanner.l b/src/json/scanner.l index 45c7c7ca2f1..ee2435559e4 100644 --- a/src/json/scanner.l +++ b/src/json/scanner.l @@ -20,27 +20,27 @@ static int isatty(int) { return 0; } #include "json_y.tab.h" %} -string \"\"|\"{chars}\" -chars {char}+ -char [^\"]|\\\" - -number {int}|{int}{frac}|{int}{exp}|{int}{frac}{exp} -int {digit}|{digit19}{digits}|-{digit}|-{digit19}{digits} -frac "."{digits} -exp e{digits} -digits {digit}+ +string \"\"|\"{chars}\" +chars {char}+ +char [^\"]|\\\" + +number {int}|{int}{frac}|{int}{exp}|{int}{frac}{exp} +int {digit}|{digit19}{digits}|-{digit}|-{digit19}{digits} +frac "."{digits} +exp {e}{digits} +digits {digit}+ digit [0-9] digit19 [1-9] -e e|e\+|e-|E|E\+|E- +e e|e\+|e-|E|E\+|E- %% -{string} { return TOK_STRING; } -{number} { return TOK_NUMBER; } -"true" { return TOK_TRUE; } -"false" { return TOK_FALSE; } -"null" { return TOK_NULL; } +{string} { return TOK_STRING; } +{number} { return TOK_NUMBER; } +"true" { return TOK_TRUE; } +"false" { return TOK_FALSE; } +"null" { return TOK_NULL; } -[" "\r\n\t] { /* eat */ } -. { return yytext[0]; } +[" "\r\n\t] { /* eat */ } +. { return yytext[0]; } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 58a73fb6c91..76724e30856 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -176,8 +176,7 @@ void linkingt::detailed_conflict_report_rec( exprt &conflict_path) { #ifdef DEBUG - str << ""; - debug_msg(); + debug() << "" << eom; #endif std::string msg; @@ -217,6 +216,8 @@ void linkingt::detailed_conflict_report_rec( const struct_union_typet::componentst &components2= to_struct_union_type(t2).components(); + exprt conflict_path_before=conflict_path; + if(components1.size()!=components2.size()) { msg="number of members is different ("; @@ -238,11 +239,25 @@ void linkingt::detailed_conflict_report_rec( } else if(!base_type_eq(subtype1, subtype2, ns)) { + typedef hash_set_cont type_sett; + type_sett parent_types; + + exprt e=conflict_path_before; + while(e.id()==ID_dereference || + e.id()==ID_member || + e.id()==ID_index) + { + parent_types.insert(e.type()); + e=e.op0(); + } + + conflict_path=conflict_path_before; conflict_path.type()=t1; conflict_path= member_exprt(conflict_path, components1[i].get_name()); - if(depth>0) + if(depth>0 && + parent_types.find(t1)==parent_types.end()) detailed_conflict_report_rec( old_symbol, new_symbol, @@ -251,11 +266,29 @@ void linkingt::detailed_conflict_report_rec( depth-1, conflict_path); else + { msg="type of member "+ id2string(components1[i].get_name())+ " differs"; + if(depth>0) + { + std::string msg_bak; + msg_bak.swap(msg); + symbol_exprt c(ID_C_this); + detailed_conflict_report_rec( + old_symbol, + new_symbol, + subtype1, + subtype2, + depth-1, + c); + msg.swap(msg_bak); + } - break; + } + + if(parent_types.find(t1)==parent_types.end()) + break; } } } @@ -368,19 +401,18 @@ void linkingt::detailed_conflict_report_rec( if(!msg.empty()) { - str << std::endl; - str << "reason for conflict at " - << expr_to_string(ns, "", conflict_path) - << ": " << msg << std::endl; - - str << std::endl; - str << type_to_string_verbose(ns, old_symbol, t1) << std::endl; - str << type_to_string_verbose(ns, new_symbol, t2) << std::endl; + error() << '\n'; + error() << "reason for conflict at " + << expr_to_string(ns, "", conflict_path) + << ": " << msg << '\n'; + + error() << '\n'; + error() << type_to_string_verbose(ns, old_symbol, t1) << '\n'; + error() << type_to_string_verbose(ns, new_symbol, t2) << '\n'; } #ifdef DEBUG - str << ""; - debug_msg(); + debug() << "" << eom; #endif } @@ -401,17 +433,17 @@ void linkingt::link_error( const symbolt &new_symbol, const std::string &msg) { - err_location(new_symbol.location); - - str << "error: " << msg << " `" - << old_symbol.display_name() - << "'" << "\n"; - str << "old definition in module `" << old_symbol.module - << "' " << old_symbol.location << "\n" - << type_to_string_verbose(ns, old_symbol) << "\n"; - str << "new definition in module `" << new_symbol.module - << "' " << new_symbol.location << "\n" - << type_to_string_verbose(ns, new_symbol); + error().source_location=new_symbol.location; + + error() << "error: " << msg << " `" + << old_symbol.display_name() + << "'" << '\n'; + error() << "old definition in module `" << old_symbol.module + << "' " << old_symbol.location << '\n' + << type_to_string_verbose(ns, old_symbol) << '\n'; + error() << "new definition in module `" << new_symbol.module + << "' " << new_symbol.location << '\n' + << type_to_string_verbose(ns, new_symbol) << eom; throw 0; } @@ -433,17 +465,15 @@ void linkingt::link_warning( const symbolt &new_symbol, const std::string &msg) { - str << "warning: " << msg << " \"" - << old_symbol.display_name() - << "\"" << std::endl; - str << "old definition in module " << old_symbol.module - << " " << old_symbol.location << std::endl - << type_to_string_verbose(ns, old_symbol) << std::endl; - str << "new definition in module " << new_symbol.module - << " " << new_symbol.location << std::endl - << type_to_string_verbose(ns, new_symbol) << std::endl; - - warning_msg(); + warning() << "warning: " << msg << " \"" + << old_symbol.display_name() + << "\"" << '\n'; + warning() << "old definition in module " << old_symbol.module + << " " << old_symbol.location << '\n' + << type_to_string_verbose(ns, old_symbol) << '\n'; + warning() << "new definition in module " << new_symbol.module + << " " << new_symbol.location << '\n' + << type_to_string_verbose(ns, new_symbol) << eom; } /*******************************************************************\ @@ -542,6 +572,7 @@ void linkingt::duplicate_code_symbol( old_symbol.type=new_symbol.type; old_symbol.location=new_symbol.location; + old_symbol.is_weak=new_symbol.is_weak; } else if(!new_symbol.location.get_function().empty() && new_symbol.value.is_nil()) @@ -561,10 +592,64 @@ void linkingt::duplicate_code_symbol( { old_symbol.type=new_symbol.type; old_symbol.location=new_symbol.location; + old_symbol.is_weak=new_symbol.is_weak; + } + } + // replace weak symbols + else if(old_symbol.is_weak) + { + if(new_symbol.value.is_nil()) + link_warning( + old_symbol, + new_symbol, + "function declaration conflicts with with weak definition"); + else + old_symbol.value.make_nil(); + } + else if(new_symbol.is_weak) + { + if(new_symbol.value.is_nil() || + old_symbol.value.is_not_nil()) + { + new_symbol.value.make_nil(); + + link_warning( + old_symbol, + new_symbol, + "ignoring conflicting weak function declaration"); + } + } + // Linux kernel uses void f(void) as generic prototype + else if((old_t.return_type().id()==ID_empty && + old_t.parameters().empty() && + !old_t.has_ellipsis() && + old_symbol.value.is_nil()) || + (new_t.return_type().id()==ID_empty && + new_t.parameters().empty() && + !new_t.has_ellipsis() && + new_symbol.value.is_nil())) + { + // issue a warning + link_warning( + old_symbol, + new_symbol, + "ignoring conflicting void f(void) function declaration"); + + if(old_t.return_type().id()==ID_empty && + old_t.parameters().empty() && + !old_t.has_ellipsis() && + old_symbol.value.is_nil()) + { + old_symbol.type=new_symbol.type; + old_symbol.location=new_symbol.location; + old_symbol.is_weak=new_symbol.is_weak; } } // mismatch on number of parameters is definitively an error - else if(old_t.parameters().size()!=new_t.parameters().size()) + else if((old_t.parameters().size()new_t.parameters().size() && + !new_t.has_ellipsis())) { link_error( old_symbol, @@ -584,17 +669,28 @@ void linkingt::duplicate_code_symbol( conflicts.push_back( std::make_pair(old_t.return_type(), new_t.return_type())); - code_typet::parameterst::const_iterator n_it= - new_t.parameters().begin(); - for(code_typet::parameterst::const_iterator - o_it=old_t.parameters().begin(); - o_it!=old_t.parameters().end(); + code_typet::parameterst::const_iterator + n_it=new_t.parameters().begin(), + o_it=old_t.parameters().begin(); + for( ; + o_it!=old_t.parameters().end() && + n_it!=new_t.parameters().end(); ++o_it, ++n_it) { if(!base_type_eq(o_it->type(), n_it->type(), ns)) conflicts.push_back( std::make_pair(o_it->type(), n_it->type())); } + if(o_it!=old_t.parameters().end()) + { + assert(new_t.has_ellipsis()); + replace=new_symbol.value.is_not_nil(); + } + else if(n_it!=new_t.parameters().end()) + { + assert(old_t.has_ellipsis()); + replace=new_symbol.value.is_not_nil(); + } while(!conflicts.empty()) { @@ -635,12 +731,10 @@ void linkingt::duplicate_code_symbol( // _GNU_SOURCE consistent else if((t1.id()==ID_union && (t1.get_bool(ID_C_transparent_union) || - conflicts.front().first.get_bool(ID_C_transparent_union)) && - new_symbol.value.is_nil()) || + conflicts.front().first.get_bool(ID_C_transparent_union))) || (t2.id()==ID_union && (t2.get_bool(ID_C_transparent_union) || - conflicts.front().second.get_bool(ID_C_transparent_union)) && - old_symbol.value.is_nil())) + conflicts.front().second.get_bool(ID_C_transparent_union)))) { const bool use_old= t1.id()==ID_union && @@ -648,14 +742,14 @@ void linkingt::duplicate_code_symbol( conflicts.front().first.get_bool(ID_C_transparent_union)) && new_symbol.value.is_nil(); - const union_typet &dest_union_type= - to_union_type(use_old?t1:t2); - const typet &src_type=use_old?t2:t1; + const union_typet &union_type= + to_union_type(t1.id()==ID_union?t1:t2); + const typet &src_type=t1.id()==ID_union?t2:t1; bool found=false; for(union_typet::componentst::const_iterator - it=dest_union_type.components().begin(); - !found && it!=dest_union_type.components().end(); + it=union_type.components().begin(); + !found && it!=union_type.components().end(); it++) if(base_type_eq(it->type(), src_type, ns)) { @@ -710,6 +804,7 @@ void linkingt::duplicate_code_symbol( rename_symbol(new_symbol.type); old_symbol.value=new_symbol.value; old_symbol.type=new_symbol.type; // for parameter identifiers + old_symbol.is_weak=new_symbol.is_weak; } else if(to_code_type(old_symbol.type).get_inlined()) { @@ -718,10 +813,9 @@ void linkingt::duplicate_code_symbol( else if(base_type_eq(old_symbol.type, new_symbol.type, ns)) { // keep the one in old_symbol -- libraries come last! - str << "warning: function `" << old_symbol.name << "' in module `" << - new_symbol.module << "' is shadowed by a definition in module `" << - old_symbol.module << "'" << std::endl; - warning_msg(); + warning() << "function `" << old_symbol.name << "' in module `" + << new_symbol.module << "' is shadowed by a definition in module `" + << old_symbol.module << "'" << eom; } else link_error( @@ -833,12 +927,13 @@ void linkingt::duplicate_object_symbol( !new_symbol.value.get_bool(ID_C_zero_initializer)) { if(old_symbol.value.is_nil() || - old_symbol.value.get_bool(ID_C_zero_initializer)) + old_symbol.value.get_bool(ID_C_zero_initializer) || + old_symbol.is_weak) { // new_symbol wins old_symbol.value=new_symbol.value; } - else + else if(!new_symbol.is_weak) { // try simplifier exprt tmp_old=old_symbol.value, @@ -854,15 +949,15 @@ void linkingt::duplicate_object_symbol( else { err_location(new_symbol.value); - str << "error: conflicting initializers for variable \"" - << old_symbol.name - << "\"" << '\n'; - str << "old value in module " << old_symbol.module - << " " << old_symbol.value.find_source_location() << '\n' - << expr_to_string(ns, old_symbol.name, tmp_old) << '\n'; - str << "new value in module " << new_symbol.module - << " " << new_symbol.value.find_source_location() << '\n' - << expr_to_string(ns, new_symbol.name, tmp_new); + error() << "error: conflicting initializers for variable \"" + << old_symbol.name + << "\"" << '\n'; + error() << "old value in module " << old_symbol.module + << " " << old_symbol.value.find_source_location() << '\n' + << expr_to_string(ns, old_symbol.name, tmp_old) << '\n'; + error() << "new value in module " << new_symbol.module + << " " << new_symbol.value.find_source_location() << '\n' + << expr_to_string(ns, new_symbol.name, tmp_new) << eom; throw 0; } } @@ -1069,7 +1164,7 @@ Function: linkingt::do_type_dependencies void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) { - // Any type that uses a type that will be renamed also + // Any type that uses a symbol that will be renamed also // needs to be renamed, and so on, until saturation. used_byt used_by; @@ -1078,12 +1173,13 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) { if(s_it->second.is_type) { - find_symbols_sett type_symbols_used; - find_type_symbols(s_it->second.type, type_symbols_used); + // find type and array-size symbols + find_symbols_sett symbols_used; + find_type_and_expr_symbols(s_it->second.type, symbols_used); for(find_symbols_sett::const_iterator - it=type_symbols_used.begin(); - it!=type_symbols_used.end(); + it=symbols_used.begin(); + it!=symbols_used.end(); it++) { used_by[*it].insert(s_it->first); @@ -1114,8 +1210,8 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) { queue.push(*d_it); #ifdef DEBUG - str << "LINKING: needs to be renamed (dependency): " << *d_it; - debug_msg(); + debug() << "LINKING: needs to be renamed (dependency): " + << *d_it << eom; #endif } } @@ -1154,9 +1250,8 @@ void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) new_symbol.name=new_identifier; #ifdef DEBUG - str << "LINKING: renaming " << *it << " to " - << new_identifier; - debug_msg(); + debug() << "LINKING: renaming " << *it << " to " + << new_identifier << eom; #endif if(new_symbol.is_type) @@ -1263,8 +1358,8 @@ void linkingt::typecheck() { needs_to_be_renamed.insert(s_it->first); #ifdef DEBUG - str << "LINKING: needs to be renamed: " << s_it->first; - debug_msg(); + debug() << "LINKING: needs to be renamed: " + << s_it->first << eom; #endif } } diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index e15a33cb80e..40b6217102f 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -15,14 +15,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class linkingt:public legacy_typecheckt +class linkingt:public typecheckt { public: linkingt( symbol_tablet &_main_symbol_table, symbol_tablet &_src_symbol_table, message_handlert &_message_handler): - legacy_typecheckt(_message_handler), + typecheckt(_message_handler), main_symbol_table(_main_symbol_table), src_symbol_table(_src_symbol_table), ns(_main_symbol_table) diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 71c801254ce..cdb59b3baa9 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -132,6 +132,15 @@ void remove_internal_symbols( symbol.value.is_not_nil() && !symbol.value.get_bool(ID_C_zero_initializer); + // __attribute__((constructor)), __attribute__((destructor)) + if(symbol.mode==ID_C && is_function && is_file_local) + { + const code_typet &code_type=to_code_type(symbol.type); + if(code_type.return_type().id()==ID_constructor || + code_type.return_type().id()==ID_destructor) + is_file_local=false; + } + if(is_type) { // never EXPORTED by itself diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 6c909e19d11..096a4e7f749 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -160,8 +160,8 @@ bool static_lifetime_init( { const symbolt &symbol=ns.lookup(id); - if(symbol.type.get_bool("initialization") && - symbol.type.id()==ID_code) + if(symbol.type.id()==ID_code && + to_code_type(symbol.type).return_type().id()==ID_constructor) { code_function_callt function_call; function_call.function()=symbol.symbol_expr(); diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp index d3932cc0dab..a3504953030 100644 --- a/src/util/file_util.cpp +++ b/src/util/file_util.cpp @@ -115,3 +115,24 @@ void delete_directory(const std::string &path) rmdir(path.c_str()); } +/*******************************************************************\ + +Function: concat_dir_file + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::string concat_dir_file(const std::string &directory, + const std::string &file_name) +{ + #ifdef _WIN32 + return directory+"\\"+file_name; + #else + return directory+"/"+file_name; + #endif +} diff --git a/src/util/file_util.h b/src/util/file_util.h index b6db7ad4655..94939c9d6ec 100644 --- a/src/util/file_util.h +++ b/src/util/file_util.h @@ -15,4 +15,7 @@ void delete_directory(const std::string &path); std::string get_current_working_directory(); +std::string concat_dir_file(const std::string &directory, + const std::string &file_name); + #endif diff --git a/src/util/get_base_name.cpp b/src/util/get_base_name.cpp index 3e1bbdf6add..944603ce86d 100644 --- a/src/util/get_base_name.cpp +++ b/src/util/get_base_name.cpp @@ -22,9 +22,11 @@ Function: get_base_name \*******************************************************************/ -std::string get_base_name(const std::string &in) +std::string get_base_name(const std::string &in, bool strip_suffix) { - size_t r=in.rfind('.', in.length()-1); + size_t r=std::string::npos; + if(strip_suffix) + r=in.rfind('.', in.length()-1); if(r==std::string::npos) r=in.length(); size_t f=in.rfind('/', in.length()-1); diff --git a/src/util/get_base_name.h b/src/util/get_base_name.h index c38500a1c54..cabf7741a4f 100644 --- a/src/util/get_base_name.h +++ b/src/util/get_base_name.h @@ -10,4 +10,4 @@ Author: CM Wintersteiger #include -std::string get_base_name(const std::string &in); +std::string get_base_name(const std::string &in, bool strip_suffix); diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 452b12ba4aa..86a5d39d08b 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -724,3 +724,4 @@ C_spec_requires #spec_requires C_spec_ensures #spec_ensures virtual_function C_element_type #element_type +working_directory diff --git a/src/util/parser.h b/src/util/parser.h index 8cd510bbd52..dd672e81b1a 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -7,6 +7,7 @@ #include "expr.h" #include "message.h" +#include "file_util.h" class parsert:public messaget { @@ -75,6 +76,8 @@ class parsert:public messaget inline void set_file(const irep_idt &file) { source_location.set_file(file); + source_location.set_working_directory( + get_current_working_directory()); } inline irep_idt get_file() const diff --git a/src/util/source_location.h b/src/util/source_location.h index 46b01ed0ea4..7be5aaa9f29 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -25,6 +25,11 @@ class source_locationt:public irept return get(ID_file); } + inline const irep_idt &get_working_directory() const + { + return get(ID_working_directory); + } + inline const irep_idt &get_line() const { return get(ID_line); @@ -60,6 +65,11 @@ class source_locationt:public irept set(ID_file, file); } + inline void set_working_directory(const irep_idt &cwd) + { + set(ID_working_directory, cwd); + } + inline void set_line(const irep_idt &line) { set(ID_line, line); diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 42fb6f13201..25fbc97ad0f 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -125,20 +125,15 @@ static void build_object_descriptor_rec( { const member_exprt &member=to_member_expr(expr); const exprt &struct_op=member.struct_op(); - const typet &struct_type=ns.follow(struct_op.type()); build_object_descriptor_rec(ns, struct_op, dest); - if(struct_type.id()==ID_union) - return; - - mp_integer offset= - member_offset(to_struct_type(struct_type), - member.get_component_name(), ns); - assert(offset>=0); + exprt offset=member_offset_expr(member, ns); + assert(offset.is_not_nil()); dest.offset()= - plus_exprt(dest.offset(), from_integer(offset, index_type)); + plus_exprt(dest.offset(), + typecast_exprt(offset, index_type)); } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) @@ -154,6 +149,14 @@ static void build_object_descriptor_rec( typecast_exprt(to_byte_extract_expr(expr).offset(), index_type)); } + else if(expr.id()==ID_typecast) + { + const typecast_exprt &tc=to_typecast_expr(expr); + + dest.object()=tc.op(); + + build_object_descriptor_rec(ns, tc.op(), dest); + } } /*******************************************************************\ diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 288bc23f11e..6f9f665326c 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1720,7 +1720,7 @@ class and_exprt:public exprt * 3) returns true otherwise */ -exprt conjunction(const exprt::operandst &op); +exprt conjunction(const exprt::operandst &); /*! \brief Cast a generic exprt to a \ref and_exprt * @@ -1822,7 +1822,7 @@ class or_exprt:public exprt * 3) returns false otherwise */ -exprt disjunction(const exprt::operandst &op); +exprt disjunction(const exprt::operandst &); /*! \brief Cast a generic exprt to a \ref or_exprt * diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp index 6a310a39b52..625a7801e2c 100644 --- a/src/util/tempdir.cpp +++ b/src/util/tempdir.cpp @@ -116,11 +116,7 @@ Function: temp_dirt::operator() std::string temp_dirt::operator()(const std::string &file) { - #ifdef _WIN32 - return path+"\\"+file; - #else - return path+"/"+file; - #endif + return concat_dir_file(path, file); } /*******************************************************************\ diff --git a/src/util/typecheck.h b/src/util/typecheck.h index 5823c0b2e34..c300bea81ca 100644 --- a/src/util/typecheck.h +++ b/src/util/typecheck.h @@ -44,7 +44,18 @@ class typecheckt:public messaget return messaget::error(); } + // not pretty, but makes transition easier + inline void err_location(const exprt &src) + { + error().source_location=src.find_source_location(); + } + bool error_found; + + inline bool get_error_found() const + { + return error_found; + } protected: // main function -- overload this one diff --git a/src/xmllang/parser.y b/src/xmllang/parser.y index 5bfd4a2ef3d..727c4c947db 100644 --- a/src/xmllang/parser.y +++ b/src/xmllang/parser.y @@ -48,7 +48,7 @@ misc_seq_opt ; misc - : COMMENT { free($1); } + : COMMENT { free($1); } | PI ; @@ -58,24 +58,24 @@ PI attribute_seq_opt { xml_parser.stack.pop_back(); } ENDPI - ; + ; element - : START { xml_parser.current().name=$1; + : START { xml_parser.current().name=$1; free($1); - } + } attribute_seq_opt empty_or_content ; empty_or_content - : SLASH CLOSE { } - | CLOSE { } - content END name_opt CLOSE { free($5); } + : SLASH CLOSE { } + | CLOSE { } + content END name_opt CLOSE { free($5); } ; content - : content DATA { xml_parser.current().data+=xmlt::unescape($2); free($2); } + : content DATA { xml_parser.current().data+=xmlt::unescape($2); free($2); } | content misc | content { xml_parser.new_level(); } @@ -85,8 +85,8 @@ content ; name_opt - : NAME { $$=$1; } - | /*empty*/ { $$=strdup(""); } + : NAME { $$=$1; } + | /*empty*/ { $$=strdup(""); } ; attribute_seq_opt @@ -95,7 +95,7 @@ attribute_seq_opt ; attribute - : NAME EQ VALUE { xml_parser.current().set_attribute( + : NAME EQ VALUE { xml_parser.current().set_attribute( xmlt::unescape($1), xmlt::unescape($3)); free($1); free($3);} ; diff --git a/src/xmllang/scanner.l b/src/xmllang/scanner.l index 281aaecab01..9db5f50c243 100644 --- a/src/xmllang/scanner.l +++ b/src/xmllang/scanner.l @@ -17,7 +17,7 @@ static int isatty(int) { return 0; } #define PARSER xml_parser -//static int keep; /* To store start condition */ +//static int keep; /* To store start condition */ static char *word(char *s) { @@ -34,17 +34,17 @@ static char *word(char *s) %} -nl (\r\n|\r|\n) -ws [ \t\r\n]+ -open {nl}?"<" -close ">"{nl}? -namestart [A-Za-z\200-\377_] -namechar [A-Za-z\200-\377_0-9.:-] -esc "&#"[0-9]+";"|"&#x"[0-9a-fA-F]+";"|"&"[a-zA-Z]+";" -name {namestart}{namechar}* -data ([^<\n&]|\n[^<&]|\n{esc}|{esc})+ -comment {open}"!--"([^-]|"-"[^-])*"--"{close} -string \"([^"&]|{esc})*\"|\'([^'&]|{esc})*\' +nl (\r\n|\r|\n) +ws [ \t\r\n]+ +open {nl}?"<" +close ">"{nl}? +namestart [A-Za-z\200-\377_] +namechar [A-Za-z\200-\377_0-9.:-] +esc "&#"[0-9]+";"|"&#x"[0-9a-fA-F]+";"|"&"[a-zA-Z]+";" +name {namestart}{namechar}* +data ([^<\n&]|\n[^<&]|\n{esc}|{esc})+ +comment {open}"!--"([^-]|"-"[^-])*"--"{close} +string \"([^"&]|{esc})*\"|\'([^'&]|{esc})*\' /* * The CONTENT mode is used for the content of elements, i.e., @@ -59,28 +59,28 @@ string \"([^"&]|{esc})*\"|\'([^'&]|{esc})*\' %% -{ws} {/* skip */} -"/" {return SLASH;} -"=" {return EQ;} -{close} {BEGIN(CONTENT); return CLOSE;} -{name} {yyxmllval.s=strdup(yytext); return NAME;} -{string} {yyxmllval.s=strdup(yytext); return VALUE;} -"?"{close} {BEGIN(INITIAL); return ENDPI;} +{ws} {/* skip */} +"/" {return SLASH;} +"=" {return EQ;} +{close} {BEGIN(CONTENT); return CLOSE;} +{name} {yyxmllval.s=strdup(yytext); return NAME;} +{string} {yyxmllval.s=strdup(yytext); return VALUE;} +"?"{close} {BEGIN(INITIAL); return ENDPI;} -{open}{ws}?{name} {BEGIN(INITIAL); yyxmllval.s=word(yytext); return START;} -{open}{ws}?"/" {BEGIN(INITIAL); return END;} -{open}"?xml" {BEGIN(INITIAL); return STARTXMLDECL;} -{open}"?" {BEGIN(PI); yyxmllval.s=word(yytext); return STARTPI;} -{comment} {yyxmllval.s=strdup(yytext); return COMMENT;} +{open}{ws}?{name} {BEGIN(INITIAL); yyxmllval.s=word(yytext); return START;} +{open}{ws}?"/" {BEGIN(INITIAL); return END;} +{open}"?xml" {BEGIN(INITIAL); return STARTXMLDECL;} +{open}"?" {BEGIN(PI); yyxmllval.s=word(yytext); return STARTPI;} +{comment} {yyxmllval.s=strdup(yytext); return COMMENT;} -{data} {yyxmllval.s=strdup(yytext); return DATA;} +{data} {yyxmllval.s=strdup(yytext); return DATA;} {open}"!"{ws}?"DOCTYPE" {BEGIN(DTD); /* skip */} -. {/* skip */} +. {/* skip */} \]{close} {BEGIN(INITIAL); /* skip */} -. { yyxmlerror("unexpected character"); } -{nl} {/* skip, must be an extra one at EOF */;} +. { yyxmlerror("unexpected character"); } +{nl} {/* skip, must be an extra one at EOF */;} %%