Merge branch 'master' into buildfixes

project-everest · Jan 22, 2024 · 3fe0156 · 3fe0156
2 parents 987823e + 36b7b46
commit 3fe0156
Show file tree

Hide file tree

Showing 11 changed files with 60 additions and 55 deletions.
diff --git a/.docker/hierarchic.Dockerfile b/.docker/hierarchic.Dockerfile
@@ -13,8 +13,9 @@ RUN sudo apt-get update && eval $(opam env) && .docker/build/install-other-deps.
 # CI dependencies: sphinx (for the docs)
 # sudo pip3 because of https://bugs.launchpad.net/ubuntu/+source/bash/+bug/1588562
 # jinja2==3.0.0 because of https://github.com/mkdocs/mkdocs/issues/2799
+# alabaster==0.7.13 because of https://alabaster.readthedocs.io/en/latest/changelog.html (0.7.14 breaks old Sphinx versions.)
 RUN sudo apt-get install --yes --no-install-recommends python3-pip python3-setuptools python3-distutils
-RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 sphinx_rtd_theme
+RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 alabaster==0.7.13 sphinx_rtd_theme
 
 # CI proper
 ARG CI_THREADS=24

diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile
@@ -20,8 +20,9 @@ RUN eval $(opam env) && .docker/build/install-deps.sh
 # CI dependencies: sphinx (for the docs)
 # sudo pip3 because of https://bugs.launchpad.net/ubuntu/+source/bash/+bug/1588562
 # jinja2==3.0.0 because of https://github.com/mkdocs/mkdocs/issues/2799
+# alabaster==0.7.13 because of https://alabaster.readthedocs.io/en/latest/changelog.html (0.7.14 breaks old Sphinx versions.)
 RUN sudo apt-get install --yes --no-install-recommends python3-pip python3-setuptools python3-distutils
-RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 sphinx_rtd_theme
+RUN sudo pip3 install sphinx==1.7.2 jinja2==3.0.0 alabaster==0.7.13 sphinx_rtd_theme
 
 # CI proper
 ARG CI_THREADS=24

diff --git a/doc/3d-lang.rst b/doc/3d-lang.rst
@@ -374,8 +374,10 @@ A variation is:
 
 * ``T f[:byte-size-single-element-array-at-most n]``
 
-similar to the previous form, but where ``n`` is an upper bound on the
-size in bytes.
+which describes a field ``f`` that contains a single element of type
+``T`` occupying at most ``n`` bytes, followed by padding bytes to make
+up to ``n`` bytes. This construct thus always consumes exactly ``n``
+bytes.
 
 We expect to add several other kinds of variable-length array-like
 types in the uture.

diff --git a/doc/3d-snapshot/BF.c b/doc/3d-snapshot/BF.c
@@ -96,32 +96,32 @@ ValidateBf2bis(
       /* Validating field z */
       /* Checking that we have enough space for a UINT8, i.e., 1 byte */
       BOOLEAN hasBytes = 1ULL <= (InputLength - positionAfterBitfield11);
-      uint64_t positionAfterBf2bis;
+      uint64_t positionAfterBf2bis1;
       if (hasBytes)
       {
-        positionAfterBf2bis = positionAfterBitfield11 + 1ULL;
+        positionAfterBf2bis1 = positionAfterBitfield11 + 1ULL;
       }
       else
       {
-        positionAfterBf2bis =
+        positionAfterBf2bis1 =
           EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
             positionAfterBitfield11);
       }
       uint64_t res;
-      if (EverParseIsSuccess(positionAfterBf2bis))
+      if (EverParseIsSuccess(positionAfterBf2bis1))
       {
-        res = positionAfterBf2bis;
+        res = positionAfterBf2bis1;
       }
       else
       {
         ErrorHandlerFn("_BF2bis",
           "z",
-          EverParseErrorReasonOfResult(positionAfterBf2bis),
-          EverParseGetValidatorErrorKind(positionAfterBf2bis),
+          EverParseErrorReasonOfResult(positionAfterBf2bis1),
+          EverParseGetValidatorErrorKind(positionAfterBf2bis1),
           Ctxt,
           Input,
           positionAfterBitfield11);
-        res = positionAfterBf2bis;
+        res = positionAfterBf2bis1;
       }
       positionAfterBf2bis0 = res;
     }
@@ -232,32 +232,32 @@ ValidateBf3(
       /* Validating field z */
       /* Checking that we have enough space for a UINT8BE, i.e., 1 byte */
       BOOLEAN hasBytes = 1ULL <= (InputLength - positionAfterBitfield11);
-      uint64_t positionAfterBf3;
+      uint64_t positionAfterBf31;
       if (hasBytes)
       {
-        positionAfterBf3 = positionAfterBitfield11 + 1ULL;
+        positionAfterBf31 = positionAfterBitfield11 + 1ULL;
       }
       else
       {
-        positionAfterBf3 =
+        positionAfterBf31 =
           EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
             positionAfterBitfield11);
       }
       uint64_t res;
