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

nikswamy · 2022-10-04T22:00:49Z

Summary

We now support anonymous nested structs and case types. Previously, all such types had to be named at the top level.
You can use a #if to enforce some constraints based on compile-time boolean expressions in the constraint associated with a field.
You can also use #if to selectively add fields to a type, with some restrictions explained in the detailed section later in this email.

The generated code preserves those #if expressions, so that the C code can be compiled for multiple compile-time configurations.

Limitations

Since we are generating C code that contains the #if (since the goal is to be able to generate C code for multiple compile-time configurations at once from a single 3d specification), we are NOT using a preprocessor to just evaluate the #if terms away at the 3D level. This means, unlike C, you cannot use #if everywhere to syntactically preprocess terms (e.g., conditionally adding a function argument, renaming a type, etc.)

Note also, due to FStarLang/karamel#293 some examples do not yet produce compilable C code. See, tests/ifdefs/src/AnonNestedStructIfDefs.3d, which produces C code, but the compilation to produce a .o is currently excluded from the regression suite until the krml bug is fixed.

How it works

A config file

Associated with 3d project (which may consist of multiple 3d files), we associate a new JSON formatted .3d.config file.

See tests/ifdefs/src/CompileTimeIfFlags.3d.config, for an example, reproduced here:

{ "compile_time_flags":
    {
      "flags":["ABOVE_DIAGONAL","STRICT","DIM3","DIM4"],
      "include_file":"compile_time_flags.h"
    }
}

It contains a key called compile_time_flags whose value contains:

The names of all the flags used in the project in a field called "flags"
The name of an .h file that provides definitions for all those flags, e.g., "compile_time_flags.h"

Based on these configuration options, 3d will

Check that if you are writing #if F1 && F2, that all the variables mentioned in F1 && F2 are recorded in the config file. The flags field of the config is a clear contract between 3d and include file (compile_time_flags.h), meaning that if definitions for all the flags variables are provided, then we guarantee that the code produced by 3d should be compilable for all values of those flags.
When 3d generates code, in every C file it produces, it will also inject the following directive in its corresponding .h file:

#include "compile_time_flags.h"

It is then responsibility of the user to actually provide compile_time_flags.h, making sure that it is available on the include path, and that it provides definitions for all the flags.

It also provides the user with the flexibility to define those flags however they please, e.g., using complex macro expressions, referencing other header files, etc.

In a typical usage, one could:

define a new flag , recording it in the .3d.config file
make changes to the 3d file, delimiting your changes within #if conditionals
generate C code that retains those #if conditionals,
provide a definition for your new flag in the include file mentioned in the config file, e.g., compile_time_flags.h
compile the code as usual

Some more details

##. #if in constraints

In the constraint associated with a field, you can use a #if to enforce some constraints based on compile-time boolean expressions:

For example, you can write:

typedef struct _PointConditional {
  UINT32 x;
  UINT32 y
  {
    #if (ABOVE_DIAGONAL && STRICT)
        x < y
    #elif ABOVE_DIAGONAL
        x <= y
    #else
        true
    #endif
  };
} PointConditional;

This produces the following C code fragment for validating the y field:

    /* reading field_value */
    uint32_t y_refinement = Load32Le(Input + (uint32_t)positionAfterx);
    /* start: checking constraint */
    BOOLEAN y_refinementConstraintIsOk;
    #if ABOVE_DIAGONAL && STRICT
    y_refinementConstraintIsOk = x < y_refinement;
    #elif ABOVE_DIAGONAL
    y_refinementConstraintIsOk = x <= y_refinement;
    #else
    y_refinementConstraintIsOk = TRUE;
    #endif
    /* end: checking constraint */

`#if` in the fields of a type

You can also use #if to selectively add fields to a type, based on some compile-time boolean expressions.

For example:

typedef struct _StaticConditionalPoint {
     UINT32 d1;
     UINT32 d2;
  #if (DIM3 || DIM4)
     UINT32 d3;
  #endif
  #if DIM4
     UINT32 d4;
  #endif
} StaticConditionalPoint;

Which produces C code of the following shape:

  #if DIM3 || DIM4
  /* Validating field d3 */
  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
  BOOLEAN hasBytes = (uint64_t)4U <= (InputLength - positionAfterd2);
  ...
  #endif

  #if DIM4
  /* Validating field d4 */
  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
  BOOLEAN hasBytes = (uint64_t)4U <= (InputLength - positionAfterX4);
  ...
  #endif

Note, dependence between the branches of a #if is not allowed. For example, you cannot write

typedef struct _StaticConditionalPoint {
     UINT32 d1;
     UINT32 d2;
  #if (DIM3 || DIM4)
     UINT32 d3;
  #endif
  #if DIM4
     UINT32 d4
     { d3 <= d4 }; // <---- d3 is not available for use here!
  #endif
} StaticConditionalPoint;

