DOC-43: Documentation of GOTO model (de)serialisation. #2802

marek-trtik · 2018-08-21T17:23:17Z

No description provided.

tautschnig · 2018-08-21T17:56:21Z

src/goto-programs/README.md

+The content of the written stream will have this strucutre:
+  - The header:
+    - A magic number: byte `0x7f` followed by 3 characters `GBF`.
+    - A version number written in the 7-bit encoding. Currently, only version `4` is supported.


Could a link explaining "7-bit encoding" be provided? It's used a lot below.

tautschnig · 2018-08-21T17:57:00Z

src/goto-programs/README.md

+      - The string `s.mode`.
+      - The string `s.pretty_name`.
+      - The number `0` in the 7-bit encoding.
+      - The flags word in the 7-bit encoding. The bits in the flags word correspond to the following `bool` fields (from the most significant bit):


I'd use "Boolean" instead of "bool".

tautschnig · 2018-08-21T17:57:30Z

src/goto-programs/README.md

+    - The array of individual function with bodies. Each written function has this structure:
+      - The string with the name of the function.
+      - The number of instructions in the body of the function in the 7-bit encoding.
+      - The array of individual instruction in function's body. Each written instruction `I` has this structure:


individual instruction_s_

tautschnig · 2018-08-21T17:58:58Z

src/goto-programs/README.md

+
+An important propery of the serialisation is that each serialised `irept`
+instance occurs in the stream exactly once. Namely, in the position of
+its first serialisation query. All other such queries save only hash


only a hash

tautschnig · 2018-08-21T18:00:32Z

src/goto-programs/README.md

+the [previous subsection](\ref subsection-goto-binary-serialisation).
+The process of the deserialisation does not involve any seeking in the file.
+The content is read linearly from the beginning to the end. `irept` instances
+and their string constats are deserialised into the memory only once at their


s/constats/constants/

tautschnig · 2018-08-21T18:00:48Z

src/goto-programs/README.md

+The process of the deserialisation does not involve any seeking in the file.
+The content is read linearly from the beginning to the end. `irept` instances
+and their string constats are deserialised into the memory only once at their
+first occurreces in the stream. All subsequent deserialisation queries are


s/occurreces/occurrence/

tautschnig · 2018-08-21T18:02:09Z

src/goto-programs/README.md

+  - `elf_reader.h`
+  - `elf_reader.cpp`
+
+\subsubsection subsection-goto-binary-deserialisation-from-mac-o-fat-image Deserialisation from Mac-O fat image


It's "mach-o", not "mac-o" (multiple instances below as well)

tautschnig · 2018-08-21T18:04:09Z

src/util/README.md

+\subsubsection irep-serialization-numbers Serialization of Numbers
+
+A number is serialiased in 7-bit encoding. For example. given a 2-byte
+number in base 2, like `10101010 01010101`, then it is save in 3 bytes,


is is save_d_

tautschnig · 2018-08-21T18:04:40Z

src/util/README.md

+number in base 2, like `10101010 01010101`, then it is save in 3 bytes,
+where each byte takes only 7 bits from the number, reading from the
+left. The 8th bit in each output byte is set to 1 except in the last
+byte, where the bit is 0. That 0 bit indicates the end of the end


duplicate "the end"

peterschrammel · 2018-08-21T22:17:51Z

src/goto-programs/README.md

@@ -377,3 +377,181 @@ This stage concludes the *analysis-independent* program transformations.
 \subsubsection goto-program-example-1-section Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; }

 To be documented.
+
+
+\section section-goto-binary Binary Represenration


Representation

peterschrammel · 2018-08-21T22:18:33Z

src/goto-programs/README.md

+
+To serialise a `goto_modelt` instance `gm` to a stream `ostr` call the function `write_goto_binary`, e.g. `write_goto_binary(ostr, gm)`.
+
+The content of the written stream will have this strucutre:


peterschrammel · 2018-08-21T22:21:15Z

src/goto-programs/README.md

+its first serialisation query. All other such queries save only hash
+code (i.e. reference) of the `irept` instance.
+
+The similar strategy is used for serialisation of string constants


peterschrammel · 2018-08-21T22:21:42Z

src/goto-programs/README.md

+The similar strategy is used for serialisation of string constants
+shared amongst `irept` instances. Such a string is fully saved only in
+the first serialisation query of an `irept` instance it appears in and
+all other queries only save its integer has code.


peterschrammel · 2018-08-21T22:22:07Z

src/goto-programs/README.md

+  - `read_bin_goto_object.h`
+  - `read_bin_goto_object.cpp`
+
+First two modules are responsible for location of the stream with the


The first two

peterschrammel · 2018-08-21T22:22:27Z

src/goto-programs/README.md

+
+First two modules are responsible for location of the stream with the
+serialised data within a passed file. And the remaining two modules
+perform the actual deserialisation of `goto_modelt` instance from


peterschrammel · 2018-08-21T22:24:32Z

src/goto-programs/README.md

+\subsubsection subsection-goto-binary-is-binary-file Checking file type
+
+You can use function `is_goto_binary` to check whether a passed file contains
+a sederialised `goto_modelt` instance or not. This is done by checking the


deserialised

peterschrammel · 2018-08-21T22:26:14Z

src/util/README.md

+characters `0` and `\\` are escaped by writing additional `\\` 
+before them. 
+
+This is implmented in the function `write_gb_string` and the


Prefix function with class name so that it is linked by doxygen

marek-trtik · 2018-08-22T10:10:22Z

Requested updates are available.

peterschrammel · 2018-08-30T08:18:17Z

@marek-trtik, please rebase.

marek-trtik · 2018-08-31T15:52:05Z

@peterschrammel Done.

tautschnig · 2018-09-03T14:02:54Z

@marek-trtik Would you mind squashing your commits? Then this one should be ready to be merged.

marek-trtik · 2018-09-05T09:26:11Z

@tautschnig Done.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 6cd614b).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

marek-trtik added the documentation label Aug 21, 2018

marek-trtik self-assigned this Aug 21, 2018

marek-trtik requested review from peterschrammel and danpoe August 21, 2018 17:23

marek-trtik requested review from kroening, pkesseli, smowton and tautschnig as code owners August 21, 2018 17:23

tautschnig reviewed Aug 21, 2018

View reviewed changes

peterschrammel reviewed Aug 21, 2018

View reviewed changes

peterschrammel approved these changes Aug 30, 2018

View reviewed changes

marek-trtik force-pushed the doc_add_goto_binary branch from 988e26c to b25bdfe Compare August 31, 2018 15:50

Documentation of GOTO model (de)serialisation.

6cd614b

marek-trtik force-pushed the doc_add_goto_binary branch from b25bdfe to 6cd614b Compare September 5, 2018 09:25

allredj reviewed Sep 5, 2018

View reviewed changes

tautschnig merged commit a6d2e2a into diffblue:develop Sep 5, 2018


		To serialise a `goto_modelt` instance `gm` to a stream `ostr` call the function `write_goto_binary`, e.g. `write_goto_binary(ostr, gm)`.

		The content of the written stream will have this strucutre:

DOC-43: Documentation of GOTO model (de)serialisation. #2802

DOC-43: Documentation of GOTO model (de)serialisation. #2802

Uh oh!

Conversation

marek-trtik commented Aug 21, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

marek-trtik commented Aug 22, 2018

Uh oh!

peterschrammel commented Aug 30, 2018

Uh oh!

marek-trtik commented Aug 31, 2018

Uh oh!

tautschnig commented Sep 3, 2018

Uh oh!

marek-trtik commented Sep 5, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!