Skip to content

Commit 2b06115

Browse files
ajewellamzajewellamz
committed
m
1 parent 38c9233 commit 2b06115

File tree

2 files changed

+53
-40
lines changed

2 files changed

+53
-40
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

Lines changed: 51 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -863,33 +863,38 @@ module DynamoDBFilterExpr {
863863
(x, MakeAttr(s[pos..pos+x]))
864864
}
865865

866-
function method {:opaque} VarOrSize(input: seq<Token>)
867-
: (ret : nat)
868-
ensures ret <= |input|
866+
function method {:opaque} VarOrSize(input: seq<Token>, pos : uint64)
867+
: (ret : uint64)
868+
requires pos as nat <= |input|
869+
ensures pos as nat + ret as nat <= |input|
869870
{
870-
if |input| == 0 then
871+
SequenceIsSafeBecauseItIsInMemory(input);
872+
if |input| as uint64 == pos then
871873
0
872-
else if input[0].Value? || input[0].Attr? then
874+
else if input[pos].Value? || input[pos].Attr? then
873875
1
874-
else if 3 < |input| && input[0].Size? && input[1].Open? && IsVar(input[2]) && input[3].Close? then
876+
else if Add(3, pos) < |input| as uint64 && input[pos].Size? && input[pos+1].Open? && IsVar(input[pos+2]) && input[pos+3].Close? then
875877
4
876878
else
877879
0
878880
}
879881

