From b35b913cbec2c4ec97c64f50606e42a2b55f96d8 Mon Sep 17 00:00:00 2001 From: Daniele Demichelis Date: Wed, 21 Feb 2018 00:00:47 +0100 Subject: [PATCH] Bael 1490 the checker framework and java pluggable type systems (#3584) * BAEL-1490 First examples, Maven setup * BAEL-1490 Each checker has its own source file * BAEL-1490 Added checker for String.format * BAEL-1490 The Checker Framework and Java Pluggable Type Systems * Added comments, removed example that is probably too technical for a brad audience. --- checker-plugin/pom.xml | 114 ++++++++++++++++++ .../baeldung/typechecker/FakeNumExample.java | 42 +++++++ .../baeldung/typechecker/FormatExample.java | 23 ++++ .../baeldung/typechecker/KeyForExample.java | 31 +++++ .../typechecker/MonotonicNotNullExample.java | 28 +++++ .../baeldung/typechecker/NonNullExample.java | 27 +++++ .../baeldung/typechecker/RegexExample.java | 18 +++ 7 files changed, 283 insertions(+) create mode 100644 checker-plugin/pom.xml create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/FakeNumExample.java create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/FormatExample.java create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/KeyForExample.java create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/MonotonicNotNullExample.java create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/NonNullExample.java create mode 100644 checker-plugin/src/main/java/com/baeldung/typechecker/RegexExample.java diff --git a/checker-plugin/pom.xml b/checker-plugin/pom.xml new file mode 100644 index 0000000000..bc7a669d4f --- /dev/null +++ b/checker-plugin/pom.xml @@ -0,0 +1,114 @@ + + 4.0.0 + com.baeldung + checker-plugin + jar + 1.0-SNAPSHOT + checker-plugin + http://maven.apache.org + + + + + + ${org.checkerframework:jdk8:jar} + + + + + + + + + + org.checkerframework + checker-qual + 2.3.1 + + + org.checkerframework + checker + 2.3.1 + + + org.checkerframework + jdk8 + 2.3.1 + + + + org.checkerframework + compiler + 2.3.1 + + + + + + + + + + org.apache.maven.plugins + maven-dependency-plugin + + + + + properties + + + + + + + maven-compiler-plugin + 3.6.1 + + 1.8 + 1.8 + + + + 10000 + 10000 + + + + org.checkerframework.checker.nullness.NullnessChecker + org.checkerframework.checker.interning.InterningChecker + org.checkerframework.checker.fenum.FenumChecker + org.checkerframework.checker.formatter.FormatterChecker + org.checkerframework.checker.regex.RegexChecker + + + -AprintErrorStack + + + -Xbootclasspath/p:${annotatedJdk} + + + + + + -Awarns + + + + + + + diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/FakeNumExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/FakeNumExample.java new file mode 100644 index 0000000000..f1769cfdea --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/FakeNumExample.java @@ -0,0 +1,42 @@ +package com.baeldung.typechecker; + +import org.checkerframework.checker.fenum.qual.Fenum; + +//@SuppressWarnings("fenum:assignment.type.incompatible") +public class FakeNumExample { + + // Here we use some String constants to represents countries. + static final @Fenum("country") String ITALY = "IT"; + static final @Fenum("country") String US = "US"; + static final @Fenum("country") String UNITED_KINGDOM = "UK"; + + // Here we use other String constants to represent planets instead. + static final @Fenum("planet") String MARS = "Mars"; + static final @Fenum("planet") String EARTH = "Earth"; + static final @Fenum("planet") String VENUS = "Venus"; + + // Now we write this method and we want to be sure that + // the String parameter has a value of a country, not that is just a String. + void greetCountries(@Fenum("country") String country) { + System.out.println("Hello " + country); + } + + // Similarly we're enforcing here that the provided + // parameter is a String that represent a planet. + void greetPlanets(@Fenum("planet") String planet) { + System.out.println("Hello " + planet); + } + + public static void main(String[] args) { + + FakeNumExample obj = new FakeNumExample(); + + // This will fail because we pass a planet-String to a method that + // accept a country-String. + obj.greetCountries(MARS); + + // Here the opposite happens. + obj.greetPlanets(US); + } + +} diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/FormatExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/FormatExample.java new file mode 100644 index 0000000000..2fa53ff2c2 --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/FormatExample.java @@ -0,0 +1,23 @@ +package com.baeldung.typechecker; + +public class FormatExample { + + public static void main(String[] args) { + + // Just enabling org.checkerframework.checker.formatter.FormatterChecker + // we can be sure at compile time that the format strings we pass to format() + // are correct. Normally we would have those errors raised just at runtime. + // All those formats are in fact wrong. + + String.format("%y", 7); // error: invalid format string + + String.format("%d", "a string"); // error: invalid argument type for %d + + String.format("%d %s", 7); // error: missing argument for %s + + String.format("%d", 7, 3); // warning: unused argument 3 + + String.format("{0}", 7); // warning: unused argument 7, because {0} is wrong syntax + } + +} diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/KeyForExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/KeyForExample.java new file mode 100644 index 0000000000..b3072b72ee --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/KeyForExample.java @@ -0,0 +1,31 @@ +package com.baeldung.typechecker; + +import org.checkerframework.checker.nullness.qual.KeyFor; + +import java.util.HashMap; +import java.util.Map; + +public class KeyForExample { + + private final Map config = new HashMap<>(); + + KeyForExample() { + + // Here we initialize a map to store + // some config data. + config.put("url", "http://1.2.3.4"); + config.put("name", "foobaz"); + } + + public void dumpPort() { + + // Here, we want to dump the port value stored in the + // config, so we declare that this key has to be + // present in the config map. + // Obviously that will fail because such key is not present + // in the map. + @KeyFor("config") String key = "port"; + System.out.println( config.get(key) ); + } + +} diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/MonotonicNotNullExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/MonotonicNotNullExample.java new file mode 100644 index 0000000000..c4b9c6afe1 --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/MonotonicNotNullExample.java @@ -0,0 +1,28 @@ +package com.baeldung.typechecker; + +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; + +import java.util.Date; + +public class MonotonicNotNullExample { + + // The idea is we need this field to be to lazily initialized, + // so it starts as null but once it becomes not null + // it cannot return null. + // In these cases, we can use @MonotonicNonNull + @MonotonicNonNull private Date firstCall; + + public Date getFirstCall() { + if (firstCall == null) { + firstCall = new Date(); + } + return firstCall; + } + + public void reset() { + // This is reported as error because + // we wrongly set the field back to null. + firstCall = null; + } + +} diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/NonNullExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/NonNullExample.java new file mode 100644 index 0000000000..c929eea23f --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/NonNullExample.java @@ -0,0 +1,27 @@ +package com.baeldung.typechecker; + +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class NonNullExample { + + // This method's parameter is annotated in order + // to tell the pluggable type system that it can never be null. + private static int countArgs(@NonNull String[] args) { + return args.length; + } + + // This method's parameter is annotated in order + // to tell the pluggable type system that it may be null. + public static void main(@Nullable String[] args) { + + // Here lies a potential error, + // because we pass a potential null reference to a method + // that does not accept nulls. + // The Checker Framework will spot this problem at compile time + // instead of runtime. + System.out.println(countArgs(args)); + + } + +} diff --git a/checker-plugin/src/main/java/com/baeldung/typechecker/RegexExample.java b/checker-plugin/src/main/java/com/baeldung/typechecker/RegexExample.java new file mode 100644 index 0000000000..9503865214 --- /dev/null +++ b/checker-plugin/src/main/java/com/baeldung/typechecker/RegexExample.java @@ -0,0 +1,18 @@ +package com.baeldung.typechecker; + +import org.checkerframework.checker.regex.qual.Regex; + +public class RegexExample { + + // For some reason we want to be sure that this regex + // contains at least one capturing group. + // However, we do an error and we forgot to define such + // capturing group in it. + @Regex(1) private static String findNumbers = "\\d*"; + + public static void main(String[] args) { + String message = "My phone number is +3911223344."; + message.matches(findNumbers); + } + +}