Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Anonymous structs and case types and compile-time flags #85

Merged
merged 15 commits into from
Nov 4, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions doc/3d-lang.rst
Original file line number Diff line number Diff line change
Expand Up @@ -508,6 +508,60 @@ Restrictions

* Actions cannot be associated with bit fields.

Generating code with for several compile-time configurations
------------------------------------------------------------

Sometimes one wants to write a single format specification to
accommodate several compile-time configurations, e.g., to support
multiple architectures. 3D offers some limited support for decorating
a specification with compile-time conditionals familiar to C
programmmers, e.g., ``#if`` and ``#else``, and to generate C code
while preserving these C preprocessor directives.

For example, the listing below shows an integer type that can either
be represented using 64 bits (if ``ARCH64`` is true) or 32 bits.

.. literalinclude:: PointArch_32_64.3d
:language: c

To compile such a file using 3D, we also need to provide a
``.3d.config`` file that declares all the compile-time flags used in
the specification and mentions a C header file in which to find
definitions for those flags. Here is a sample config file:

.. literalinclude:: Arch.3d.config

Then, one can invoke ``3d.exe --config Arch.3d.config
PointArch_32_64.3d --batch``, which produces the following C code as
output.

In the header file ``PointArch_32_64.h``, we see an include for
the header file mentioned in the config:

.. code-block:: c

#include "arch_flags.h"

In the generated C file, ``PointArch_32_64.c``, we see the code below,
with the suitable preprocessor directives protecting the two variants
of the the ``Int`` type declared in the source 3d file.

.. code-block:: c

static inline uint64_t
ValidateInt(...) {
{
#if ARCH64
/* Validating field x */
/* Checking that we have enough space for a UINT64, i.e., 8 bytes */
...
#else
/* Validating field x */
/* Checking that we have enough space for a UINT32, i.e., 4 bytes */
...
#endif
}

Checking 3d types for correspondence with existing C types
----------------------------------------------------------

Expand Down
141 changes: 141 additions & 0 deletions doc/3d-snapshot/PointArch_32_64.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,141 @@


#include "PointArch_32_64.h"



static inline uint64_t
ValidateInt(
uint8_t *Ctxt,
void
(*Err)(
EverParseString x0,
EverParseString x1,
EverParseString x2,
uint64_t x3,
uint8_t *x4,
uint8_t *x5,
uint64_t x6
),
uint8_t *Input,
uint64_t InputLen,
uint64_t StartPosition
)
{
#if ARCH64
{
/* Validating field x */
/* Checking that we have enough space for a UINT64, i.e., 8 bytes */
BOOLEAN hasBytes = (uint64_t)8U <= (InputLen - StartPosition);
uint64_t positionAfterInt;
if (hasBytes)
{
positionAfterInt = StartPosition + (uint64_t)8U;
}
else
{
positionAfterInt =
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
StartPosition);
}
if (EverParseIsSuccess(positionAfterInt))
{
return positionAfterInt;
}
Err("_INT",
"x",
EverParseErrorReasonOfResult(positionAfterInt),
EverParseGetValidatorErrorKind(positionAfterInt),
Ctxt,
Input,
StartPosition);
return positionAfterInt;
}
#else
{
/* Validating field x */
/* Checking that we have enough space for a UINT32, i.e., 4 bytes */
BOOLEAN hasBytes = (uint64_t)4U <= (InputLen - StartPosition);
uint64_t positionAfterInt;
if (hasBytes)
{
positionAfterInt = StartPosition + (uint64_t)4U;
}
else
{
positionAfterInt =
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
StartPosition);
}
if (EverParseIsSuccess(positionAfterInt))
{
return positionAfterInt;
}
Err("_INT",
"x",
EverParseErrorReasonOfResult(positionAfterInt),
EverParseGetValidatorErrorKind(positionAfterInt),
Ctxt,
Input,
StartPosition);
return positionAfterInt;
}
#endif
}

