From 596ffad8ddbb3e7b4ed4a3fd3fc63724a58e9371 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 1 May 2019 10:39:28 -0700 Subject: [PATCH] [demo] add more examples Summary: some examples of bugs infer finds Reviewed By: jeremydubreil Differential Revision: D15081483 fbshipit-source-id: 4e40c7384 --- examples/demo/00/Makefile | 15 ++++++++++ examples/demo/00/simple_null.cpp | 10 +++++++ examples/demo/01/Makefile | 15 ++++++++++ examples/demo/01/simple_null_interproc.c | 15 ++++++++++ .../demo/01/simple_null_interproc_fixed.c | 19 ++++++++++++ examples/demo/01/wrappers.c | 11 +++++++ examples/demo/02/Makefile | 15 ++++++++++ examples/demo/02/Resources.java | 26 ++++++++++++++++ examples/demo/02/ResourcesFixed.java | 20 +++++++++++++ examples/demo/03.fixed/Account.java | 12 ++++++++ .../demo/03.fixed/AccountImplementation.java | 30 +++++++++++++++++++ examples/demo/03.fixed/Client.java | 19 ++++++++++++ examples/demo/03.fixed/Makefile | 15 ++++++++++ examples/demo/03.fixed/ThreadSafe.java | 7 +++++ examples/demo/03/Account.java | 10 +++++++ examples/demo/03/AccountImplementation.java | 30 +++++++++++++++++++ examples/demo/03/Client.java | 19 ++++++++++++ examples/demo/03/Makefile | 15 ++++++++++ examples/demo/03/ThreadSafe.java | 7 +++++ examples/demo/04.fixed/Client.java | 15 ++++++++++ examples/demo/04.fixed/Library.java | 21 +++++++++++++ examples/demo/04.fixed/Makefile | 15 ++++++++++ examples/demo/04.fixed/Nullable.java | 8 +++++ examples/demo/04/Client.java | 14 +++++++++ examples/demo/04/Library.java | 21 +++++++++++++ examples/demo/04/Makefile | 15 ++++++++++ examples/demo/04/Nullable.java | 8 +++++ examples/demo/Makefile | 14 +++++++++ examples/demo/demo.sh | 16 ++++++++++ 29 files changed, 457 insertions(+) create mode 100644 examples/demo/00/Makefile create mode 100644 examples/demo/00/simple_null.cpp create mode 100644 examples/demo/01/Makefile create mode 100644 examples/demo/01/simple_null_interproc.c create mode 100644 examples/demo/01/simple_null_interproc_fixed.c create mode 100644 examples/demo/01/wrappers.c create mode 100644 examples/demo/02/Makefile create mode 100644 examples/demo/02/Resources.java create mode 100644 examples/demo/02/ResourcesFixed.java create mode 100644 examples/demo/03.fixed/Account.java create mode 100644 examples/demo/03.fixed/AccountImplementation.java create mode 100644 examples/demo/03.fixed/Client.java create mode 100644 examples/demo/03.fixed/Makefile create mode 100644 examples/demo/03.fixed/ThreadSafe.java create mode 100644 examples/demo/03/Account.java create mode 100644 examples/demo/03/AccountImplementation.java create mode 100644 examples/demo/03/Client.java create mode 100644 examples/demo/03/Makefile create mode 100644 examples/demo/03/ThreadSafe.java create mode 100644 examples/demo/04.fixed/Client.java create mode 100644 examples/demo/04.fixed/Library.java create mode 100644 examples/demo/04.fixed/Makefile create mode 100644 examples/demo/04.fixed/Nullable.java create mode 100644 examples/demo/04/Client.java create mode 100644 examples/demo/04/Library.java create mode 100644 examples/demo/04/Makefile create mode 100644 examples/demo/04/Nullable.java create mode 100644 examples/demo/Makefile create mode 100755 examples/demo/demo.sh diff --git a/examples/demo/00/Makefile b/examples/demo/00/Makefile new file mode 100644 index 000000000..d4c1a43ea --- /dev/null +++ b/examples/demo/00/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = simple_null.cpp +OBJECTS = $(SOURCES:.cpp=.o) + +all: $(OBJECTS) + +.cpp.o: + ${CC} -c $< + +clean: + rm -rf $(OBJECTS) diff --git a/examples/demo/00/simple_null.cpp b/examples/demo/00/simple_null.cpp new file mode 100644 index 000000000..a95420c1c --- /dev/null +++ b/examples/demo/00/simple_null.cpp @@ -0,0 +1,10 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +void deref_null() { + int* p = nullptr; + *p = 42; +} diff --git a/examples/demo/01/Makefile b/examples/demo/01/Makefile new file mode 100644 index 000000000..92075fae2 --- /dev/null +++ b/examples/demo/01/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = simple_null_interproc.c wrappers.c +OBJECTS = $(SOURCES:.c=.o) + +all: $(OBJECTS) + +.cpp.o: + ${CC} -c $< + +clean: + rm -rf $(OBJECTS) diff --git a/examples/demo/01/simple_null_interproc.c b/examples/demo/01/simple_null_interproc.c new file mode 100644 index 000000000..d1102ce7f --- /dev/null +++ b/examples/demo/01/simple_null_interproc.c @@ -0,0 +1,15 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +int* allocate_int(); +void set(int* p, int value); + +void deref_null() { + int* p = allocate_int(); + set(p, 42); +} diff --git a/examples/demo/01/simple_null_interproc_fixed.c b/examples/demo/01/simple_null_interproc_fixed.c new file mode 100644 index 000000000..c55c8d146 --- /dev/null +++ b/examples/demo/01/simple_null_interproc_fixed.c @@ -0,0 +1,19 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include + +int* allocate_int(); +void set(int* p, int value); + +void deref_null_ok() { + int* p = allocate_int(); + if (p != NULL) { + set(p, 42); + } + free(p); +} diff --git a/examples/demo/01/wrappers.c b/examples/demo/01/wrappers.c new file mode 100644 index 000000000..8276abb69 --- /dev/null +++ b/examples/demo/01/wrappers.c @@ -0,0 +1,11 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +int* allocate_int() { return malloc(sizeof(int)); } + +void set(int* p, int value) { *p = value; } diff --git a/examples/demo/02/Makefile b/examples/demo/02/Makefile new file mode 100644 index 000000000..6749eef7d --- /dev/null +++ b/examples/demo/02/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = Resources.java +OBJECT = Resources.class + +all: $(OBJECT) + +$(OBJECT): $(SOURCES) + javac $^ + +clean: + rm -rf $(OBJECT) diff --git a/examples/demo/02/Resources.java b/examples/demo/02/Resources.java new file mode 100644 index 000000000..4b74722d4 --- /dev/null +++ b/examples/demo/02/Resources.java @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +import java.io.File; +import java.io.FileInputStream; +import java.io.FileOutputStream; +import java.io.IOException; + +class Resources { + + public static void cat() throws IOException { + FileInputStream fis = null; + FileOutputStream fos = null; + try { + fis = new FileInputStream(new File("infile.txt")); + fos = new FileOutputStream(new File("outfile.txt")); + fos.write(fis.read()); + } finally { + if (fis != null) fis.close(); + if (fos != null) fos.close(); + } + } +} diff --git a/examples/demo/02/ResourcesFixed.java b/examples/demo/02/ResourcesFixed.java new file mode 100644 index 000000000..276ba645b --- /dev/null +++ b/examples/demo/02/ResourcesFixed.java @@ -0,0 +1,20 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +import java.io.File; +import java.io.FileInputStream; +import java.io.FileOutputStream; +import java.io.IOException; + +public class ResourcesFixed { + + public static void cat() throws IOException { + try (FileInputStream fis = new FileInputStream(new File("infile.txt")); + FileOutputStream fos = new FileOutputStream(new File("outfile.txt")); ) { + fos.write(fis.read()); + } + } +} diff --git a/examples/demo/03.fixed/Account.java b/examples/demo/03.fixed/Account.java new file mode 100644 index 000000000..1efb233b8 --- /dev/null +++ b/examples/demo/03.fixed/Account.java @@ -0,0 +1,12 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +@ThreadSafe +public interface Account { + void deposit(int amount); + int withdraw(int amount); +} diff --git a/examples/demo/03.fixed/AccountImplementation.java b/examples/demo/03.fixed/AccountImplementation.java new file mode 100644 index 000000000..369595e8a --- /dev/null +++ b/examples/demo/03.fixed/AccountImplementation.java @@ -0,0 +1,30 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +class AccountImplementation implements Account { + + int mBalance = 0; + + private void addToBalance(int amount) { + mBalance += amount; + } + + public synchronized void deposit(int amount) { + if (amount > 0) { + addToBalance(amount); + } + } + + public synchronized int withdraw(int amount){ + if (amount >= 0 && mBalance - amount >= 0) { + addToBalance(-amount); + return mBalance; + } else { + return 0; + } + } +} diff --git a/examples/demo/03.fixed/Client.java b/examples/demo/03.fixed/Client.java new file mode 100644 index 000000000..157331fdb --- /dev/null +++ b/examples/demo/03.fixed/Client.java @@ -0,0 +1,19 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +@ThreadSafe +public class Client { + + Account account; + + void getPaid(int amount) { + account.deposit(amount); + } + + int buyCoffee() { + return account.withdraw(5); + } +} diff --git a/examples/demo/03.fixed/Makefile b/examples/demo/03.fixed/Makefile new file mode 100644 index 000000000..c7947edd8 --- /dev/null +++ b/examples/demo/03.fixed/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = Account.java AccountImplementation.java Client.java +OBJECT = Client.class + +all: $(OBJECT) + +$(OBJECT): $(SOURCES) + javac $^ + +clean: + rm -rf $(OBJECT) diff --git a/examples/demo/03.fixed/ThreadSafe.java b/examples/demo/03.fixed/ThreadSafe.java new file mode 100644 index 000000000..97361463b --- /dev/null +++ b/examples/demo/03.fixed/ThreadSafe.java @@ -0,0 +1,7 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +public @interface ThreadSafe {} diff --git a/examples/demo/03/Account.java b/examples/demo/03/Account.java new file mode 100644 index 000000000..313fd59ab --- /dev/null +++ b/examples/demo/03/Account.java @@ -0,0 +1,10 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +public interface Account { + void deposit(int amount); + int withdraw(int amount); +} diff --git a/examples/demo/03/AccountImplementation.java b/examples/demo/03/AccountImplementation.java new file mode 100644 index 000000000..352ec52f0 --- /dev/null +++ b/examples/demo/03/AccountImplementation.java @@ -0,0 +1,30 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +class AccountImplementation implements Account { + + int mBalance = 0; + + private void addToBalance(int amount) { + mBalance += amount; + } + + public void deposit(int amount) { + if (amount > 0) { + addToBalance(amount); + } + } + + public int withdraw(int amount){ + if (amount >= 0 && mBalance - amount >= 0) { + addToBalance(-amount); + return mBalance; + } else { + return 0; + } + } +} diff --git a/examples/demo/03/Client.java b/examples/demo/03/Client.java new file mode 100644 index 000000000..157331fdb --- /dev/null +++ b/examples/demo/03/Client.java @@ -0,0 +1,19 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +@ThreadSafe +public class Client { + + Account account; + + void getPaid(int amount) { + account.deposit(amount); + } + + int buyCoffee() { + return account.withdraw(5); + } +} diff --git a/examples/demo/03/Makefile b/examples/demo/03/Makefile new file mode 100644 index 000000000..c7947edd8 --- /dev/null +++ b/examples/demo/03/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = Account.java AccountImplementation.java Client.java +OBJECT = Client.class + +all: $(OBJECT) + +$(OBJECT): $(SOURCES) + javac $^ + +clean: + rm -rf $(OBJECT) diff --git a/examples/demo/03/ThreadSafe.java b/examples/demo/03/ThreadSafe.java new file mode 100644 index 000000000..97361463b --- /dev/null +++ b/examples/demo/03/ThreadSafe.java @@ -0,0 +1,7 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +public @interface ThreadSafe {} diff --git a/examples/demo/04.fixed/Client.java b/examples/demo/04.fixed/Client.java new file mode 100644 index 000000000..274133589 --- /dev/null +++ b/examples/demo/04.fixed/Client.java @@ -0,0 +1,15 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public class Client { + + String foo() { + Library lib = new Library(); + T t = lib.get(); + return t == null? "default": t.toString(); + } +} diff --git a/examples/demo/04.fixed/Library.java b/examples/demo/04.fixed/Library.java new file mode 100644 index 000000000..3296ebafd --- /dev/null +++ b/examples/demo/04.fixed/Library.java @@ -0,0 +1,21 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public class Library { + + @Nullable T t; + + private native @Nullable T mayReturnNull(); + + public Library() { + t = mayReturnNull(); + } + + @Nullable public T get() { + return t; + } +} diff --git a/examples/demo/04.fixed/Makefile b/examples/demo/04.fixed/Makefile new file mode 100644 index 000000000..9024e83cd --- /dev/null +++ b/examples/demo/04.fixed/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = Client.java Library.java +OBJECT = Client.class + +all: $(OBJECT) + +$(OBJECT): $(SOURCES) + javac $^ + +clean: + rm -rf $(OBJECT) diff --git a/examples/demo/04.fixed/Nullable.java b/examples/demo/04.fixed/Nullable.java new file mode 100644 index 000000000..8f1ae2c6a --- /dev/null +++ b/examples/demo/04.fixed/Nullable.java @@ -0,0 +1,8 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public @interface Nullable {} diff --git a/examples/demo/04/Client.java b/examples/demo/04/Client.java new file mode 100644 index 000000000..4cb22cfb1 --- /dev/null +++ b/examples/demo/04/Client.java @@ -0,0 +1,14 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public class Client { + + String foo() { + Library lib = new Library(); + return lib.get().toString(); + } +} diff --git a/examples/demo/04/Library.java b/examples/demo/04/Library.java new file mode 100644 index 000000000..9b3c88f2c --- /dev/null +++ b/examples/demo/04/Library.java @@ -0,0 +1,21 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public class Library { + + T t; + + private native @Nullable T mayReturnNull(); + + public Library() { + t = mayReturnNull(); + } + + public T get() { + return t; + } +} diff --git a/examples/demo/04/Makefile b/examples/demo/04/Makefile new file mode 100644 index 000000000..9024e83cd --- /dev/null +++ b/examples/demo/04/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) 2017-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SOURCES = Client.java Library.java +OBJECT = Client.class + +all: $(OBJECT) + +$(OBJECT): $(SOURCES) + javac $^ + +clean: + rm -rf $(OBJECT) diff --git a/examples/demo/04/Nullable.java b/examples/demo/04/Nullable.java new file mode 100644 index 000000000..8f1ae2c6a --- /dev/null +++ b/examples/demo/04/Nullable.java @@ -0,0 +1,8 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +public @interface Nullable {} diff --git a/examples/demo/Makefile b/examples/demo/Makefile new file mode 100644 index 000000000..5d61749d5 --- /dev/null +++ b/examples/demo/Makefile @@ -0,0 +1,14 @@ +# Copyright (c) 2019-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +SUBDIRS = 00 01 02 03 + +default: all + +clean: + $(foreach subdir,$(SUBDIRS),$(MAKE) -C $(subdir) clean;) + rm -fr $(foreach subdir,$(SUBDIRS),$(subdir)/infer-out/) + +all: $(OBJECTS) diff --git a/examples/demo/demo.sh b/examples/demo/demo.sh new file mode 100755 index 000000000..d7f72d72d --- /dev/null +++ b/examples/demo/demo.sh @@ -0,0 +1,16 @@ +#!/bin/bash +# Copyright (c) 2019-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +set -e + +infer -- make -C 00 clean all +infer -- make -C 01 clean all +infer explore --no-source-preview --select 1 +infer -- make -C 02 clean all +infer explore --no-source-preview --select 0 +infer -- make -C 03 clean all +infer explore --no-source-preview --select 1 +infer --eradicate-only -- make -C 04 clean all