If you must have dependence between the fields, then you need to distribute the fields between the branches,
For example, this is legal:

typedef struct _StaticConditionalPoint {
     UINT32 d1;
     UINT32 d2;
  #if DIM3
     UINT32 d3;
  #elif DIM4
     UINT32 d3;
     UINT32 d4
     { d3 <= d4 }; //Now you can refer to d3 in the constraint on d4
  #endif
} StaticConditionalPoint;

…ith both makefile and batch mode support

… fix grouping of fields; fix expected output in one case

nikswamy · 2022-10-05T21:23:04Z

FYI, as part of the generalization of the syntax to support nested structs and unions, I fixed the syntax to insist on every field declaration in a struct concluding with a semi-colon. This is in keeping with C syntax, whereas previously we would allow things like { int f; int g} without the semicolon after g. This syntax fix necessitated changes in a few examples.

…NY in a Makefile

nikswamy · 2022-11-03T23:16:34Z

src/3d/Ast.fst

+and field' =
+  | AtomicField of atomic_field
+  | RecordField : record -> ident -> field'
+  | SwitchCaseField : switch_case -> ident -> field'


This is one of the main changes in the PR.
A field is no longer just an atomic field. It can be a composite field too, enabled nested structs (RecordField) and unions (SwitchCaseField)

nikswamy · 2022-11-03T23:19:38Z

src/3d/BitFields.fst

+        match field.v with
+        | RecordField _ _
+        | SwitchCaseField _ _ ->
+          Inl (rewrite_composite_field field) :: out


recurse to rewrite_field, to group bitfields within the record or union

nikswamy · 2022-11-03T23:20:32Z

src/3d/BitFields.fst

+              then Inr(index, typ, af :: atomic_fields) :: tl //extend this bitfield group
+              else Inr(bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group
+
+            | _ -> Inr (bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group


The behavior on atomic fields is the same as before

nikswamy · 2022-11-03T23:22:37Z

src/3d/Deps.fst

+
+let get_config () = 
+  match !parsed_config with
+  | Some c -> Some c


parse the config once and memoize it

nikswamy · 2022-11-03T23:25:22Z

src/3d/Desugar.fst

+    | This -> error "'this' is not allowed in the guard of an #if" e.range
+    | Static _ -> failwith "static should have been eliminated already"
+    | Constant _ -> ()
+    | Identifier i ->


ensures that all variables in a #if are declared as compile-time flags in the config

nikswamy added 9 commits August 12, 2022 23:18

basic support for #if/#else in expressions

d2d144d

boolean expressions in #if

40431f5

code complete on anonymous structs and case types, arbitrarily nested

4ae7cb9

support for anonymous structs, case types, and #if fields

6bd1150

support for #elif

2c458dd

Merge remote-tracking branch 'origin/master' into nik_ifdef

d999384

parsing a JSON-formatted config file

5b28218

Merge remote-tracking branch 'origin/master' into nik_ifdef

76ac456

support for compile-time flags specified in a separate config file, w…

b6235c1

…ith both makefile and batch mode support

nikswamy requested review from tahina-pro and aseemr October 4, 2022 22:01

fix up syntax of some examples that miss semicolons on struct fields;…

edc712d

… fix grouping of fields; fix expected output in one case

nikswamy added 5 commits October 8, 2022 04:48

fixing up an ugly typo that was not caught by CI due to a missing PHO…

4bc815b

…NY in a Makefile

updating documentation to include #if and config files

57694a6

Merge remote-tracking branch 'origin/master' into nik_ifdef

69706ca

enable ifdef C compiler test and krml bug fix; update snapshot

10f19bf

remove spurious make target

80a4185

nikswamy commented Nov 3, 2022

View reviewed changes

src/3d/Deps.fst

let get_config () =

match !parsed_config with

| Some c -> Some c

Copy link

Contributor Author

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

parse the config once and memoize it

nikswamy commented Nov 3, 2022

View reviewed changes

tahina-pro merged commit 4ee7762 into master Nov 4, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

nikswamy commented Oct 4, 2022

nikswamy commented Oct 5, 2022

nikswamy Nov 3, 2022

nikswamy Nov 3, 2022

nikswamy Nov 3, 2022

nikswamy Nov 3, 2022

nikswamy Nov 3, 2022

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

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

Conversation

nikswamy commented Oct 4, 2022

Summary

Limitations

How it works

A config file

Some more details

#if in the fields of a type

nikswamy commented Oct 5, 2022

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

nikswamy Nov 3, 2022

Choose a reason for hiding this comment

`#if` in the fields of a type