Debugger fails with textual cbmc output

[markrtuttle]

The debugger fails when run on the output of cbmc-viewer when cbmc-viewer was run on the textual output of cbmc.

To reproduce, build any of the FreeRTOS proofs using the legacy starter kit:

git clone https://github.com/FreeRTOS/FreeRTOS-Plus-TCP.git
cd FreeRTOS-Plus-TCP
git submodule update --init --checkout --recursive
cd test/cbmc/proofs
./prepare.py 
cd ARP/ARPAgeCache
make

This runs cbmc in text mode without the --xml-ui flag and produces cbmc.txt instead of cbmc.xml.

Now start up code, load the traces, and start the debugger.

The debugger fails in simulatorState.addAssignment while trying to parse the scope of the left-hand side of the assignment because the scope is null. This invocation of addAssignment occurs while simulating an assignment step. The null value arises because the scope is taken from lhs-lexical-scope in the trace step.

The problem is that when cbmc-viewer is scanning the traces produced by cbmc, viewer finds a value for lhs-lexical-scope when parsing xml output of cbmc not when parsing text output or parsing json output. The problem is that this scope simply isn't present in the textual output of cbmc.

[karkhaz]

Thank you. I wonder what the impact of this is? Are there specific authors of the FreeRTOS repository who are attempting to use the debugger?

It seems reasonable to me for the debugger to assume the presence of certain files that are emitted from the more widely-used starter kit. If the FreeRTOS's custom starter kit doesn't write these files out, then it seems like FreeRTOS should be fixed (e.g. add --xml-ui). I'm not convinced that we should fix anything up in the debugger.

Could you clarify what you're expecting here? As you point out, the debugger cannot use the text output, the only option is to give it XML. I'm inclined to close this issue, and possibly create one on FreeRTOS if it's causing any actual pain.

[markrtuttle]

This bug report comes from a FreeRTOS developer trying to debug proof issues. I proposed to him that, as a short-term solution, I think it should be fairly easy to modify prepare.py to generate a Makefile that produces and consumes xml output.

[karkhaz]

Thank you. I'll see if we can fix FreeRTOS's starter kit in a more permanent way. Keeping this issue open until then.

[markrtuttle]

Applying this patch file makefile.patch to Makefile.template appears to solve the problem. Maybe we could apply this patch file in all of the legacy FreeRTOS and FreeRTOS-Plus-TCP proof repositories.

This patch has the side effect of renaming the report directory from the old html to the modern report name.

[karkhaz]

OK, I posted PRs for FreeRTOS/FreeRTOS-Plus-TCP and FreeRTOS/FreeRTOS/

[markrtuttle]

Closed by FreeRTOS/FreeRTOS-Plus-TCP#673 and FreeRTOS/FreeRTOS#912