C++/Docs: more examples and rewording for guards

This commit is contained in:
Robert Marsh
2019-10-16 12:45:59 -07:00
parent 9aea2eda9b
commit 0cc0977a09

View File

@@ -3,10 +3,10 @@ Using the guards library in C and C++
Overview
--------
The guards library (defined in ``semmle.code.cpp.controlflow.Guards``) provides a class ``GuardCondition`` representing Boolean values that are used to make control flow decisions.
The guards library (defined in ``semmle.code.cpp.controlflow.Guards``) provides a class `GuardCondition <https://help.semmle.com/qldoc/cpp/semmle/code/cpp/controlflow/Guards.qll/type.Guards$GuardCondition.html>`__ representing Boolean values that are used to make control flow decisions.
A ``GuardCondition`` is considered to guard a basic block if the block can only be reached if the ``GuardCondition`` is evaluated a certain way. For instance, in the following code, ``x < 10`` is a ``GuardCondition``, and it guards all the code before the return statement.
.. code:: cpp
.. code-block:: cpp
if(x < 10) {
f(x);
@@ -24,7 +24,7 @@ The ``controls`` predicate helps determine which blocks are only run when the ``
In the following code sample, the call to ``isValid`` controls the calls to ``performAction`` and ``logFailure`` but not the return statement.
.. code:: cpp
.. code-block:: cpp
if(isValid(accessToken)) {
performAction();
@@ -35,22 +35,49 @@ In the following code sample, the call to ``isValid`` controls the calls to ``pe
}
return succeeded;
In the following code sample, the call to `isValid` controls the body of the if and also the code after the if.
.. code-block:: cpp
if(!isValid(accessToken)) {
logFailure();
return 0;
}
performAction();
return succeeded;
The ``ensuresEq`` and ``ensuresLt`` predicates
----------------------------------------------
The ``ensuresEq`` and ``ensuresLt`` predicates are the main way of determining what, if any, guarantees the ``GuardCondition`` provides for a given basic block.
The ``ensuresEq`` predicate
***************************
When ``ensuresEq(left, right, k, block, true)`` holds, then ``block`` is only executed if ``left`` was equal to ``right + k`` at their last evaluation. When ``ensuresEq(left, right, k, block, false)`` holds, then ``block`` is only executed if ``left`` was not equal to ``right + k`` at their last evaluation.
The ``ensuresLt`` predicate
***************************
When ``ensuresLt(left, right, k, block, true)`` holds, then ``block`` is only executed if ``left`` was strictly less than ``right + k`` at their last evaluation. When ``ensuresLt(left, right, k, block, false)`` holds, then ``block`` is only executed if ``left`` was greater than or equal to ``right + k`` at their last evaluation.
.. TODO: examples for these predicates (none for others?)
In the following code sample, the comparison on the first line ensures that ``index`` is less than ``size`` in the then block, and that ``index`` is greater than or equal to ``size`` in the else block.
.. code-block:: cpp
if(index < size) {
ret = array[index];
} else {
ret = nullptr
}
return ret;
The ``comparesEq`` and ``comparesLt`` predicates
------------------------------------------------
The ``comparesEq`` and ``comparesLt`` predicates help determine if the ``GuardCondition`` evaluates to true.
The ``comparesEq`` predicate
****************************
``comparesEq(left, right, k, true, testIsTrue)`` holds if ``left`` equals ``right + k`` when the expression evaluates to ``testIsTrue``.
The ``comparesLt`` predicate
****************************
``comparesLt(left, right, k, isLessThan, testIsTrue)`` holds if ``left < right + k`` evaluates to ``isLessThan`` when the expression evaluates to ``testIsTrue``.