[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

@@ -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)

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;
+}

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)

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 <stdlib.h>
+
+int* allocate_int();
+void set(int* p, int value);
+
+void deref_null() {
+  int* p = allocate_int();
+  set(p, 42);
+}

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 <stdlib.h>
+
+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);
+}

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 <stdlib.h>
+
+int* allocate_int() { return malloc(sizeof(int)); }
+
+void set(int* p, int value) { *p = value; }

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)

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();
+    }
+  }
+}

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());
+    }
+  }
+}

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);
+}

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;
+    }
+  }
+}

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);
+  }
+}

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)

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 {}

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);
+}

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;
+    }
+  }
+}

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);
+  }
+}

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)

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 {}

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<T> {
+
+  String foo() {
+    Library<T> lib = new Library<T>();
+    T t = lib.get();
+    return t == null? "default": t.toString();
+  }
+}

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<T> {
+
+  @Nullable T t;
+
+  private native @Nullable T mayReturnNull();
+
+  public Library() {
+    t = mayReturnNull();
+  }
+
+  @Nullable public T get() {
+    return t;
+  }
+}

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)

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 {}

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<T> {
+
+  String foo() {
+    Library<T> lib = new Library<T>();
+    return lib.get().toString();
+  }
+}

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 t;
+
+  private native @Nullable T mayReturnNull();
+
+  public Library() {
+    t = mayReturnNull();
+  }
+
+  public T get() {
+    return t;
+  }
+}

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)

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 {}

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)

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