uint64_t
PointArch3264ValidatePoint(
uint8_t *Ctxt,
void
(*Err)(
EverParseString x0,
EverParseString x1,
EverParseString x2,
uint64_t x3,
uint8_t *x4,
uint8_t *x5,
uint64_t x6
),
uint8_t *Input,
uint64_t InputLength,
uint64_t StartPosition
)
{
/* Validating field x */
uint64_t positionAfterPoint = ValidateInt(Ctxt, Err, Input, InputLength, StartPosition);
uint64_t positionAfterx;
if (EverParseIsSuccess(positionAfterPoint))
{
positionAfterx = positionAfterPoint;
}
else
{
Err("_POINT",
"x",
EverParseErrorReasonOfResult(positionAfterPoint),
EverParseGetValidatorErrorKind(positionAfterPoint),
Ctxt,
Input,
StartPosition);
positionAfterx = positionAfterPoint;
}
if (EverParseIsError(positionAfterx))
{
return positionAfterx;
}
/* Validating field y */
uint64_t positionAfterPoint0 = ValidateInt(Ctxt, Err, Input, InputLength, positionAfterx);
if (EverParseIsSuccess(positionAfterPoint0))
{
return positionAfterPoint0;
}
Err("_POINT",
"y",
EverParseErrorReasonOfResult(positionAfterPoint0),
EverParseGetValidatorErrorKind(positionAfterPoint0),
Ctxt,
Input,
positionAfterx);
return positionAfterPoint0;
}

39 changes: 39 additions & 0 deletions doc/3d-snapshot/PointArch_32_64.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@


#ifndef __PointArch_32_64_H
#define __PointArch_32_64_H

#if defined(__cplusplus)
extern "C" {
#endif





#include "arch_flags.h"
#include "EverParse.h"
uint64_t
PointArch3264ValidatePoint(
uint8_t *Ctxt,
void
(*Err)(
EverParseString x0,
EverParseString x1,
EverParseString x2,
uint64_t x3,
uint8_t *x4,
uint8_t *x5,
uint64_t x6
),
uint8_t *Input,
uint64_t InputLength,
uint64_t StartPosition
);

#if defined(__cplusplus)
}
#endif

#define __PointArch_32_64_H_DEFINED
#endif
41 changes: 41 additions & 0 deletions doc/3d-snapshot/PointArch_32_64Wrapper.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
#include "PointArch_32_64Wrapper.h"
#include "EverParse.h"
#include "PointArch_32_64.h"
void PointArch_32_64EverParseError(const char *StructName, const char *FieldName, const char *Reason);

static
void DefaultErrorHandler(
const char *typename_s,
const char *fieldname,
const char *reason,
uint64_t error_code,
uint8_t *context,
EverParseInputBuffer input,
uint64_t start_pos)
{
EverParseErrorFrame *frame = (EverParseErrorFrame*)context;
EverParseDefaultErrorHandler(
typename_s,
fieldname,
reason,
error_code,
frame,
input,
start_pos
);
}

