Modify Defect Checker Behavior During Analysis Without Changing PQL Queries

R2026b

You can separate defect checker logic from application-specific configuration in your PQL custom checkers. You can update this configuration data without modifying the query implementation or rebuilding the checker. This separation makes custom checkers easier to maintain and reuse across applications.

The directive Keyword

To create a configurable checker, use a predicate whose body is defined externally in a Datalog file. In your .pql file, you only declare this predicate using the directive keyword.

For example, the IsForbiddenFunctionName predicate in this defect checker is declared to be a directive:

package main
catalog Directive = {
    section Test = {
        rule Rule = {
            defect ForbiddenFunctionName =
                when Cpp.Function.is(&function)
                and function.name(&name)
                and IsForbiddenFunctionName(name)
                raise "found function with forbidden name {name}"
                on function
        }
    }
}

directive IsForbiddenFunctionName(Lang.String name)

To make the ForbiddenFunctionName defect checker flag the function names hello and world, create a Datalog file forbidden_func.dl with this content:

main.IsForbiddenFunctionName("hello").
main.IsForbiddenFunctionName("world").

When running the analysis, provide this Datalog file to Polyspace® using the -code-behavior-specifications option.

polyspace-query-language test -s source.c -code-behavior-specifications forbidden_func.dl

To reconfigure your checker (for example, update the list of forbidden function names), simply update the Datalog file before running your analysis. You do not need to change the PQL queries or regenerate the .pschk file.

How Directives Behave

A directive is a predicate that has zero or more input parameters and no output parameter.

  • If the directive has at least one parameter, the Datalog file specifies the parameter tuples for which the predicate is true. For every other tuple, the predicate is false.

  • A directive that has no parameters is just a boolean value. If the predicate is present in your Datalog file, it is always true. If the predicate is commented out or not listed, it is always false.

Examples of Directive Use in Checkers

These are some simple examples of PQL queries that use directives to configure the checker. You can place the directive declaration in the same package as the defect checker or in a separate package for better organization.

Use 0-Parameter Directive to Enable or Disable Checker

In your main.pql file, define a defect checker that reports a violation if a variable in your source code is of the int data type. Use the config.IsIntForbidden directive to control if this checker should be enabled.

package main
catalog Directive = {
    section Test = {
        rule Rule = {
            defect ForbiddenInt =
                when config.IsIntForbidden()
                and Cpp.Variable.is(&var)
                and var.type(&type)
                and type.isInt()
                raise "forbidden type: int"
                on var
        }
    }
}

To put the directive in the config package, create this separate declaration.pql file.

package config
directive IsIntForbidden()

When you run the analysis:

  • To enable the checker, provide a Datalog file that contains the config.IsIntForbidden predicate:

    config.IsIntForbidden().

  • To disable the checker, provide a Datalog file that does not contain the config.IsIntForbidden predicate. For example, you can comment out the line containing the predicate:

    // config.IsIntForbidden().

Use 1-Parameter Directive to Supply Special Names or Values to Checker

In your main.pql file, define a defect checker that forbids specific data type names for variables in your source code. Use the IsForbiddenTypeName directive to control which data type names are forbidden. In this example, include the declaration of the directive in the main package itself.

package main
catalog Directive = {
    section Test = {
        rule Rule = {
            defect ForbiddenTypeName =
                when Cpp.Variable.is(&var)
                and var.type(&type)
                and type.toString(&typename)
                and IsForbiddenTypeName(typename)
                raise "forbidden type: {typename}"
                on var
        }
    }
}

directive IsForbiddenTypeName(Lang.String typename)

When you run the analysis, specify the forbidden type names in the Datalog file. For example, to forbid the type names int and myType, create a Datalog file with this content:

main.IsForbiddenTypeName("int").
main.IsForbiddenTypeName("myType").

Like in the previous example, if you do not want to forbid any type name, provide a Datalog file with all the main.IsForbiddenTypeName predicate lines commented out.

Use 2-Parameter Directive to Supply Special Name Combinations to Checker

In your main.pql file, define a defect checker that forbids specific (function name, return type name) combinations in your source code. Use the config.test.IsForbiddenFunctionReturnType directive to control which combinations are forbidden.

package main
catalog Directive = {
    section Test = {
        rule Rule = {
            defect ForbiddenReturnType =
                when Cpp.Function.is(&func)
                and func.name(&funcname)
                and func.returnType(&type)
                and type.toString(&typename)
                and config.test.IsForbiddenFunctionReturnType(funcname,typename)
                raise "forbidden return type: {typename}"
                on func
        }
    }
}

To put the directive in the config.test package, create this separate declaration.pql file.

package config.test
directive IsForbiddenFunctionReturnType(Lang.String funcname, Lang.String typename)

When you run the analysis, specify the forbidden (function name, return type name) combinations in the Datalog file. For example, to forbid the return type name myType for the function foo and the return type name float for the function bar, create a Datalog file with this content:

config.test.IsForbiddenFunctionReturnType("foo","myType").
config.test.IsForbiddenFunctionReturnType("bar","float").

Like in the preceding two examples, if you do not want to forbid any combination, provide a Datalog file with all the config.test.IsForbiddenFunctionReturnType predicate lines commented out.

See Also

|

Topics