880882
// does it start with "A BETWEEN X AND Y"
881-
function method IsBetween(input: seq<Token>)
882-
: (ret : Option<(int, int, int)>)
883-
ensures ret.Some? ==> (ret.value.0 + ret.value.1 + ret.value.2 + 2) <= |input|
883+
function method IsBetween(input: seq<Token>, pos : uint64)
884+
: (ret : Option<(uint64, uint64, uint64)>)
885+
ensures HasUint64Size(|input|)
886+
ensures ret.Some? ==> (pos as nat + ret.value.0 as nat + ret.value.1 as nat + ret.value.2 as nat + 2) <= |input|
884887
{
885-
if |input| < 5 then
888+
SequenceIsSafeBecauseItIsInMemory(input);
889+
var input_size : uint64 := |input| as uint64;
890+
if input_size < Add(pos, 5) then
886891
None
887892
else
888-
var p1 := VarOrSize(input);
889-
if 0 < p1 && (p1+1 < |input|) && input[p1].Between? then
890-
var p2 := VarOrSize(input[p1+1..]);
891-
if 0 < p2 && (p1+p2+2 < |input|) && input[p1+p2+1].And? then
892-
var p3 := VarOrSize(input[p1+p2+2..]);
893+
var p1 := VarOrSize(input, pos);
894+
if 0 < p1 && (Add(pos+p1, 1) < input_size) && input[pos+p1].Between? then
895+
var p2 := VarOrSize(input, pos+p1+1);
896+
if 0 < p2 && (Add(pos+p1+p2, 2) < input_size) && input[pos+p1+p2+1].And? then
897+
var p3 := VarOrSize(input, pos+p1+p2+2);
893898
if 0 < p3 then
894899
Some((p1, p2, p3))
895900
else
@@ -901,15 +906,17 @@ module DynamoDBFilterExpr {
901906
}
902907

903908
// does it start with "A IN ("
904-
predicate method IsIN(input: seq<Token>)
909+
predicate method IsIN(input: seq<Token>, pos : uint64)
910+
requires pos as nat < |input|
905911
{
906-
if |input| < 3 then
912+
SequenceIsSafeBecauseItIsInMemory(input);
913+
if |input| as uint64 < Add(pos, 3) then
907914
false
908-
else if !IsVar(input[0]) then
915+
else if !IsVar(input[pos]) then
909916
false
910-
else if input[1] != In then
917+
else if input[pos+1] != In then
911918
false
912-
else if input[2] != Open then
919+
else if input[pos+2] != Open then
913920
false
914921
else
915922
true
@@ -919,22 +926,23 @@ module DynamoDBFilterExpr {
919926
// transform A BETWEEN X AND Y to BETWEEN(A, X, Y)
920927
function method ConvertToPrefix(input: seq<Token>) : (res : seq<Token>)
921928
{
922-
var between := IsBetween(input);
923929
if |input| < 5 then
924930
input
925-
else if IsIN(input) then
931+
else if IsIN(input, 0) then
926932
[input[1], input[2], input[0], Comma] + ConvertToPrefix(input[3..])
927-
else if between.Some? then
928-
var b := between.value;
929-
[Between, Open] + input[0..b.0] + [Comma] + input[b.0+1..b.0+b.1+1] + [Comma]
930-
+ input[b.0+b.1+2..b.0+b.1+b.2+2] + [Close] + ConvertToPrefix(input[b.0+b.1+b.2+2..])
931933
else
932-
[input[0]] + ConvertToPrefix(input[1..])
934+
var between := IsBetween(input, 0);
935+
if between.Some? then
936+
var b := between.value;
937+
[Between, Open] + input[0..b.0] + [Comma] + input[b.0+1..b.0+b.1+1] + [Comma]
938+
+ input[b.0+b.1+2..b.0+b.1+b.2+2] + [Close] + ConvertToPrefix(input[b.0+b.1+b.2+2..])
939+
else
940+
[input[0]] + ConvertToPrefix(input[1..])
933941
}
934942

935943
lemma TestConvertToPrefix3(input: seq<Token>)
936944
requires input == [MakeAttr("A"), In, Open, MakeAttr("B"), Comma, MakeAttr("C"), Close]
937-
ensures IsIN(input)
945+
ensures IsIN(input, 0)
938946
ensures ConvertToPrefix(input) == [In, Open, MakeAttr("A"), Comma, MakeAttr("B"), Comma, MakeAttr("C"), Close]
939947
{}
940948

@@ -1084,7 +1092,7 @@ module DynamoDBFilterExpr {
10841092
)
10851093
returns (ret : Result<bool, Error>)
10861094
{
1087-
ret := InnerEvalExpr(input, [], item, names, values);
1095+
ret := InnerEvalExpr(input, [], item, names, values, 0);
10881096
}
10891097

10901098
// count the number of strings
@@ -1224,8 +1232,8 @@ module DynamoDBFilterExpr {
12241232

12251233
// true if target in list
12261234
predicate method is_in(target : DDB.AttributeValue, list : seq<StackValue>, pos : uint64 := 0)
1227-
requires pos as nat <= |list|
1228-
decreases |list| - pos as nat
1235+
requires pos as nat <= |list|
1236+
decreases |list| - pos as nat
12291237
{
12301238
SequenceIsSafeBecauseItIsInMemory(list);
12311239
if |list| as uint64 == pos then
@@ -1484,43 +1492,47 @@ module DynamoDBFilterExpr {
14841492
stack : seq<StackValue>,
14851493
item : DDB.AttributeMap,
14861494
names : Option<DDB.ExpressionAttributeNameMap>,
1487-
values : DDB.ExpressionAttributeValueMap
1495+
values : DDB.ExpressionAttributeValueMap,
1496+
pos : uint64
14881497
)
14891498
returns (ret : Result<bool, Error>)
1499+
requires pos as nat <= |input|
1500+
decreases |input| - pos as nat
14901501
{
1491-
if 0 == |input| {
1502+
SequenceIsSafeBecauseItIsInMemory(input);
1503+
if pos == |input| as uint64 {
14921504
if 1 == |stack| && stack[0].Bool? {
14931505
return Success(stack[0].b);
14941506
} else {
14951507
return Failure(E("ended with bad stack"));
14961508
}
14971509
} else {
1498-
var t := input[0];
1510+
var t := input[pos];
14991511
if t.Value? {
1500-
ret := InnerEvalExpr(input[1..], stack + [StackValueFromValue(t.s, values)], item, names, values);
1512+
ret := InnerEvalExpr(input, stack + [StackValueFromValue(t.s, values)], item, names, values, pos+1);
15011513
} else if t.Attr? {
1502-
ret := InnerEvalExpr(input[1..], stack + [StackValueFromAttr(t, item, names)], item, names, values);
1514+
ret := InnerEvalExpr(input, stack + [StackValueFromAttr(t, item, names)], item, names, values, pos+1);
15031515
} else if IsUnary(t) {
15041516
if 0 == |stack| {
15051517
ret := Failure(E("Empty stack for unary op"));
15061518
} else {
15071519
var val :- apply_unary(t, stack[|stack|-1]);
1508-
ret := InnerEvalExpr(input[1..], stack[..|stack|-1] + [val], item, names, values);
1520+
ret := InnerEvalExpr(input, stack[..|stack|-1] + [val], item, names, values, pos+1);
15091521
}
15101522
} else if IsBinary(t) {
15111523
if |stack| < 2 {
15121524
ret := Failure(E("Empty stack for binary op"));
15131525
} else {
15141526
var val :- apply_binary(t, stack[|stack|-2], stack[|stack|-1]);
1515-
ret := InnerEvalExpr(input[1..], stack[..|stack|-2] + [val], item, names, values);
1527+
ret := InnerEvalExpr(input, stack[..|stack|-2] + [val], item, names, values, pos+1);
15161528
}
15171529
} else if IsFunction(t) {
15181530
var num_args := NumArgs(t, stack);
15191531
if |stack| < num_args {
15201532
ret := Failure(E("Empty stack for function call"));
15211533
} else {
15221534
var val :- apply_function(t, stack, num_args);
1523-
ret := InnerEvalExpr(input[1..], stack[..|stack|-num_args] + [val], item, names, values);
1535+
ret := InnerEvalExpr(input, stack[..|stack|-num_args] + [val], item, names, values, pos+1);
15241536
}
15251537
} else {
15261538
ret := Success(true);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,8 @@ module TestDynamoDBFilterExpr {
6363
expect_equal(ParseExpr(" A_B AnD B_C "), [MakeAttr("A_B"), And, MakeAttr("B_C")]);
6464

6565
var input := [Not, MakeAttr("A"), In, Open, MakeAttr("B"), Comma, MakeAttr("C"), Close, Or];
66-
expect IsIN(input[1..]);
66+
expect IsIN(input, 1);
67+
expect IsIN(input[1..], 0);
6768
expect_equal(ConvertToPrefix(input), [Not, In, Open, MakeAttr("A"), Comma, MakeAttr("B"), Comma, MakeAttr("C"), Close, Or]);
6869

6970
input := [And, Or, Not, And, Or, Not, And, Or, Not];

0 commit comments

Comments
 (0)