Skip to content

Commit

Permalink
fixing #125; avoid generating loops to check arrays whose elements ar…
Browse files Browse the repository at this point in the history 
…e unconstrained
  • Loading branch information
@nikswamy
nikswamy committed Oct 17, 2024
1 parent 786b370 commit b6f0dc9
Show file tree
Hide file tree
Showing 4 changed files with 61 additions and 259 deletions.
130 changes: 12 additions & 118 deletions doc/3d-snapshot/GetFieldPtr.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
{
Expand All @@ -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))
{
Expand Down
139 changes: 6 additions & 133 deletions doc/3d-snapshot/Triangle2.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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;
Expand Down
35 changes: 34 additions & 1 deletion src/3d/InterpreterTarget.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
Loading

0 comments on commit b6f0dc9

Please sign in to comment.