From b6f0dc95e7039cb0fdad8b6a5a0ba30982204a59 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Oct 2024 17:55:00 -0700 Subject: [PATCH] fixing #125; avoid generating loops to check arrays whose elements are unconstrained --- doc/3d-snapshot/GetFieldPtr.c | 130 ++----------------- doc/3d-snapshot/Triangle2.c | 139 +-------------------- src/3d/InterpreterTarget.fst | 35 +++++- src/3d/prelude/EverParse3d.Interpreter.fst | 16 +-- 4 files changed, 61 insertions(+), 259 deletions(-) diff --git a/doc/3d-snapshot/GetFieldPtr.c b/doc/3d-snapshot/GetFieldPtr.c index 4a9d8484e..a27ce647f 100644 --- a/doc/3d-snapshot/GetFieldPtr.c +++ b/doc/3d-snapshot/GetFieldPtr.c @@ -22,70 +22,17 @@ GetFieldPtrValidateT( ) { /* Validating field f1 */ - BOOLEAN hasEnoughBytes0 = (uint64_t)(uint32_t)10U <= (InputLength - StartPosition); - uint64_t positionAfterT; - if (!hasEnoughBytes0) + BOOLEAN hasBytes0 = (uint64_t)10U <= (InputLength - StartPosition); + uint64_t res0; + if (hasBytes0) { - positionAfterT = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - StartPosition); + res0 = StartPosition + (uint64_t)10U; } else { - uint8_t *truncatedInput = Input; - uint64_t truncatedInputLength = StartPosition + (uint64_t)(uint32_t)10U; - uint64_t result = StartPosition; - while (TRUE) - { - uint64_t position = result; - BOOLEAN ite; - if (!(1ULL <= (truncatedInputLength - position))) - { - ite = TRUE; - } - else - { - /* Checking that we have enough space for a UINT8, i.e., 1 byte */ - BOOLEAN hasBytes = 1ULL <= (truncatedInputLength - position); - uint64_t positionAfterT0; - if (hasBytes) - { - positionAfterT0 = position + 1ULL; - } - else - { - positionAfterT0 = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - position); - } - uint64_t res; - if (EverParseIsSuccess(positionAfterT0)) - { - res = positionAfterT0; - } - else - { - ErrorHandlerFn("_T", - "f1.element", - EverParseErrorReasonOfResult(positionAfterT0), - EverParseGetValidatorErrorKind(positionAfterT0), - Ctxt, - truncatedInput, - position); - res = positionAfterT0; - } - uint64_t result1 = res; - result = result1; - ite = EverParseIsError(result1); - } - if (ite) - { - break; - } - } - uint64_t res = result; - positionAfterT = res; + res0 = EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); } + uint64_t positionAfterT = res0; uint64_t positionAfterf1; if (EverParseIsSuccess(positionAfterT)) { @@ -107,70 +54,17 @@ GetFieldPtrValidateT( return positionAfterf1; } /* Validating field f2 */ - BOOLEAN hasEnoughBytes = (uint64_t)(uint32_t)20U <= (InputLength - positionAfterf1); - uint64_t positionAfterT0; - if (!hasEnoughBytes) + BOOLEAN hasBytes = (uint64_t)20U <= (InputLength - positionAfterf1); + uint64_t res; + if (hasBytes) { - positionAfterT0 = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - positionAfterf1); + res = positionAfterf1 + (uint64_t)20U; } else { - uint8_t *truncatedInput = Input; - uint64_t truncatedInputLength = positionAfterf1 + (uint64_t)(uint32_t)20U; - uint64_t result = positionAfterf1; - while (TRUE) - { - uint64_t position = result; - BOOLEAN ite; - if (!(1ULL <= (truncatedInputLength - position))) - { - ite = TRUE; - } - else - { - /* Checking that we have enough space for a UINT8, i.e., 1 byte */ - BOOLEAN hasBytes = 1ULL <= (truncatedInputLength - position); - uint64_t positionAfterT1; - if (hasBytes) - { - positionAfterT1 = position + 1ULL; - } - else - { - positionAfterT1 = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - position); - } - uint64_t res; - if (EverParseIsSuccess(positionAfterT1)) - { - res = positionAfterT1; - } - else - { - ErrorHandlerFn("_T", - "f2.base.element", - EverParseErrorReasonOfResult(positionAfterT1), - EverParseGetValidatorErrorKind(positionAfterT1), - Ctxt, - truncatedInput, - position); - res = positionAfterT1; - } - uint64_t result1 = res; - result = result1; - ite = EverParseIsError(result1); - } - if (ite) - { - break; - } - } - uint64_t res = result; - positionAfterT0 = res; + res = EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, positionAfterf1); } + uint64_t positionAfterT0 = res; uint64_t positionAfterf2; if (EverParseIsSuccess(positionAfterT0)) { diff --git a/doc/3d-snapshot/Triangle2.c b/doc/3d-snapshot/Triangle2.c index 3a60a2855..7425f375b 100644 --- a/doc/3d-snapshot/Triangle2.c +++ b/doc/3d-snapshot/Triangle2.c @@ -2,87 +2,6 @@ #include "Triangle2.h" -static inline uint64_t -ValidatePoint( - uint8_t *Ctxt, - void - (*ErrorHandlerFn)( - EVERPARSE_STRING x0, - EVERPARSE_STRING x1, - EVERPARSE_STRING 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 */ - /* Checking that we have enough space for a UINT16, i.e., 2 bytes */ - BOOLEAN hasBytes0 = 2ULL <= (InputLength - StartPosition); - uint64_t positionAfterPoint; - if (hasBytes0) - { - positionAfterPoint = StartPosition + 2ULL; - } - else - { - positionAfterPoint = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - StartPosition); - } - uint64_t res; - if (EverParseIsSuccess(positionAfterPoint)) - { - res = positionAfterPoint; - } - else - { - ErrorHandlerFn("_point", - "x", - EverParseErrorReasonOfResult(positionAfterPoint), - EverParseGetValidatorErrorKind(positionAfterPoint), - Ctxt, - Input, - StartPosition); - res = positionAfterPoint; - } - uint64_t positionAfterx = res; - if (EverParseIsError(positionAfterx)) - { - return positionAfterx; - } - /* Validating field y */ - /* Checking that we have enough space for a UINT16, i.e., 2 bytes */ - BOOLEAN hasBytes = 2ULL <= (InputLength - positionAfterx); - uint64_t positionAfterPoint0; - if (hasBytes) - { - positionAfterPoint0 = positionAfterx + 2ULL; - } - else - { - positionAfterPoint0 = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - positionAfterx); - } - if (EverParseIsSuccess(positionAfterPoint0)) - { - return positionAfterPoint0; - } - ErrorHandlerFn("_point", - "y", - EverParseErrorReasonOfResult(positionAfterPoint0), - EverParseGetValidatorErrorKind(positionAfterPoint0), - Ctxt, - Input, - positionAfterx); - return positionAfterPoint0; -} - uint64_t Triangle2ValidateTriangle( uint8_t *Ctxt, @@ -102,63 +21,17 @@ Triangle2ValidateTriangle( ) { /* Validating field corners */ - BOOLEAN hasEnoughBytes = (uint64_t)(4U * (uint32_t)3U) <= (InputLength - StartPosition); - uint64_t positionAfterTriangle; - if (!hasEnoughBytes) + BOOLEAN hasBytes = (uint64_t)12U <= (InputLength - StartPosition); + uint64_t res; + if (hasBytes) { - positionAfterTriangle = - EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, - StartPosition); + res = StartPosition + (uint64_t)12U; } else { - uint8_t *truncatedInput = Input; - uint64_t truncatedInputLength = StartPosition + (uint64_t)(4U * (uint32_t)3U); - uint64_t result = StartPosition; - while (TRUE) - { - uint64_t position = result; - BOOLEAN ite; - if (!(1ULL <= (truncatedInputLength - position))) - { - ite = TRUE; - } - else - { - uint64_t - positionAfterTriangle0 = - ValidatePoint(Ctxt, - ErrorHandlerFn, - truncatedInput, - truncatedInputLength, - position); - uint64_t result1; - if (EverParseIsSuccess(positionAfterTriangle0)) - { - result1 = positionAfterTriangle0; - } - else - { - ErrorHandlerFn("_triangle", - "corners.element", - EverParseErrorReasonOfResult(positionAfterTriangle0), - EverParseGetValidatorErrorKind(positionAfterTriangle0), - Ctxt, - truncatedInput, - position); - result1 = positionAfterTriangle0; - } - result = result1; - ite = EverParseIsError(result1); - } - if (ite) - { - break; - } - } - uint64_t res = result; - positionAfterTriangle = res; + res = EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition); } + uint64_t positionAfterTriangle = res; if (EverParseIsSuccess(positionAfterTriangle)) { return positionAfterTriangle; diff --git a/src/3d/InterpreterTarget.fst b/src/3d/InterpreterTarget.fst index 9da6a5d7c..045c67260 100644 --- a/src/3d/InterpreterTarget.fst +++ b/src/3d/InterpreterTarget.fst @@ -814,8 +814,41 @@ let rec print_typ (mname:string) (t:typ) c | T_nlist fn n t -> - Printf.sprintf "(T_nlist \"%s\" %s %s)" + let rec as_constant n = + let open T in + match fst n with + | Constant (A.Int sw i) -> + Some (A.Int sw i) + | App (Cast _from to) [ n ] -> ( + match as_constant n with + | Some (A.Int _ i) -> Some (A.Int to i) + | _ -> None + ) + | App (Plus _) [ n; m ] -> ( + match as_constant n, as_constant m with + | Some (A.Int sw i), Some (A.Int _ j) -> Some (A.Int sw (i + j)) + | _ -> None + ) + | App (Minus _) [ n; m ] -> ( + match as_constant n, as_constant m with + | Some (A.Int sw i), Some (A.Int _ j) -> Some (A.Int sw (i - j)) + | _ -> None + ) + | App (Mul _) [ n; m ] -> ( + match as_constant n, as_constant m with + | Some (A.Int sw i), Some (A.Int _ j) -> Some (A.Int sw (i `op_Multiply` j)) + | _ -> None + ) + | _ -> None + in + let is_const, n = + match as_constant n with + | None -> false, n + | Some m -> true, (T.Constant m, snd n) + in + Printf.sprintf "(T_nlist \"%s\" %b %s %s)" fn + is_const (T.print_expr mname n) (print_typ mname t) diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst index a7f7e6595..74c303f2e 100644 --- a/src/3d/prelude/EverParse3d.Interpreter.fst +++ b/src/3d/prelude/EverParse3d.Interpreter.fst @@ -696,6 +696,7 @@ let rec action_as_action (* Some AST nodes contain source comments that we propagate to the output *) let comments = string + [@@ no_auto_projectors] noeq type typ @@ -900,6 +901,7 @@ type typ fieldname:string -> #wk:_ -> #pk:P.parser_kind true wk -> #i:_ -> #l:_ -> #d:_ -> #b:_ -> + n_is_constant:bool -> n:U32.t -> t:typ pk i d l b -> typ P.kind_nlist i d l false @@ -1005,7 +1007,7 @@ let rec as_type | T_with_dep_action _ i _ -> dtyp_as_type i - | T_nlist _ n t -> + | T_nlist _ _ n t -> P.nlist n (as_type t) | T_at_most _ n t -> @@ -1094,7 +1096,7 @@ let rec as_parser //assert_norm (as_type g (T_with_comment t c) == as_type g t); as_parser t - | T_nlist _ n t -> + | T_nlist _ _ n t -> P.parse_nlist n (as_parser t) | T_at_most _ n t -> @@ -1300,11 +1302,11 @@ let rec as_validator assert_norm (as_parser (T_with_comment fn t c) == as_parser t); A.validate_with_comment c (as_validator typename t) - | T_nlist fn n t -> - assert_norm (as_type (T_nlist fn n t) == P.nlist n (as_type t)); - assert_norm (as_parser (T_nlist fn n t) == P.parse_nlist n (as_parser t)); + | T_nlist fn n_is_const n t -> + assert_norm (as_type (T_nlist fn n_is_const n t) == P.nlist n (as_type t)); + assert_norm (as_parser (T_nlist fn n_is_const n t) == P.parse_nlist n (as_parser t)); A.validate_with_error_handler typename fn - (A.validate_nlist n (as_validator typename t)) + (A.validate_nlist_constant_size_without_actions n_is_const n (as_validator typename t)) | T_at_most fn n t -> assert_norm (as_type (T_at_most fn n t) == P.t_at_most n (as_type t)); @@ -1490,4 +1492,4 @@ let coerce_dt_app (steps:_) : T.Tac unit = zeta; iota; simplify]; - T.trivial() + T.trivial() \ No newline at end of file