v2020.10.23

Changes between v2020.10.01 and Release v2020.10.23

• Support for 3d field alignment padding with aligned (thanks @nikswamy !)
• With -types_from Foo.fst, QuackyDucky can now skip the generation of F* type definitions for "simple" types (leaf types, or struct or tagged unions of simple types), instead taking them from Foo.fst. (Those types must still be defined in the .rfc file, though.)
• Bug fixes for the binary package: do not make 3d symlink krml on Windows, avoid quirks on F* and KReMLin .checked files in their respective standard libraries, recompile HACL* without bzero following hacl-star/hacl-star#365, thanks to help from @msprotz

v2020.10.01

Changes between v2020.09.08 and Release v2020.10.01:

• 3d now produces a standalone EverParse.h when building 3d, so that a user can now concurrently run several instances of 3d with --skip_makefiles. (Each instance will still be sequential, though.) By default, this EverParse.h file is copied to the output directory, but that step can be skipped with --no_copy_everparse_h and the user can directly add the src/3d subdirectory of the EverParse binary package (or source working copy) to their C include path.

• 3d can now compute a hash of the contents of some Example.3d file and the EverParse, F* and KReMLin version numbers and output it into the generated Example.c and Example.h (and *Wrappers*) files as soon as the EVERPARSEHASHES placeholder is present somewhere on its own line in Example.3d.copyright.txt. Then, with --check_inplace_hashes, 3d can read those .c and .h files and skip their generation if hashes match. A variant with --save_hashes and --check_hashes will write and read those hashes in a separate hashes file. These features are using EverCrypt, thanks to integration help by @msprotz.

• Allow casetype on Bool and on integer literals (thanks @nikswamy !)

v2020.09.08

Changes between v2020.08.17 and Release v2020.09.08:

3d

• Revising notations for array types, fixing a bug on computing their sizes (thanks @nikswamy and @aseemr !)
• Move C static assertions to a separate C file (thanks @nikswamy !)

QuackyDucky

• Support for 64-bit unsigned integers (uint64, uint64_le)
• Generate low-level readers and writers for "simple types" (i.e. leaf types, or structs or tagged unions of simple types, inductively)

EverParse/3d v2020.08.17

Changes between v2020.08.07 and Release v2020.08.17

Thanks @nikswamy for these enhancements!

• Support for a default case in casetype
• Produce C static assertions on sizeof; the 3d refining construct tells which are the .h files where to look for the C type definitions

EverParse/3d v2020.08.07

This release is the result of solving #24 .

Changes from v2020.07.22:

• Given a module A.3d, EverParse now generates a separate A.Types.fst to make arith error reporting more user-friendly (#23 ). Thanks @aseemr and @nikswamy !
• EverParse now checks that a .3d file has at least one entrypoint (#20, #25 ). Thanks @aseemr !
• Warnings 7, 8 (static inline), 15 (strings) from the C code generation backend now disappeared. Thanks @msprotz !
• EverParse now generates C++-compatible headers wrapped into extern "C". Thanks @msprotz !
• New operators on integer types: modulus (%), bitwise operators (#26 ). Thanks @nikswamy !
• Multi-line comments. Thanks @nikswamy !
• Additional arguments to the F* verification backend (resp. the KReMLin C code generation backend) can be passed via the EVERPARSE_FSTAR_OPTIONS (resp. EVERPARSE_KREMLIN_OPTIONS) environment variables (#22 for KReMLin).
• Windows binary package: everparse.bat renamed into everparse.cmd
• Branch master has caught up with everparse_3d, so the latter has been removed.

EverParse/3d v2020.07.22

Changes from v2020.06.15:

• overhauled the overloading of integer operators at different bit widths. Now, integer constants without an explicit width specifier are introduced in the smallest integer type that can hold them. Further, all integer expressions are implicitly widened to the needed width depending on the context, e.g., if you have a UINT16 x and a UINT32 y, then when you write x + y this is implicitly elaborated as (UINT32)x + y for an addition in UINT32. Thanks @nikswamy !

EverParse/3d v2020.06.14

This pre-release is the result of merging #15 .

Changes from v2020.05.21:

• The command-line syntax of everparse.bat deeply changed:
  everparse.bat [options] path-to-file1.3d path-to-file2.3d

  • several .3d files can now be provided on the same command line, so that the resulting EverParse.h is common to all.
  • options are now Unix-style instead of Windows-style. The most useful are:
    --help
--odir <output directory> (default is ., the current directory)
    --clang_format
--clang_format_executable <path-to-clang-format.exe>

• Copyright headers are now automatically handled: if EverParse is called with Foo.3d as argument, and if some text file Foo.3d.copyright.txt is present, then the contents of the latter is prepended to the produced Foo.c, Foo.h, FooWrappers.c and FooWrappers.h. This text file can contain any of the following placeholders anywhere:

  • EVERPARSEVERSION to be replaced with the EverParse version tag (here v2020.06.14)
  • FILENAME to be replaced with the name of the file being produced

• A Linux binary package is now available, with an everparse.sh "entrypoint" playing the same role as that of everparse.bat in the Windows release. However, contrary to the Windows package, the Linux package contains no copy of clang-format.

• Official documentation, including the 3d language and the everparse.bat and everparse.sh command line arguments, now at http://project-everest.github.io/everparse , its source (reStructuredText) for this release is at https://github.com/project-everest/everparse/tree/v2020.06.14/doc

EverParse/3d v2020.05.21

Changes from v2020.04.16:

• 3d: validators for arrays of structs of integer fields without constraints or actions now properly extract with optimizations

EverParse/3d v2020.04.16

Changes from EverParse/3d v2020.02.27:

• A formal guarantee of absence of double fetches for 3d validators
• everparse.bat: add a /F option to run clang-format on produced .c/.h files

EverParse/3d v2020.02.27

Changes from EverParse v2020.02.25:

• 3d: add a t field[= size] construct for one t element of exactly size bytes (thanks @nikswamy )
• fixed KReMLin invocation in everparse.bat