BOOLEAN PointArch3264CheckPoint(uint8_t *base, uint32_t len) {
EverParseErrorFrame frame;
frame.filled = FALSE;
uint64_t result = PointArch3264ValidatePoint( (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0);
if (EverParseIsError(result))
{
if (frame.filled)
{
PointArch_32_64EverParseError(frame.typename_s, frame.fieldname, frame.reason);
}
return FALSE;
}
return TRUE;
}
16 changes: 16 additions & 0 deletions doc/3d-snapshot/PointArch_32_64Wrapper.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
#include "EverParseEndianness.h"
#define EVERPARSE_ERROR_GENERIC 1uL
#define EVERPARSE_ERROR_NOT_ENOUGH_DATA 2uL
#define EVERPARSE_ERROR_IMPOSSIBLE 3uL
#define EVERPARSE_ERROR_LIST_SIZE_NOT_MULTIPLE 4uL
#define EVERPARSE_ERROR_ACTION_FAILED 5uL
#define EVERPARSE_ERROR_CONSTRAINT_FAILED 6uL
#define EVERPARSE_ERROR_UNEXPECTED_PADDING 7uL

#ifdef __cplusplus
extern "C" {
#endif
BOOLEAN PointArch3264CheckPoint(uint8_t *base, uint32_t len);
#ifdef __cplusplus
}
#endif
8 changes: 4 additions & 4 deletions doc/3d-snapshot/TaggedUnion.c
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ ValidateIntPayload(
return positionAfterIntPayload;
}
Err("_int_payload",
"missing",
"value8",
EverParseErrorReasonOfResult(positionAfterIntPayload),
EverParseGetValidatorErrorKind(positionAfterIntPayload),
Ctxt,
Expand Down Expand Up @@ -73,7 +73,7 @@ ValidateIntPayload(
return positionAfterIntPayload;
}
Err("_int_payload",
"missing",
"value16",
EverParseErrorReasonOfResult(positionAfterIntPayload),
EverParseGetValidatorErrorKind(positionAfterIntPayload),
Ctxt,
Expand Down Expand Up @@ -102,7 +102,7 @@ ValidateIntPayload(
return positionAfterIntPayload;
}
Err("_int_payload",
"missing",
"value32",
EverParseErrorReasonOfResult(positionAfterIntPayload),
EverParseGetValidatorErrorKind(positionAfterIntPayload),
Ctxt,
Expand All @@ -119,7 +119,7 @@ ValidateIntPayload(
return positionAfterIntPayload;
}
Err("_int_payload",
"missing",
"_x_2",
EverParseErrorReasonOfResult(positionAfterIntPayload),
EverParseGetValidatorErrorKind(positionAfterIntPayload),
Ctxt,
Expand Down
6 changes: 6 additions & 0 deletions doc/Arch.3d.config
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{ "compile_time_flags":
{
"flags":["ARCH64"],
"include_file":"arch_flags.h"
}
}
2 changes: 1 addition & 1 deletion doc/BF.3d
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
typedef struct _BF {
UINT32 x : 6;
UINT32 y : 10 { y <= 900 };
UINT32 z : 16 { y + z <= 60000 }
UINT32 z : 16 { y + z <= 60000 };
} BF;
// SNIPPET_END: BF

Expand Down
8 changes: 6 additions & 2 deletions doc/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@ export KRML_HOME?=$(realpath $(EVERPARSE_HOME)/../karamel)

3D=$(EVERPARSE_HOME)/bin/3d.exe
3D_EXCLUDE=ConstColor.3d
3D_FILES=$(filter-out $(3D_EXCLUDE),$(wildcard *.3d))
3D_MODULES=$(basename $(3D_FILES))
3D_CONFIG=Arch.3d.config
3D_FILES_WITH_CONFIG=PointArch_32_64.3d
3D_FILES=$(filter-out $(3D_EXCLUDE) $(3D_FILES_WITH_CONFIG),$(wildcard *.3d))
3D_MODULES=$(basename $(3D_FILES) $(3D_FILES_WITH_CONFIG))
3D_MODULES_AND_WRAPPERS=$(3D_MODULES) $(addsuffix Wrapper,$(3D_MODULES))
3D_C_AND_H_FILES=$(filter-out BaseWrapper.c BaseWrapper.h,$(addsuffix .c,$(3D_MODULES_AND_WRAPPERS)) $(addsuffix .h,$(3D_MODULES_AND_WRAPPERS)))
3D_DIFF=$(addsuffix .diff,$(3D_C_AND_H_FILES))
Expand Down Expand Up @@ -43,12 +45,14 @@ help:
3d-do-tests:
mkdir -p out
$(3D) --odir out --batch $(3D_FILES)
$(3D) --odir out --batch $(3D_FILES_WITH_CONFIG) --config $(3D_CONFIG)
cp $(AUX_HEADERS) out
+$(MAKE) -C out -f Makefile.basic USER_TARGET=test USER_CFLAGS='-Wno-ignored-qualifiers' test

3d-do-interpreter-tests:
mkdir -p interpret.out
$(3D) --odir interpret.out --batch $(3D_FILES) --interpret
$(3D) --odir interpret.out --batch $(3D_FILES_WITH_CONFIG) --config $(3D_CONFIG) --interpret
cp $(AUX_HEADERS) interpret.out
+$(MAKE) -C interpret.out -f Makefile.basic USER_TARGET=test USER_CFLAGS='-Wno-ignored-qualifiers' test

Expand Down
14 changes: 14 additions & 0 deletions doc/PointArch_32_64.3d
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
typedef struct _INT {
#if ARCH64
UINT64 x;
#else
UINT32 x;
#endif
} INT;


entrypoint
typedef struct _POINT {
INT x;
INT y;
} POINT;
1 change: 1 addition & 0 deletions doc/out/arch_flags.h
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
#define ARCH64 1
Loading