From 9a4db183d1eaf08e14f97b43722b3bd0b1eb52bf Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 19 Oct 2024 08:51:03 +0300 Subject: [PATCH 1/4] Add DeleteOfStructSlot inferences to ConstWrittenToBytesOfStorVarProcessed --- clientlib/storage_modeling/tight_packing.dl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl index 8b7ce3f0..74c4f8ef 100644 --- a/clientlib/storage_modeling/tight_packing.dl +++ b/clientlib/storage_modeling/tight_packing.dl @@ -686,6 +686,10 @@ ConstWrittenToBytesOfStorVarProcessed("0xNoVar", newVal, store, load, $Variable( ValueIsByteMask(mask), newVal = as(@and_256(@shr_256(@number_to_hex(excessRightBytes*8), const), mask), Value). +ConstWrittenToBytesOfStorVarProcessed("0xNoVar", "0x0", store, store, $Variable(parentCons), actualByteLow, actualByteHigh):- + DeleteOfStructSlot(store, $Variable(parentCons)), + ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, actualByteLow, actualByteHigh)). + /** Basic type inference Hacky for now just to print the correct uintX or address if nessesary. From 63581f870ae3b98185e449c582373a15ae1b5f3c Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 19 Oct 2024 09:44:39 +0300 Subject: [PATCH 2/4] Increase completeness of simple ConstWrittenToBytesOfStorVar case --- clientlib/storage_modeling/tight_packing.dl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl index 74c4f8ef..3e715830 100644 --- a/clientlib/storage_modeling/tight_packing.dl +++ b/clientlib/storage_modeling/tight_packing.dl @@ -214,8 +214,8 @@ VarWrittenToBytesOfStorVar(var, store, construct, 0, numOfBytes - 1):- // Added for completeness to revisit ConstWrittenToBytesOfStorVar(var, val, store, store, construct, 0, 31):- SSTOREToConstruct(store, construct, var), - Variable_Value(var, val), - !SLOADOfConstruct(_, construct, _). + Variable_Value(var, val). + // !SLOADOfConstruct(_, construct, _). FailedMergedStorageModelingReason(storVar, stmt, stmt2, [low, high], [otherLow, otherHigh]), FailedMergedStorageModeling(storVar):- From 90cda2b6ce42da6d06c3344975ac0d342a19cf6d Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 19 Oct 2024 17:51:25 +0300 Subject: [PATCH 3/4] fix new pattern for viaIR code --- clientlib/storage_modeling/tight_packing.dl | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl index 3e715830..05f590ef 100644 --- a/clientlib/storage_modeling/tight_packing.dl +++ b/clientlib/storage_modeling/tight_packing.dl @@ -214,7 +214,9 @@ VarWrittenToBytesOfStorVar(var, store, construct, 0, numOfBytes - 1):- // Added for completeness to revisit ConstWrittenToBytesOfStorVar(var, val, store, store, construct, 0, 31):- SSTOREToConstruct(store, construct, var), - Variable_Value(var, val). + Variable_Value(var, val), + // 0x0 is handled differently due to new viaIR delete patterns + val != "0x0". // !SLOADOfConstruct(_, construct, _). FailedMergedStorageModelingReason(storVar, stmt, stmt2, [low, high], [otherLow, otherHigh]), From 51c49d6934cde5bba4f18118d6ce304b18ccc49b Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Wed, 23 Oct 2024 21:42:52 -0700 Subject: [PATCH 4/4] Increase completeness of VarHoldsBytesOfStorVarFinal --- clientlib/storage_modeling/tight_packing.dl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl index 05f590ef..466331b8 100644 --- a/clientlib/storage_modeling/tight_packing.dl +++ b/clientlib/storage_modeling/tight_packing.dl @@ -174,7 +174,15 @@ VarHoldsBytesOfStorVarFinal(var, load, storVar, low, high):- VarHoldsBytesOfStorVarFinal(var, load, storVar, low, high):- VarHoldsBytesOfStorVar(var, load, storVar, low, high), - (MSTORE(_, _, var); ActualArgs(_, var, _); ActualReturnArgs(_, var, _)). + VariableUsedInEndLevelOperation(var). + +// end-level in regards to byte-level shifting/casting trasformations (is incomplete) +.decl VariableUsedInEndLevelOperation(var: Variable) +VariableUsedInEndLevelOperation(var):- + MSTORE(_, _, var); ActualArgs(_, var, _); ActualReturnArgs(_, var, _); + LT(_, var, _, _); LT(_, _, var, _); GT(_, var, _, _); GT(_, _, var, _); + SLT(_, var, _, _); SLT(_, _, var, _); SGT(_, var, _, _); SGT(_, _, var, _); + EQ(_, var, _, _); EQ(_, _, var, _). .decl AnyLoadStoreStorVarBytes(loadOrStore: Statement, storVar: StorageConstruct, low: number, high: number) DEBUG_OUTPUT(AnyLoadStoreStorVarBytes)