-      if (EverParseIsSuccess(positionAfterBf3))
+      if (EverParseIsSuccess(positionAfterBf31))
       {
-        res = positionAfterBf3;
+        res = positionAfterBf31;
       }
       else
       {
         ErrorHandlerFn("_BF3",
           "z",
-          EverParseErrorReasonOfResult(positionAfterBf3),
-          EverParseGetValidatorErrorKind(positionAfterBf3),
+          EverParseErrorReasonOfResult(positionAfterBf31),
+          EverParseGetValidatorErrorKind(positionAfterBf31),
           Ctxt,
           Input,
           positionAfterBitfield11);
-        res = positionAfterBf3;
+        res = positionAfterBf31;
       }
       positionAfterBf30 = res;
     }

diff --git a/doc/3d-snapshot/BoundedSumWhere.c b/doc/3d-snapshot/BoundedSumWhere.c
@@ -90,10 +90,10 @@ BoundedSumWhereValidateBoundedSum(
             EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
               positionAfterleft);
         }
-        uint64_t positionAfterBoundedSum0;
+        uint64_t positionAfterBoundedSum1;
         if (EverParseIsError(positionAfterright_refinement))
         {
-          positionAfterBoundedSum0 = positionAfterright_refinement;
+          positionAfterBoundedSum1 = positionAfterright_refinement;
         }
         else
         {
@@ -103,24 +103,24 @@ BoundedSumWhereValidateBoundedSum(
           BOOLEAN
           right_refinementConstraintIsOk = left <= Bound && right_refinement <= (Bound - left);
           /* end: checking constraint */
-          positionAfterBoundedSum0 =
+          positionAfterBoundedSum1 =
             EverParseCheckConstraintOk(right_refinementConstraintIsOk,
               positionAfterright_refinement);
         }
-        if (EverParseIsSuccess(positionAfterBoundedSum0))
+        if (EverParseIsSuccess(positionAfterBoundedSum1))
         {
-          positionAfterBoundedSum = positionAfterBoundedSum0;
+          positionAfterBoundedSum = positionAfterBoundedSum1;
         }
         else
         {
           ErrorHandlerFn("_boundedSum",
             "right.refinement",
-            EverParseErrorReasonOfResult(positionAfterBoundedSum0),
-            EverParseGetValidatorErrorKind(positionAfterBoundedSum0),
+            EverParseErrorReasonOfResult(positionAfterBoundedSum1),
+            EverParseGetValidatorErrorKind(positionAfterBoundedSum1),
             Ctxt,
             Input,
             positionAfterleft);
-          positionAfterBoundedSum = positionAfterBoundedSum0;
+          positionAfterBoundedSum = positionAfterBoundedSum1;
         }
       }
     }

