From f79c95aa234be01b22f8684d9c00c7aaa0b0ae6f Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 6 May 2020 14:45:42 +0000 Subject: [PATCH 1/5] Add definedness condition for substrBytes --- k-distribution/include/builtin/domains.k | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 3b73ebb9ac4..b79e9ab42ac 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -863,6 +863,13 @@ endmodule module BYTES-SYMBOLIC [symbolic, kast] imports BYTES-IN-K + + rule #Ceil(substrBytes(@B, @START, @END)) + => { @START <=Int @END #Equals true } + #And + { lengthBytes(@B) <=Int @END #Equals true } + #And #Ceil(@B) #And #Ceil(@START) #And #Ceil(@END) + [anywhere] endmodule module BYTES From 49a09caa3be482223cf8cf67435c7df5e113a09f Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 6 May 2020 14:46:15 +0000 Subject: [PATCH 2/5] Add simplification for removing substrBytes --- k-distribution/include/builtin/domains.k | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index b79e9ab42ac..5d2e8c1c2d9 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -870,6 +870,11 @@ module BYTES-SYMBOLIC [symbolic, kast] { lengthBytes(@B) <=Int @END #Equals true } #And #Ceil(@B) #And #Ceil(@START) #And #Ceil(@END) [anywhere] + + rule substrBytes(B, START, END) => B + requires START ==Int 0 + andBool lengthBytes(B) ==Int END + [simplification] endmodule module BYTES From e45e3d9359f428680a4c07c494cb831fc8636ef4 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 6 May 2020 14:47:17 +0000 Subject: [PATCH 3/5] Add simplifications for substrBytes over concatenation --- k-distribution/include/builtin/domains.k | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 5d2e8c1c2d9..29300cf4d04 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -875,6 +875,22 @@ module BYTES-SYMBOLIC [symbolic, kast] requires START ==Int 0 andBool lengthBytes(B) ==Int END [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B1, START, END) + requires END <=Int lengthBytes(B1) + [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) => substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) + requires lengthBytes(B1) <=Int START + [simplification] + + rule substrBytes(B1 +Bytes B2, START, END) + => substrBytes(B1, START, lengthBytes(B1)) + +Bytes + substrBytes(B2, START -Int lengthBytes(B1), END -Int lengthBytes(B1)) + requires notBool (lengthBytes(B1) >=Int END) + andBool notBool (lengthBytes(B1) <=Int START) + [simplification] endmodule module BYTES From 0cad72df39052d184759d1b66480a6d591fca242 Mon Sep 17 00:00:00 2001 From: Rikard Hjort Date: Fri, 8 May 2020 12:46:42 +0200 Subject: [PATCH 4/5] Move to module `BYTES-KORE-SYMBOLIC` --- k-distribution/include/builtin/domains.k | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 29300cf4d04..54340288151 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -863,7 +863,11 @@ endmodule module BYTES-SYMBOLIC [symbolic, kast] imports BYTES-IN-K +endmodule +module BYTES-KORE-SYMBOLIC [kore, symbolic] + import BYTES-IN-K + rule #Ceil(substrBytes(@B, @START, @END)) => { @START <=Int @END #Equals true } #And From ac38817fac6fcc3342717214bf2db5162c6db319 Mon Sep 17 00:00:00 2001 From: Rikard Hjort Date: Fri, 8 May 2020 19:13:41 +0200 Subject: [PATCH 5/5] Import BYTES-KORE instead of BYTES-IN-K --- k-distribution/include/builtin/domains.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 54340288151..d1f49daec36 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -866,7 +866,7 @@ module BYTES-SYMBOLIC [symbolic, kast] endmodule module BYTES-KORE-SYMBOLIC [kore, symbolic] - import BYTES-IN-K + import BYTES-KORE rule #Ceil(substrBytes(@B, @START, @END)) => { @START <=Int @END #Equals true }