Detect Implicit Casts with Precision Loss

This example shows how to use Polyspace Query Language (PQL) to check for violation of this rule: Avoid implicit casts that results in precision loss.

This topic focuses on application of PQL. For more details about creating semantic defect checkers, see Detect Semantic Issues Using Polyspace Query Language Semantic Classes.

Analyze Rule

To implement the rule in PQL, analyze the components of the rule:

• Precision loss — When a variable is cast into a type that is narrowed than the original type, the cast results in precision loss. For example, if you cast a float variable to int, it results in precision loss. The predicate precisionLoss of the class Cast detects such casts.

• Implicit casts — If your code performs the cast without explicitly using one of the explicit cast syntaxes, the cast is implicit. The predicate isimplicit of the class Cast detects implicit casts.

Implement Rule in PQL

The defect can be defined like this:

defect rmydefectd =
when
  Cpp.Cast.is(&cs)
  and cs.isImplicit()
  and cs.precisionLoss()
  raise "Cast with precision loss."
on cs

Test Defect

To test and verify the defect:

1. Initialize a test standard in a writable location:

   polyspace-query-language init

2. In main.pql, insert the defect in a test standard:

   package main
   
   /// Main PQL file defines the catalog of your PQL project.
   /// The catalog is a collection of sections.
   catalog PQL_CastPrecisionLoss = {
   #[Description("MySection")]
   	section mysection = {
   #[Description("myRule"), Id(Rule1)]
   		rule myRule = {
   			defect rmydefectd =
   			when
               Cpp.Cast.is(&cs)
   			and cs.isImplicit()
   			and cs.precisionLoss()
               raise "Cast with precision loss."
   			on cs
   		}
   	}
   }

3. Package the standard in a pschk file:

   polyspace-query-language package

4. Create example.cpp in the same folder:

   #include <cstdint>
   
   float readHWSensor();
   void noReturnFunction();
   
   int returnImportantValue()
   {
       // implicit cast from float to int may lead to precision loss
       return readHWSensor(); // expect-1-Rule1
   }
   
   void cast_return_to_void()
   {
       // explicit cast for int to void
       (void)returnImportantValue(); // expect-0-Rule1
       (void)noReturnFunction();     // expect-0-Rule1
   }
   
   int undetected_precisionLosses()
   {
       // here EDG is folding the float constant into an integer constant,
       // there is no cast expression in vvir.
       return 1.2f;
   }
   
   extern unsigned readU();
   extern double readD();
   
   void precision()
   {
       int i = static_cast<int>(readU()); // expect-0-Rule1
       unsigned j = i;                    // expect-1-Rule1
   
       float f = static_cast<float>(readD()); // expect-0-Rule1
   
       double d = static_cast<double>(f); // expect-0-Rule1
   
       int x = // expect-1-Rule1
           f + d;
   
       char c = x; // expect-1-Rule1
   }
   
   template <typename T>
   T divBy2(T &v)
   {
       v = v / static_cast<T>(2);
   }
   
   double result()
   {
       unsigned res;
       // although it is never used later on, result is not immediately discarded,
       // hence RULE_02 does not fire.
       res = readU(); 
   
       double d;
       d = readD(); 
       divBy2(d);   
       return d;
   }
   
   double integralToDouble(int x)
   {
       if (x == 0)
       {
           // 2^53
           return static_cast<double>(9007199254740992); // expect-0-Rule1
       }
       else if (x == 1)
       {
           // 2^53+1
           return static_cast<double>(9007199254740993); // expect-0-Rule1
       }
       else if (x == 2)
       {
           // -2^53
           return static_cast<double>(-9007199254740992); // expect-0-Rule1
       }
       else
       {
           // -2^53-1
           return static_cast<double>(-9007199254740993); // expect-0-Rule1
       }
   }

   This code explicitly states where a violation of the rule is expected using annotation expect-1-Rule1. Absence of the violation is also annotated using expect-0-Rule1.

5. Run a test for the defect on the example code:

   polyspace-query-language test example.cpp

   The test verifies the expected violations as well as the expected absence of violations:

   Number of actual defects: 4
   Number of expected annotations: 13 (including 9 expected absence of defects).
   _______________________________________________
     Checking expected defects with actuals...
     -----------------------------------------
   _______________________________________________
     Looking for unexpected defects...
   -------------------------------------------
   _______________________________________________
   Tests passed