diff --git a/doc/3d-snapshot/GetFieldPtr.c b/doc/3d-snapshot/GetFieldPtr.c
@@ -47,32 +47,32 @@ GetFieldPtrValidateT(
       {
         /* Checking that we have enough space for a UINT8, i.e., 1 byte */
         BOOLEAN hasBytes = 1ULL <= (truncatedInputLength - position);
-        uint64_t positionAfterT;
+        uint64_t positionAfterT0;
         if (hasBytes)
         {
-          positionAfterT = position + 1ULL;
+          positionAfterT0 = position + 1ULL;
         }
         else
         {
-          positionAfterT =
+          positionAfterT0 =
             EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
               position);
         }
         uint64_t res;
-        if (EverParseIsSuccess(positionAfterT))
+        if (EverParseIsSuccess(positionAfterT0))
         {
-          res = positionAfterT;
+          res = positionAfterT0;
         }
         else
         {
           ErrorHandlerFn("_T",
             "f1.element",
-            EverParseErrorReasonOfResult(positionAfterT),
-            EverParseGetValidatorErrorKind(positionAfterT),
+            EverParseErrorReasonOfResult(positionAfterT0),
+            EverParseGetValidatorErrorKind(positionAfterT0),
             Ctxt,
             truncatedInput,
             position);
-          res = positionAfterT;
+          res = positionAfterT0;
         }
         uint64_t result1 = res;
         result = result1;
@@ -132,32 +132,32 @@ GetFieldPtrValidateT(
       {
         /* Checking that we have enough space for a UINT8, i.e., 1 byte */
         BOOLEAN hasBytes = 1ULL <= (truncatedInputLength - position);
-        uint64_t positionAfterT;
+        uint64_t positionAfterT1;
         if (hasBytes)
         {
-          positionAfterT = position + 1ULL;
+          positionAfterT1 = position + 1ULL;
         }
         else
         {
-          positionAfterT =
+          positionAfterT1 =
             EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
               position);
         }
         uint64_t res;
-        if (EverParseIsSuccess(positionAfterT))
+        if (EverParseIsSuccess(positionAfterT1))
         {
-          res = positionAfterT;
+          res = positionAfterT1;
         }
         else
         {
           ErrorHandlerFn("_T",
             "f2.base.element",
-            EverParseErrorReasonOfResult(positionAfterT),
-            EverParseGetValidatorErrorKind(positionAfterT),
+            EverParseErrorReasonOfResult(positionAfterT1),
+            EverParseGetValidatorErrorKind(positionAfterT1),
             Ctxt,
             truncatedInput,
             position);
-          res = positionAfterT;
+          res = positionAfterT1;
         }
         uint64_t result1 = res;
         result = result1;

diff --git a/doc/3d-snapshot/Triangle2.c b/doc/3d-snapshot/Triangle2.c
@@ -126,27 +126,27 @@ Triangle2ValidateTriangle(
       else
       {
         uint64_t
-        positionAfterTriangle =
+        positionAfterTriangle0 =
           ValidatePoint(Ctxt,
             ErrorHandlerFn,
             truncatedInput,
             truncatedInputLength,
             position);
         uint64_t result1;
-        if (EverParseIsSuccess(positionAfterTriangle))
+        if (EverParseIsSuccess(positionAfterTriangle0))
         {
-          result1 = positionAfterTriangle;
+          result1 = positionAfterTriangle0;
         }
         else
         {
           ErrorHandlerFn("_triangle",
             "corners.element",
-            EverParseErrorReasonOfResult(positionAfterTriangle),
-            EverParseGetValidatorErrorKind(positionAfterTriangle),
+            EverParseErrorReasonOfResult(positionAfterTriangle0),
+            EverParseGetValidatorErrorKind(positionAfterTriangle0),
             Ctxt,
             truncatedInput,
             position);
-          result1 = positionAfterTriangle;
+          result1 = positionAfterTriangle0;
         }
         result = result1;
         ite = EverParseIsError(result1);

diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst
@@ -457,7 +457,7 @@ let field_bitwidth_t = either (with_meta_t int) bitfield_attr
 type array_qualifier =
   | ByteArrayByteSize  //[
   | ArrayByteSize      //[:byte-size
-  | ArrayByteSizeAtMost //[:byte-size-at-most
+  | ArrayByteSizeAtMost //[:byte-size-single-element-array-at-most
   | ArrayByteSizeSingleElementArray //[:byte-size-single-element-array
 
 [@@ PpxDerivingYoJson ]
@@ -1114,11 +1114,11 @@ and print_atomic_field (f:atomic_field) : ML string =
       begin match q with
       | ByteArrayByteSize -> Printf.sprintf "[%s]" (print_expr e)
       | ArrayByteSize -> Printf.sprintf "[:byte-size %s]" (print_expr e)
-      | ArrayByteSizeAtMost -> Printf.sprintf "[:byte-size-at-most %s]" (print_expr e)
+      | ArrayByteSizeAtMost -> Printf.sprintf "[:byte-size-single-element-array-at-most %s]" (print_expr e)
       | ArrayByteSizeSingleElementArray -> Printf.sprintf "[:byte-size-single-element-array %s]" (print_expr e)
       end
     | FieldString None -> Printf.sprintf "[::zeroterm]"
-    | FieldString (Some sz) -> Printf.sprintf "[:zeroterm-b-te-size-at-most %s]" (print_expr sz)
+    | FieldString (Some sz) -> Printf.sprintf "[:zeroterm-byte-size-at-most %s]" (print_expr sz)
     | FieldConsumeAll -> Printf.sprintf "[:consume-all]"
   in
   let sf = f.v in

diff --git a/src/3d/TypeSizes.fst b/src/3d/TypeSizes.fst
@@ -169,7 +169,7 @@ let size_and_alignment_of_atomic_field (env:env_t) (f:atomic_field)
 
       | FieldArrayQualified (n, ByteArrayByteSize) ->
         if base_size <> Fixed 1
-        then warning "Expected a byte array; if the underlying array elements are larger than a byte, use the '[:byte-size' notation"
+        then error "Expected a byte array; if the underlying array elements are larger than a byte, use the '[:byte-size' notation"
                      f.range;
         let n = value_of_const_expr env n in
         begin

diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml
@@ -361,6 +361,7 @@ let krml_args input_stream_binding emit_output_types_defs add_include skip_c_mak
                       "-fparentheses" ::
                         "-fcurly-braces" ::
                           "-fmicrosoft" ::
+                          "-fno-shadow" ::
                             "-header" :: filename_concat ddd_home "noheader.txt" ::
                               "-minimal" ::
                                 "-add-include" :: "\"EverParse.h\"" ::

diff --git a/src/3d/ocaml/lexer.mll b/src/3d/ocaml/lexer.mll
@@ -153,7 +153,7 @@ rule token =
   | "]"                          { locate lexbuf RBRACK }
   | "[="           { deprecation_warning lexbuf "[:byte-size-single-element-array";
                      locate lexbuf LBRACK_EQ }
-  | "[<="          { deprecation_warning lexbuf "[:byte-size-at-most";
+  | "[<="          { deprecation_warning lexbuf "[:byte-size-single-element-array-at-most";
                      locate lexbuf LBRACK_LEQ }
   | "*"            { locate lexbuf STAR }
   | "/"            { locate lexbuf DIV }