From a11add8fc1cb93ef1638788cac94e9ca6d21adae Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 17 May 2018 12:50:19 +0100 Subject: [PATCH 1/2] Expand the documentation of the goto-program instructions. This clarifies a few sources of mistakes and misconceptions as well as documenting some common practice. --- src/goto-programs/goto_program.h | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 88c84258b2f..0e5e08181a6 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -106,14 +106,20 @@ class goto_programt /// respective fields in this class: /// /// - GOTO: - /// if `guard` then goto `targets` + /// goto `targets` if and only if `guard` is true. + /// More than one target is deprecated. Its semantics was a + /// non-deterministic choice. /// - RETURN: /// Set the value returned by `code` (which shall be either nil or an /// instance of code_returnt) and then jump to the end of the function. + /// Many analysis tools remove these instructions before they start. /// - DECL: /// Introduces a symbol denoted by the field `code` (an instance of /// code_declt), the life-time of which is bounded by a corresponding DEAD - /// instruction. + /// instruction. Non-static symbols must be DECL'd before they are used. + /// - DEAD: + /// Ends the life of the symbol denoted by the field `code`. + /// After a DEAD instruction the symbol must be DECL'd again before use. /// - FUNCTION_CALL: /// Invoke the function denoted by field `code` (an instance of /// code_function_callt). @@ -124,7 +130,8 @@ class goto_programt /// Execute the `code` (an instance of codet of kind ID_fence, ID_printf, /// ID_array_copy, ID_array_set, ID_input, ID_output, ...). /// - ASSUME: - /// Wait for `guard` to evaluate to true. + /// This thread of execution waits for `guard` to evaluate to true. + /// Assume does not "retro-actively" affect the thread or any ASSERTs. /// - ASSERT: /// Using ASSERT instructions is the one and only way to express /// properties to be verified. Execution paths abort if `guard` evaluates @@ -134,17 +141,21 @@ class goto_programt /// - ATOMIC_BEGIN, ATOMIC_END: /// When a thread executes ATOMIC_BEGIN, no thread other will be able to /// execute any instruction until the same thread executes ATOMIC_END. + /// Concurrency is not supported by all analysis tools. /// - END_FUNCTION: - /// Can only occur as the last instruction of the list. + /// Must occur as the last instruction of the list and nowhere else. /// - START_THREAD: /// Create a new thread and run the code of this function starting from /// targets[0]. Quite often the instruction pointed by targets[0] will be /// just a FUNCTION_CALL, followed by an END_THREAD. + /// Concurrency is not supported by all analysis tools. /// - END_THREAD: /// Terminate the calling thread. + /// Concurrency is not supported by all analysis tools. /// - THROW: /// throw `exception1`, ..., `exceptionN` /// where the list of exceptions is extracted from the `code` field + /// Many analysis tools remove these instructions before they start. /// - CATCH, when code.find(ID_exception_list) is non-empty: /// Establishes that from here to the next occurrence of CATCH with an /// empty list (see below) if @@ -156,6 +167,7 @@ class goto_programt /// - CATCH, when empty code.find(ID_exception_list) is empty: /// clears all the catch clauses established as per the above in this /// function? + /// Many analysis tools remove these instructions before they start. class instructiont final { public: From 92b92d6032d4f0492603d2f85db5b52d6798b04c Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 18 May 2018 11:11:02 +0100 Subject: [PATCH 2/2] Correct the documentation of ASSERT : it does not alter control flow. After a discussion on issue #2031, this was agreed to be the correct semantics for the following reasons: 1. We want to check for conditions that do not result in termination. For example, generation of Inf and NaN, reachability of locations and unsigned overflow / underflow, error locations, exceptions or the use of program approximations. This is particularly important for binary analysis and security. 2. Allowing traces with multiple assertion failures reduces the number of solver calls and test cases generated, allowing minimisation without complex program manipulation. 3. If ASSERT alters control flow then the truth of assertions can change as more assertions are added, as the failures may get blocked. Adding more checks can result in less failures. 4. If ASSERT alters control flow, then it must be taken into account when slicing, meaning that every variable in any assert must be part of the slice. 5. ASSUME allows arbitrary blocking of execution, it is better than ASSERT is orthogonal and: ASSERT(X) ASSUME(X) is used for cases where assertion failure results in termination (such as null pointer dereference or array bounds failures). --- src/goto-programs/goto_program.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 0e5e08181a6..a630acafdb6 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -134,8 +134,9 @@ class goto_programt /// Assume does not "retro-actively" affect the thread or any ASSERTs. /// - ASSERT: /// Using ASSERT instructions is the one and only way to express - /// properties to be verified. Execution paths abort if `guard` evaluates - /// to false. + /// properties to be verified. An assertion is true / safe if `guard` + /// is true in all possible executions, otherwise it is false / unsafe. + /// The status of the assertion does not affect execution in any way. /// - SKIP, LOCATION: /// No-op. /// - ATOMIC_BEGIN, ATOMIC_END: