Document symex instructions #7497

NlightNFotis · 2023-01-23T14:56:23Z

Add documentation for the goto-symex and goto-program-instructions.

martin-cs · 2023-01-23T22:36:02Z

doc/architectural/central-data-structures.md

+The `goto_modelt` is the main data structure that CBMC (and the other tools) use to
+represent GOTO-IR (the `GOTO` Intermediate Representation).
+
+A `goto_modelt` is effectively a product type, consisting of:


Same comment as on the previous draft; I would suggest using "pair" or "tuple" as a more C++-ish way of saying this.

martin-cs · 2023-01-23T22:36:48Z

doc/architectural/central-data-structures.md

+
+A `goto_modelt` is effectively a product type, consisting of:
+
+* A list of GOTO functions (pseudocode: `type goto_functionst = list<goto_functiont>`)


It's not really a list...

martin-cs · 2023-01-23T22:37:17Z

doc/architectural/central-data-structures.md

+A `goto_functiont` is also a product type. It's designed to represent a function
+at the IR level, and effectively it's the following ADT (in pseudocode):
+
+```js


Could you use C++-style pseudocode?

And / or a reference to the code.

martin-cs · 2023-01-23T22:40:47Z

doc/architectural/central-data-structures.md

+Another important data structure that needs to be discussed at this point is
+`source_locationt`.
+
+This is an `irept`. `irep`s are the central data structure that model most entities inside


irept is pretty critical and deserves space of its own, not just under source_locationt

martin-cs · 2023-01-23T22:42:11Z

doc/architectural/symex-instructions.md

+
+## A (very) short introduction to Symex
+
+Symex is, at its core, a GOTO-program interpreter. While Symex is interpreting


'an interpreter BUT using symbolic values, not literal ones. For example... Note that this produces a formula which describes all possible outputs rather than a single output value.'

Agreed. Changed

martin-cs · 2023-01-23T22:43:18Z

doc/architectural/symex-instructions.md

+}
+```
+
+If we ask CBMC to print the GOTO-program instructions with `--show-goto-functions`, then part


Should be in the goto-functions documentation rather than just in symex.

I presume (hope) it is. Maybe here we should have a cross reference to that part of the goto-functions documentation.

martin-cs · 2023-01-23T22:46:28Z

regression/cbmc/field-sensitivity15/test.desc

+^SIGNAL=0$
+--
+--
+The test is a minimized version of code generated from s2n-quic using Kani.


More tests are always good but why is this in a documentation PR? I guess I have missed something...

martin-cs · 2023-01-23T22:50:25Z

src/goto-symex/symex_assign.cpp

@@ -215,14 +215,6 @@ void symex_assignt::assign_non_struct_symbol(
      assignment.rhs,
      target,
      symex_config.allow_pointer_unsoundness);
-    // Erase the composite symbol from our working state. Note that we need to


There could well be a good justification for this removal of code but please could they not be in a documentation PR?

NlightNFotis · 2023-01-24T10:03:05Z

Hi @martin-cs , this was branched of at an earlier point from the same branch as the other documentation PR (#7470), and it hasn't tracked the changes that addressed the comments on the other PR, so it appears like it has the same problems, but it's just being stale.

This means that the earlier commits here are just adding noise, so I will focus on addressing everything on the other PR, get it merged, and then rebase this one on top of develop, for a cleaner, less stale history. I will then address the comments that remain relevant after the rebase and ask you for a re-review.

jimgrundy · 2023-01-25T20:59:26Z

doc/architectural/cbmc-architecture.md

@@ -64,9 +71,10 @@ To be documented.

 To be documented.

-## Goto functions &rarr; BMC &rarr; Counterexample (trace) ##
+## Goto functions &rarr; BMC &rarr; Counterexample (trace)


Why this change? Doesn't seem to match the other lines.

I did this as a drive-by clean up. As far as I know headings in markdown are only prepended by a ##.

On a second visit, it appears that doxygen does support any number of # after the title, but that's invalid markdown.

If this change offends in any capacity however, it's easy to be reverted.

It seems this file has that issue multiple times. Can you please clean up all occurrences? (src/goto-instrument/README.md also suffers from this problem. Maybe do one commit that does the cleanup for all of these?)

I mean fair enough. I was thinking maybe there should be a separate PR that does this clean up. Or, at least, maybe consistently clean them all up in this file as there are many line this (as Michael as noticed). You want to leave the file in a consistent state so that newcomers will follow the example.

I will make trailing # consistent by removing them in the files touched by this PR.

jimgrundy · 2023-01-25T21:08:58Z

doc/architectural/central-data-structures.md

+Another important data structure that needs to be discussed at this point is
+`source_locationt`.
+
+This is an `irept`. `irep`s are the central data structure that model most entities inside


jimgrundy · 2023-01-25T21:11:59Z

doc/architectural/symex-instructions.md

+purposes:
+
+```c
+enum goto_program_instruction_typet


Maybe throw in some "..."s here to emphasize that this isn't the full set.

jimgrundy · 2023-01-25T21:13:50Z

doc/architectural/symex-instructions.md

+enum goto_program_instruction_typet
+{
+  GOTO = 1,              // branch, possibly guarded
+  ASSUME = 2,            // non-failing guarded self loop


This is perhaps not the worlds most obvious description of an assumption.

The reason for this is that it's a copy from goto_program_instruction_typet where the comment of ASSUME states what was written.

I changed it to ASSUME to avoid confusion.

jimgrundy · 2023-01-25T21:15:15Z

doc/architectural/symex-instructions.md

+```c
+int main(int argc, char **argv)
+{
+    int arry[] = {0, 1, 2, 3};


It this point you may as well just say "array", or go the whole way and call it "a". "arry" offers neither brevity nor clarity.

Changed to a and improved assertion comment

jimgrundy · 2023-01-25T21:16:20Z

doc/architectural/symex-instructions.md

+}
+```
+
+If we ask CBMC to print the GOTO-program instructions with `--show-goto-functions`, then part


I presume (hope) it is. Maybe here we should have a cross reference to that part of the goto-functions documentation.

jimgrundy · 2023-01-25T21:18:58Z

doc/architectural/symex-instructions.md

+dispatching functions are usually in their own file, designated by the instruction's
+name. As an example, you can find the code for the function goto_symext::symex_goto
+in [symex_goto.cpp](../../src/goto-symex/symex_goto.cpp)
+


A description of what symex produces, why, and what it means could use a longer explanation.

jimgrundy · 2023-01-25T21:24:34Z

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -74,8 +74,8 @@ void multi_path_symex_only_checkert::generate_equation()
 {
  const auto symex_start = std::chrono::steady_clock::now();



This PR seems like it should be a couple of PRs about different things. This doesn't feel like it belongs in a documentation PR.

…tions.

codecov · 2023-02-09T15:36:12Z

Codecov Report

Base: 78.49% // Head: 78.49% // No change to project coverage 👍

Coverage data is based on head (1eb26aa) compared to base (eb883a6).
Patch has no changes to coverable lines.

❗ Current head 1eb26aa differs from pull request most recent head a4464fb. Consider uploading reports for the commit a4464fb to get more accurate results

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7497   +/-   ##
========================================
  Coverage    78.49%   78.49%           
========================================
  Files         1663     1663           
  Lines       191339   191339           
========================================
  Hits        150185   150185           
  Misses       41154    41154

Impacted Files	Coverage Δ
src/analyses/ai.h	`64.28% <0.00%> (ø)`

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

tautschnig · 2023-02-09T15:44:12Z

doc/architectural/cbmc-architecture.md

@@ -64,9 +71,10 @@ To be documented.

 To be documented.

-## Goto functions &rarr; BMC &rarr; Counterexample (trace) ##
+## Goto functions &rarr; BMC &rarr; Counterexample (trace)


It seems this file has that issue multiple times. Can you please clean up all occurrences? (src/goto-instrument/README.md also suffers from this problem. Maybe do one commit that does the cleanup for all of these?)

tautschnig · 2023-02-09T15:48:30Z

doc/architectural/symex-instructions.md

+Symex is, at its core, a GOTO-program interpreter. While Symex is interpreting
+the program, it's also building a list of SSA steps that form part of the equation
+that is to be sent to the solver.


Would it be better to refer the reader to src/goto-symex/README.md?

Good idea, added

tautschnig · 2023-02-09T15:50:46Z

doc/architectural/symex-instructions.md

+  SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
+  // 5 file /tmp/example.c line 5 function main
+  END_FUNCTION
+```
+
+In the above excerpt, the capitalised words at the beginning each instruction are the
+correspondent instruction types (`DECL`, `ASSIGN`, etc).


All of the above really belongs to goto programs, not so much to symex, does it?

Yes, but in this file we are describing the Instruction type that is exactly what we are showing.
In my opinion it is useful to show how the goto-program looks like.

esteffin · 2023-02-20T14:51:53Z

@martin-cs Can you please have a look and confirm your concerns have been addressed?

TGWDB · 2023-02-27T10:52:16Z

@martin-cs Can you please act on this soon? It's been a week since the last request for review and more than that since various fixes were pushed. Note that we plan to force merge this in about 24 hours unless there is some new specific concern. We can make further changes in follow up tickets if necessary, but we'd like to merge this and progress ASAP.

NlightNFotis added the documentation label Jan 23, 2023

NlightNFotis self-assigned this Jan 23, 2023

NlightNFotis requested review from martin-cs, chris-ryder, peterschrammel, tautschnig, kroening, romainbrenguier, jimgrundy and TGWDB as code owners January 23, 2023 14:56

martin-cs requested changes Jan 23, 2023

View reviewed changes

NlightNFotis added the do not review label Jan 24, 2023

jimgrundy requested changes Jan 25, 2023

View reviewed changes

Add some high-level documentation on symex and GOTO-program instruc…

1eb26aa

…tions.

NlightNFotis force-pushed the document_symex_instructions branch from 1ce9b87 to 1eb26aa Compare February 9, 2023 14:47

NlightNFotis assigned esteffin and unassigned NlightNFotis Feb 9, 2023

tautschnig reviewed Feb 9, 2023

View reviewed changes

Enrico Steffinlongo added 2 commits February 16, 2023 11:39

Removed trailing # from markdown

2c5fa86

Addressed some PR reviews comment

a4464fb

jimgrundy approved these changes Feb 17, 2023

View reviewed changes

thomasspriggs removed the do not review label Feb 20, 2023

esteffin requested a review from martin-cs February 20, 2023 11:36

TGWDB approved these changes Feb 21, 2023

View reviewed changes

peterschrammel merged commit 796fb38 into diffblue:develop Feb 28, 2023

NlightNFotis deleted the document_symex_instructions branch February 28, 2023 12:06


		A `goto_modelt` is effectively a product type, consisting of:

		* A list of GOTO functions (pseudocode: `type goto_functionst = list<goto_functiont>`)


		## A (very) short introduction to Symex

		Symex is, at its core, a GOTO-program interpreter. While Symex is interpreting

		@@ -74,8 +74,8 @@ void multi_path_symex_only_checkert::generate_equation()
		{
		const auto symex_start = std::chrono::steady_clock::now();

Document symex instructions #7497

Document symex instructions #7497

Conversation

NlightNFotis commented Jan 23, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Jan 24, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov bot commented Feb 9, 2023 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

esteffin commented Feb 20, 2023

TGWDB commented Feb 27, 2023

NlightNFotis commented Jan 24, 2023 •

edited

Loading

codecov bot commented Feb 9, 2023 •

edited

Loading