Improved constant value checks in Java with SMT solver integration
More Powerful Constant Value Checking with SMT Solving
Programming Languages
Summary
Programming languages often check if variables hold only allowed values to avoid bugs. The authors show that existing Java tools for checking constant values can miss some issues when the code is complex. They enhance this checking by using SMT solvers, which are mathematical tools that decide if logical conditions can be true. This allows the checker to verify more complicated cases and use new types that depend on other variables’ values.
What this means in practice
- •For java developers: Check more complex constraints on integer and boolean variables in Java programs to catch subtle bugs missed by simpler type checkers.
- •For software quality engineers: Integrate SMT-based constant value checking into code quality tools to improve detection of type-related errors in Java projects.
Authors
Jonas Mittnacht, Florian Lanzinger
Abstract
Pluggable type systems extend the basic type system of a programming language by introducing additional type hierarchies to specify more complex properties and dependencies between variables. We consider the Constant Value Checker, a pluggable type checker for Java implemented using the Checker Framework, which provides various pluggable type systems and corresponding checkers. The Constant Value Checker lets users specify restrictions on the values a primitive integer or boolean variable can hold using a set or range of constant values. However, the current implementation of the Value Checker makes use of a limited set of syntactic typing rules that, in practice, often fail to verify well-typedness of more complex code. In this paper, we introduce an extension to the Checker Framework using Satisfiability Modulo Theories (SMT) solvers to address these limitations by creating corresponding first-order logic formulas for expressions whose type checks fail with the current syntactic typing rules and determining their well-typedness based on the satisfiability of these formulas. Furthermore, we introduce new dependent types for specifying allowed values with expressions that can depend on other variables in the program.