From 52bac50ca186b73feeae54dc5abfb9b4f9ec0322 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 1 Nov 2024 21:57:14 +0200
Subject: [PATCH 01/53] Improve type inference for address vars in ir code

---
 clientlib/storage_modeling/tight_packing.dl | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 18f013cc..5e2e64ee 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -801,6 +801,16 @@ SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "add
   widthBytes = 1 + byteHigh - byteLow,
   widthBytes = 20.
 
+SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
+  AddressTypedVar(addrFrom),
+  DataFlows(addrFrom, addr),
+  (SUB(_, otherAddr, addr, _) ; SUB(_, addr, otherAddr, _)),
+  DataFlows(var, otherAddr),
+  VarHoldsBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh),
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  widthBytes = 1 + byteHigh - byteLow,
+  widthBytes = 20.
+
 .decl AddressTypedVar(addrVar:Variable)
 AddressTypedVar(addr):-
   CALL(_, _, addr, _, _, _, _, _, _);

From 5c0db896647232e1e4b98dd0c5cb0880a5dedf3d Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Sat, 2 Nov 2024 00:15:55 +0200
Subject: [PATCH 02/53] Change storage var type inference logic

---
 clientlib/storage_modeling/data_structures.dl | 50 ++++++++++++++++---
 clientlib/storage_modeling/tight_packing.dl   |  4 +-
 2 files changed, 45 insertions(+), 9 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 7ffbce11..adad55de 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -85,6 +85,11 @@
 // Note: Can probably be unified with `DataStructure_Type`
 .decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
 
+// Added interm relation that can results removed via subsumption
+.decl StorageVariable_IntermType(cons: StorageConstruct, type: symbol) btree_delete
+
+.decl StorageVariable_IntermTypeDone(numOfFacts: number)
+
 // Doesn't contain TightlyPackedVariable, maybe revisit
 .decl StorageConstruct_ParentAndOffset(cons: StorageConstruct, parentCons: StorageConstruct, offset: number)
 
@@ -431,23 +436,54 @@ DataStructure_Type($Array(parentCons), "string"):-
   IsDataStructureConstruct($Array(parentCons)),
   BytesOrStringLengthV2($Array(parentCons), _).
 
-StorageVariable_Type(var, "uint256"):-
+StorageVariable_IntermTypeDone(numOfFacts):-
+  numOfFacts = count : StorageVariable_IntermType(_, _).
+
+StorageVariable_Type(var, type):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType(var, type).
+
+StorageVariable_IntermType(var, "uint256"):-
   IsStorageConstruct(var),
   var = $Variable(cons), cons = cons,
   ProcessedStorageVariable(var, var).
 
-StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  !SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), _),
   widthBytes = 1 + byteHigh - byteLow,
+  widthBytes != 20,
+  widthBytes != 1,
   type = cat("uint", to_string(widthBytes * 8)).
 
-StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
+  widthBytes = 1 + byteHigh - byteLow,
+  widthBytes = 20.
 
-StorageVariable_Type(var, type):-
-  StorageVariable_Type(packedVar, type),
+StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
+  DataFlows(var, arithOp),
+  Statement_Uses(stmt, arithOp, _),
+  Statement_Opcode(stmt, op),
+  (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),
+  constVal != "0x0", constVal != "0x1".
+
+// StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+//   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+//   SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
+
+StorageVariable_IntermType(var, type):-
+  StorageVariable_IntermType(packedVar, type),
   ProcessedStorageVariable(var, packedVar),
   IsStorageConstruct(var),
   1 = count: ProcessedStorageVariable(var, _).
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 5e2e64ee..a0f9bbc9 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -767,12 +767,12 @@ ConstWrittenToBytesOfStorVarProcessed("0xNoVar", "0x0", store, store, $Variable(
 StorageVariableType(storVar, type):-
   StorageVariableInfo(storVar, slot, byteLow, byteHigh),
   widthBytes = 1 + byteHigh - byteLow,
-  !SpecialStorageVariableType($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), _),
+  !StorageVariable_Type($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), _),
   type = cat("uint", to_string(widthBytes * 8)).
 
 StorageVariableType(storVar, type):-
   StorageVariableInfo(storVar, slot, byteLow, byteHigh),
-  SpecialStorageVariableType($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), type).
+  StorageVariable_Type($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), type).
 
 SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),

From 9a268aa78f8bb076ebc312deb6ac56003cc8ddd3 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Sat, 2 Nov 2024 00:55:28 +0200
Subject: [PATCH 03/53] More work on address and uint160

---
 clientlib/storage_modeling/data_structures.dl | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index adad55de..44432ed5 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -462,6 +462,8 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "add
 
 StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
 
+StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
 
@@ -473,6 +475,15 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Statement_Opcode(stmt, op),
   (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),
+  20 = 1 + byteHigh - byteLow,
+  DataFlows(var, arithOp),
+  Statement_Uses(stmt, arithOp, _),
+  Statement_Opcode(stmt, op),
+  (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),

From 69c2031077a575c7309e6dfd8d66f281cc669937 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Sun, 3 Nov 2024 21:00:59 +0200
Subject: [PATCH 04/53] Introduce uint160flowAnalysis to fix FPs of uint160
 type inf

---
 clientlib/storage_modeling/data_structures.dl | 39 ++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 44432ed5..4186fb2c 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -475,11 +475,15 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Statement_Opcode(stmt, op),
   (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
 
+.decl IsUint(storVar: StorageConstruct, stmt: Statement)
+.output IsUint
+
+IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), stmt),
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),
   20 = 1 + byteHigh - byteLow,
-  DataFlows(var, arithOp),
+  uint160flowAnalysis.GlobalFlows(var, arithOp),
   Statement_Uses(stmt, arithOp, _),
   Statement_Opcode(stmt, op),
   (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
@@ -500,6 +504,39 @@ StorageVariable_IntermType(var, type):-
   1 = count: ProcessedStorageVariable(var, _).
 
 
+.init uint160flowAnalysis = GlobalFlowAnalysis
+uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  Statement_Opcode(stmt, op),
+  (op = "ADD"; op = "MOD" ; op = "EXP"; op = "ADDMOD"; op = "MULMOD").
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  castedTo >= 20.
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),
+  Statement_Defines(stmt, to, 0),
+  !LShiftBytes(_, to, _).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  (Statement_Opcode(stmt, "DIV"); Statement_Opcode(stmt, "SHR")),
+  Statement_Defines(stmt, to, 0),
+  !RShiftBytes(_, to, _).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  SUB(stmt, _, _, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
 // // Disable general rule for now
 // StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $Variable(cons)):-
 //   LikelyVariableLoadingStorageIndex(index),

From 47af35e79b9cab32a70db43244faa76993e85db0 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 01:04:48 +0200
Subject: [PATCH 05/53] better handling of ADD in stor type inf, refactor

---
 clientlib/storage_modeling/data_structures.dl | 43 ++++++++++++-------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 4186fb2c..6a0509e2 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -485,8 +485,11 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uin
   20 = 1 + byteHigh - byteLow,
   uint160flowAnalysis.GlobalFlows(var, arithOp),
   Statement_Uses(stmt, arithOp, _),
-  Statement_Opcode(stmt, op),
-  (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
+  (
+    ActualBinArithStmt(stmt);
+    (Statement_Opcode(stmt, op),
+    (op = "LT"; op = "GT"))
+  ).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
@@ -503,35 +506,43 @@ StorageVariable_IntermType(var, type):-
   IsStorageConstruct(var),
   1 = count: ProcessedStorageVariable(var, _).
 
+.decl ActualBinArithStmt(stmt: Statement)
 
-.init uint160flowAnalysis = GlobalFlowAnalysis
-uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
-uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
-
-uint160flowAnalysis.TransferStmt(stmt):-
+ActualBinArithStmt(stmt):-
   Statement_Opcode(stmt, op),
-  (op = "ADD"; op = "MOD" ; op = "EXP"; op = "ADDMOD"; op = "MULMOD").
+  (op = "MOD" ; op = "EXP"; op = "ADDMOD"; op = "MULMOD").
 
-uint160flowAnalysis.TransferStmt(stmt):-
-  Statement_Defines(stmt, to, 0),
-  LowBytesMaskOp(_, to, castedTo),
-  castedTo >= 20.
-
-uint160flowAnalysis.TransferStmt(stmt):-
+ActualBinArithStmt(stmt):-
   (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),
   Statement_Defines(stmt, to, 0),
   !LShiftBytes(_, to, _).
 
-uint160flowAnalysis.TransferStmt(stmt):-
+ActualBinArithStmt(stmt):-
   (Statement_Opcode(stmt, "DIV"); Statement_Opcode(stmt, "SHR")),
   Statement_Defines(stmt, to, 0),
   !RShiftBytes(_, to, _).
 
-uint160flowAnalysis.TransferStmt(stmt):-
+ActualBinArithStmt(stmt):-
   SUB(stmt, _, _, to),
   !ISZERO(_, to, _),
   !JUMPI(_, _, to).
 
+ActualBinArithStmt(stmt):-
+  ADD(stmt, _, _, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+.init uint160flowAnalysis = GlobalFlowAnalysis
+uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint160flowAnalysis.TransferStmt(stmt):- ActualBinArithStmt(stmt).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  castedTo >= 20.
+
 uint160flowAnalysis.TransferStmt(stmt):-
   PHI(stmt, _, to),
   nUses = count: PHITrans(_, to),

From b6d316fae08dd5e63525bd7d75923b8f4e59f2a3 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 13:22:07 +0200
Subject: [PATCH 06/53] cleanup

---
 clientlib/storage_modeling/data_structures.dl |  3 --
 clientlib/storage_modeling/tight_packing.dl   | 51 -------------------
 2 files changed, 54 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 6a0509e2..fe83775c 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -496,9 +496,6 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),
   constVal != "0x0", constVal != "0x1".
 
-// StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
-//   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-//   SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
 
 StorageVariable_IntermType(var, type):-
   StorageVariable_IntermType(packedVar, type),
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index a0f9bbc9..a6beef9d 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -762,8 +762,6 @@ ConstWrittenToBytesOfStorVarProcessed("0xNoVar", "0x0", store, store, $Variable(
 
 .decl StorageVariableType(storVar:symbol, type:symbol)
 
-.decl SpecialStorageVariableType(storVar:StorageConstruct, type:symbol)
-
 StorageVariableType(storVar, type):-
   StorageVariableInfo(storVar, slot, byteLow, byteHigh),
   widthBytes = 1 + byteHigh - byteLow,
@@ -774,55 +772,6 @@ StorageVariableType(storVar, type):-
   StorageVariableInfo(storVar, slot, byteLow, byteHigh),
   StorageVariable_Type($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), type).
 
-SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  VarHoldsBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes = 20,
-  DataFlows(var, addr),
-  AddressTypedVar(addr).
-
-SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes = 20,
-  DataFlows(addr, var),
-  AddressTypedVar(addr).
-
-// Hack to cover msg.sender == var and other similar things
-SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
-  AddressTypedVar(addrFrom),
-  DataFlows(addrFrom, addr),
-  (EQ(_, otherAddr, addr, _) ; EQ(_, addr, otherAddr, _)),
-  DataFlows(var, otherAddr),
-  VarHoldsBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh),
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes = 20.
-
-SpecialStorageVariableType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
-  AddressTypedVar(addrFrom),
-  DataFlows(addrFrom, addr),
-  (SUB(_, otherAddr, addr, _) ; SUB(_, addr, otherAddr, _)),
-  DataFlows(var, otherAddr),
-  VarHoldsBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh),
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes = 20.
-
-.decl AddressTypedVar(addrVar:Variable)
-AddressTypedVar(addr):-
-  CALL(_, _, addr, _, _, _, _, _, _);
-  STATICCALL(_, _, addr, _, _, _, _, _);
-  DELEGATECALL(_, _, addr, _, _, _, _, _);
-  SELFDESTRUCT(_, addr);
-  EXTCODECOPY(_, addr, _, _, _);
-  EXTCODESIZE(_, addr, _);
-  EXTCODEHASH(_, addr, _);
-  CALLER(_, addr);
-  ORIGIN(_, addr);
-  ADDRESS(_, addr).
 
 /**
   Temp statements for the source decompiler to hide

From 86221a17ef840049c0eaab9593c9b17143e1cb37 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 14:27:23 +0200
Subject: [PATCH 07/53] no-op to remove load from uint160flowAnalysis

---
 clientlib/storage_modeling/data_structures.dl | 24 ++++++++++++-------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index fe83775c..792be840 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -483,13 +483,8 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uin
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),
   20 = 1 + byteHigh - byteLow,
-  uint160flowAnalysis.GlobalFlows(var, arithOp),
-  Statement_Uses(stmt, arithOp, _),
-  (
-    ActualBinArithStmt(stmt);
-    (Statement_Opcode(stmt, op),
-    (op = "LT"; op = "GT"))
-  ).
+  uint160flowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
@@ -503,6 +498,19 @@ StorageVariable_IntermType(var, type):-
   IsStorageConstruct(var),
   1 = count: ProcessedStorageVariable(var, _).
 
+.decl UintVar(var: Variable)
+UintVar(var):-
+  Statement_Uses(stmt, var, _),
+  (
+    ActualBinArithStmt(stmt);
+    (Statement_Opcode(stmt, op),
+    (op = "LT"; op = "GT"))
+  ).
+
+UintVar(var):-
+  ActualBinArithStmt(stmt),
+  Statement_Defines(stmt, var, _).
+
 .decl ActualBinArithStmt(stmt: Statement)
 
 ActualBinArithStmt(stmt):-
@@ -533,7 +541,7 @@ ActualBinArithStmt(stmt):-
 uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
 uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
 
-uint160flowAnalysis.TransferStmt(stmt):- ActualBinArithStmt(stmt).
+// uint160flowAnalysis.TransferStmt(stmt):- ActualBinArithStmt(stmt).
 
 uint160flowAnalysis.TransferStmt(stmt):-
   Statement_Defines(stmt, to, 0),

From 914afedb1ebe4574b132f33070c4eb8b15de8bbf Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 14:32:43 +0200
Subject: [PATCH 08/53] fix bug

---
 clientlib/storage_modeling/data_structures.dl | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 792be840..be5b32c1 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -475,10 +475,10 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Statement_Opcode(stmt, op),
   (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
 
-.decl IsUint(storVar: StorageConstruct, stmt: Statement)
+.decl IsUint(storVar: StorageConstruct, uintVar: Variable)
 .output IsUint
 
-IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), stmt),
+IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), uintVar),
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),

From 8b286ff10c6774e925b9e668f0916855c8c73c5f Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 15:14:06 +0200
Subject: [PATCH 09/53] Improve uint8 inference by supporting struct ops

---
 clientlib/storage_modeling/data_structures.dl | 38 +++++++++++++++++--
 1 file changed, 34 insertions(+), 4 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index be5b32c1..979ef12e 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -470,10 +470,8 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
-  DataFlows(var, arithOp),
-  Statement_Uses(stmt, arithOp, _),
-  Statement_Opcode(stmt, op),
-  (op = "ADD"; op = "MOD"; op = "EXP"; op = "LT"; op = "GT").
+  uint8AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar).
 
 .decl IsUint(storVar: StorageConstruct, uintVar: Variable)
 .output IsUint
@@ -491,6 +489,12 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),
   constVal != "0x0", constVal != "0x1".
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
+  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  Variable_Value(uintVar, constVal),
+  constVal != "0x0", constVal != "0x1".
 
 StorageVariable_IntermType(var, type):-
   StorageVariable_IntermType(packedVar, type),
@@ -537,6 +541,31 @@ ActualBinArithStmt(stmt):-
   !ISZERO(_, to, _),
   !JUMPI(_, _, to).
 
+.decl GlobalStructFlowsBase(from: Variable, to: Variable)
+GlobalStructFlowsBase(storedVar, loadedVar):-
+  StructLoad(_, structBase, wordOffset, loadedVar),
+  VarPointsToStruct(_, structBase, heapCtx, structId),
+  VarPointsToStruct(_, structBaseAlias, heapCtx, structId),
+  StructStore(_, structBaseAlias, wordOffset, storedVar).
+
+.init uint8AliasFlowAnalysis = GlobalFlowAnalysis
+uint8AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint8AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint8AliasFlowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
+  castedTo >= 1.
+
+uint8AliasFlowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
+uint8AliasFlowAnalysis.FlowsBase(from, to):-
+  GlobalStructFlowsBase(from, to).
+
 .init uint160flowAnalysis = GlobalFlowAnalysis
 uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
 uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
@@ -546,6 +575,7 @@ uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
 uint160flowAnalysis.TransferStmt(stmt):-
   Statement_Defines(stmt, to, 0),
   LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
   castedTo >= 20.
 
 uint160flowAnalysis.TransferStmt(stmt):-

From 25cca5b8dc5569ffd9caf9f1765a767de42e5222 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 15:52:25 +0200
Subject: [PATCH 10/53] further improve uint8 inf

---
 clientlib/storage_modeling/data_structures.dl | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 979ef12e..24ad0219 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -496,6 +496,12 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Variable_Value(uintVar, constVal),
   constVal != "0x0", constVal != "0x1".
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
+  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  UintVar(uintVar).
+
 StorageVariable_IntermType(var, type):-
   StorageVariable_IntermType(packedVar, type),
   ProcessedStorageVariable(var, packedVar),

From f19415fbeefc0a23db024ab988f9de39b96b9471 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 17:21:14 +0200
Subject: [PATCH 11/53] fix bug with reusable constants causing FPs

---
 clientlib/storage_modeling/data_structures.dl | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 24ad0219..4abd1c20 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -467,11 +467,13 @@ StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(sto
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
 
+IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
   uint8AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar).
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
 
 .decl IsUint(storVar: StorageConstruct, uintVar: Variable)
 .output IsUint
@@ -496,11 +498,13 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Variable_Value(uintVar, constVal),
   constVal != "0x0", constVal != "0x1".
 
+IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
   uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  UintVar(uintVar).
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
 
 StorageVariable_IntermType(var, type):-
   StorageVariable_IntermType(packedVar, type),

From d44859ae9ef8d939a4d287b9f5e802aeb7ee4f3f Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 19:21:05 +0200
Subject: [PATCH 12/53] Try better handling of bytes32 and uint256

---
 clientlib/storage_modeling/data_structures.dl | 27 ++++++++++++++++++-
 clientlib/storage_modeling/tight_packing.dl   |  7 +++++
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 4abd1c20..c54d47de 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -443,7 +443,7 @@ StorageVariable_Type(var, type):-
   StorageVariable_IntermTypeDone(_),
   StorageVariable_IntermType(var, type).
 
-StorageVariable_IntermType(var, "uint256"):-
+StorageVariable_IntermType(var, "bytes32"):-
   IsStorageConstruct(var),
   var = $Variable(cons), cons = cons,
   ProcessedStorageVariable(var, var).
@@ -460,10 +460,20 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "add
   widthBytes = 1 + byteHigh - byteLow,
   widthBytes = 20.
 
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
 StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
 
 StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
 
+StorageVariable_IntermType(storVar, "bytes32") <= StorageVariable_IntermType(storVar, "uint256"):- 1=1.
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
 
@@ -593,6 +603,21 @@ uint160flowAnalysis.TransferStmt(stmt):-
   nUses = count: PHITrans(_, to),
   nUses < 4.
 
+.init uint256AliasFlowAnalysis = GlobalFlowAnalysis
+uint256AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint256AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint256AliasFlowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
+  castedTo >= 30.
+
+uint256AliasFlowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
 // // Disable general rule for now
 // StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $Variable(cons)):-
 //   LikelyVariableLoadingStorageIndex(index),
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index a6beef9d..3c1a1a49 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -772,6 +772,13 @@ StorageVariableType(storVar, type):-
   StorageVariableInfo(storVar, slot, byteLow, byteHigh),
   StorageVariable_Type($TightlyPackedVariable($Constant(slot), byteLow, byteHigh), type).
 
+StorageVariableType(storVar, "uint256"):-
+  StorageVariableInfo(storVar, slot, 0, 31),
+  !StorageVariable_Type($Variable($Constant(slot)), _).
+
+StorageVariableType(storVar, type):-
+  StorageVariableInfo(storVar, slot, 0, 31),
+  StorageVariable_Type($Variable($Constant(slot)), type).
 
 /**
   Temp statements for the source decompiler to hide

From 519766a37cb8ca19160b33f72f0059a99e50b9ba Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 19:58:19 +0200
Subject: [PATCH 13/53] Improve bytes32 vs uint256 analysis

---
 clientlib/storage_modeling/data_structures.dl | 15 +++++++++++++++
 clientlib/storage_modeling/tight_packing.dl   |  2 +-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index c54d47de..17ebd7fb 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -468,6 +468,21 @@ StorageVariable_IntermType(storVar, "uint256"):-
   UintVar(uintVar),
   !Variable_Value(uintVar, _).
 
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  ConstWrittenToBytesOfStorVar(_, constVal, _, _, storVar, 0, 31),
+  strlen(constVal) < 60. //is right aligned
+
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
 StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
 
 StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 3c1a1a49..e9666c02 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -724,7 +724,7 @@ StorageVariablePacksNVars(storageVar, numberOfVars):-
   numberOfVars = count : ProcessedStorageVariable(storageVar, _),
   numberOfVars > 1.
 
-// Does this need to be fixed for the (cons, cons) case
+// TODO: Does this need to be fixed for the (cons, cons) case? YES
 ConstWrittenToBytesOfStorVarProcessed(constVar, const, store, load, $Variable(parentCons), byteLow, byteHigh):-
   ConstWrittenToBytesOfStorVar(constVar, const, store, load, $Variable(parentCons), byteLow, byteHigh),
   ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, byteLow, byteHigh)).

From 7318d542dfa77b121c97da8f666c0a4be9c16ca8 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 4 Nov 2024 20:48:56 +0200
Subject: [PATCH 14/53] Improve uint256 handling

---
 clientlib/storage_modeling/data_structures.dl | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 17ebd7fb..388776f8 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -483,6 +483,15 @@ StorageVariable_IntermType(storVar, "uint256"):-
   UintVar(uintVar),
   !Variable_Value(uintVar, _).
 
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
 StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
 
 StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
@@ -618,6 +627,8 @@ uint160flowAnalysis.TransferStmt(stmt):-
   nUses = count: PHITrans(_, to),
   nUses < 4.
 
+.output uint256AliasFlowAnalysis.GlobalFlows
+
 .init uint256AliasFlowAnalysis = GlobalFlowAnalysis
 uint256AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
 uint256AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).

From f59d32462b100f9fa1c41d6142be34937da8b944 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 5 Nov 2024 17:11:53 +0200
Subject: [PATCH 15/53] support inter-method storage string/bytes inf

---
 clientlib/storage_modeling/data_structures.dl | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 388776f8..64b3e594 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -756,6 +756,21 @@ BytesOrStringLengthV2(cons, phiDef):-
   (PHIStmtTwoUses(_, otherCase, shiftedVar, phiDef); PHIStmtTwoUses(_, shiftedVar, otherCase, phiDef)),
   (ArrayAllocation(_, _, phiDef); MSTORE(_, _, phiDef)).
 
+BytesOrStringLengthV2(cons, phiDef):-
+  ArrayLengthStatement(stmt, _, cons),
+  Statement_Defines(stmt, lengthVar, 0),
+  ActualArgs(caller, lengthVar, index),
+  CallGraphEdge(caller, method),
+  FormalArgs(method, inLenVar, index),
+  SHR(_, shiftBits, inLenVar, shiftedVar),
+  Variable_Value(shiftBits, "0x1"),
+  (AND(_, var127, shiftedVar, otherCase) ; AND(_, shiftedVar, var127, otherCase)),
+  Variable_Value(var127, "0x7f"),
+  (PHIStmtTwoUses(_, otherCase, shiftedVar, phiDef); PHIStmtTwoUses(_, shiftedVar, otherCase, phiDef)),
+  FormalReturnArgs(method, phiDef, retIndex),
+  ActualReturnArgs(caller, outPhiDef, retIndex),
+  (ArrayAllocation(_, _, outPhiDef); MSTORE(_, _, outPhiDef)).
+
 // To introduce ShifyBits rels to remove this rule
 BytesOrStringLengthV2(cons, phiDef):-
   ArrayLengthStatement(stmt, _, cons),
@@ -767,6 +782,22 @@ BytesOrStringLengthV2(cons, phiDef):-
   (PHIStmtTwoUses(_, otherCase, shiftedVar, phiDef); PHIStmtTwoUses(_, shiftedVar, otherCase, phiDef)),
   (ArrayAllocation(_, _, phiDef); MSTORE(_, _, phiDef)).
 
+// To introduce ShifyBits rels to remove this rule
+BytesOrStringLengthV2(cons, phiDef):-
+  ArrayLengthStatement(stmt, _, cons),
+  Statement_Defines(stmt, lengthVar, 0),
+  ActualArgs(caller, lengthVar, index),
+  CallGraphEdge(caller, method),
+  FormalArgs(method, inLenVar, index),
+  DIV(_, inLenVar, twoVar, shiftedVar),
+  Variable_Value(twoVar, "0x2"),
+  (AND(_, var127, shiftedVar, otherCase) ; AND(_, shiftedVar, var127, otherCase)),
+  Variable_Value(var127, "0x7f"),
+  (PHIStmtTwoUses(_, otherCase, shiftedVar, phiDef); PHIStmtTwoUses(_, shiftedVar, otherCase, phiDef)),
+  FormalReturnArgs(method, phiDef, retIndex),
+  ActualReturnArgs(caller, outPhiDef, retIndex),
+  (ArrayAllocation(_, _, outPhiDef); MSTORE(_, _, outPhiDef)).
+
 /**
   A constant that flows to storage (possibly an array) to the result of its keccak256 hash.
   This is needed to model optimized array patterns produced by the `--via-ir` pipeline.

From d6c1f7f4503e72707ece0b8556d827cfd5091e21 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 5 Nov 2024 18:15:47 +0200
Subject: [PATCH 16/53] increase completeness of bytes/string inf

---
 clientlib/storage_modeling/data_structures.dl | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 64b3e594..edc15b23 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -746,6 +746,18 @@ BytesOrStringLengthV2(cons, lenVar):-
   DIV(_, almost, twoVar, lenVar),
   Variable_Value(twoVar, "0x2").
 
+BytesOrStringLengthV2(cons, lenVar):-
+  ArrayLengthStatement(stmt, _, cons),
+  Statement_Defines(stmt, lengthVar, 0),
+  (AND(_, lengthVar, oneVar, lastBitVar) ; AND(_, oneVar, lengthVar, lastBitVar)),
+  Variable_Value(oneVar, "0x1"),
+  ISZERO(_, lastBitVar, notLastBitVar),
+  LShiftBytes(notLastBitVar, shifted, 1),
+  VarPlusConst(shifted, "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", minOne),
+  (AND(_, minOne, lengthVar, almost) ; AND(_, lengthVar, minOne, almost)),
+  DIV(_, almost, twoVar, lenVar),
+  Variable_Value(twoVar, "0x2").
+
 BytesOrStringLengthV2(cons, phiDef):-
   ArrayLengthStatement(stmt, _, cons),
   Statement_Defines(stmt, lengthVar, 0),

From 9e505ba563097170c2543de77942c52569c95843 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 5 Nov 2024 20:17:01 +0200
Subject: [PATCH 17/53] Recursive type inference for uint256

---
 clientlib/storage_modeling/data_structures.dl | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index edc15b23..90244299 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -468,6 +468,26 @@ StorageVariable_IntermType(storVar, "uint256"):-
   UintVar(uintVar),
   !Variable_Value(uintVar, _).
 
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
+  StorageVariable_IntermType(storVar2, "uint256").
+  .plan 0:(6,5,4,3,2,1)
+
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  StorageVariable_IntermType(storVar2, "uint256"),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar2),
+  SSTORE(store, _, uintVar),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  ProcessedStorageVariable(storVar, storVar).
+
+
 // IsUint(storVar, uintVar),
 StorageVariable_IntermType(storVar, "uint256"):-
   ProcessedStorageVariable(storVar, storVar),

From 2ed12d4e540d2c87d37b73172bc25d21622871de Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 5 Nov 2024 22:56:02 +0200
Subject: [PATCH 18/53] Add support for constant arrays

---
 clientlib/storage_modeling/data_structures.dl | 59 ++++++++++++++++---
 1 file changed, 52 insertions(+), 7 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 90244299..8323a93a 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -9,6 +9,7 @@
   used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
 */
 .type StorageIndex = ConstantIndex {value: Value}
+                    | ConstArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
                     | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
                     | ArrayDataStartIndex {parIndex: StorageIndex}
                     | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
@@ -18,6 +19,7 @@
   `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
 */
 .type StorageConstruct = Constant {value: Value}
+                        | ConstArray {parConstruct: StorageConstruct, arraySize: number}
                         | Array {parConstruct: StorageConstruct}
                         | Mapping {parConstruct: StorageConstruct}
                         | Offset {parConstruct: StorageConstruct, offset: number}
@@ -192,6 +194,10 @@ Variable_StorageIndex(def, $ArrayAccessIndex(parentIndex, newIndexVar)):-
   ADDFix(_, indexVar, minusOneConstVar2, newIndexVar),
   Variable_Value(minusOneConstVar2, "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff").
 
+Variable_StorageIndex(def, $ConstArrayAccessIndex(parentIndex, arraySize, checkedVar)):-
+  Variable_StorageIndex(var, parentIndex),
+  ADDFix(_, var, checkedVar, def),
+  RevertEnforcesEnum(checkedVar, arraySize, _).
 
 StorageIndex_StorageConstruct($ConstantIndex(val), $Constant(val)):-
   ActualStorageIndex($ConstantIndex(val)).
@@ -212,6 +218,10 @@ StorageIndex_StorageConstruct($OffsetIndex(parentIndex, offset), $Offset(parentC
   ActualStorageIndex($OffsetIndex(parentIndex, offset)), offset != 0,
   StorageIndex_StorageConstruct(parentIndex, parentCons).
 
+StorageIndex_StorageConstruct($ConstArrayAccessIndex(parentIndex, arraySize, indexVar), $ConstArray(parentCons, arraySize)):-
+  ActualStorageIndex($ConstArrayAccessIndex(parentIndex, arraySize, indexVar)),
+  StorageIndex_StorageConstruct(parentIndex, parentCons).
+
 /**
   We're treating 0 differently to avoid ambiguity between cons+0 and cons
   Otherwise we'd have to normalize the results after all created constructs are created.
@@ -234,6 +244,7 @@ StorageIndex_ParentIndex(index, parentIndex):-
   (
     (index = $ArrayAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $ArrayDataStartIndex(parentIndex));
+    (index = $ConstArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
     (index = $MappingAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $OffsetIndex(parentIndex, offset), offset = offset) // suppress warning
   ).
@@ -243,6 +254,7 @@ StorageIndex_ParentIndexExclOffset(index, parentIndex):-
   (
     (index = $ArrayAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $ArrayDataStartIndex(parentIndex));
+    (index = $ConstArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
     (index = $MappingAccessIndex(parentIndex, indexVar), indexVar = indexVar) // suppress warning
     // commenting this out for now, helps some cases but is not right
     // ;(index = $OffsetIndex(parentIndex, offset), offset > 0) // suppress warning
@@ -277,13 +289,13 @@ ActualStorageIndex(parentIndex):-
 
 StorageIndex_HighLevelUses(index, accessVar, 0, 0, 1):-
   ActualStorageIndex(index),
-  (index = $ArrayAccessIndex($ConstantIndex(const), accessVar); index = $MappingAccessIndex($ConstantIndex(const), accessVar)),
+  (index = $ArrayAccessIndex($ConstantIndex(const), accessVar); (index = $ConstArrayAccessIndex($ConstantIndex(const), arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex($ConstantIndex(const), accessVar)),
   const = const.
 
 StorageIndex_HighLevelUses(index, otherVar, prevOffset, i, prevNestedness + 1),
 StorageIndex_HighLevelUses(index, accessVar, 0, prevNestedness, prevNestedness + 1):-
   ActualStorageIndex(index),
-  (index = $ArrayAccessIndex(parIndex, accessVar); index = $MappingAccessIndex(parIndex, accessVar)),
+  (index = $ArrayAccessIndex(parIndex, accessVar); (index = $ConstArrayAccessIndex(parIndex, arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex(parIndex, accessVar)),
   StorageIndex_HighLevelUses(parIndex, otherVar, prevOffset, i, prevNestedness).
 
 StorageIndex_HighLevelUses($OffsetIndex(parentIndex, offset), accessVar, prevOffset, i, prevNestedness):-
@@ -319,19 +331,19 @@ IsStorageConstruct(cons),
 IsDataStructureConstruct(cons):-
   ActualStorageIndex(index),
   StorageIndex_StorageConstruct(index, cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons)), // filter intermediate constructs
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize)), // filter intermediate constructs
   parentCons = parentCons. // suppress warning
 
 StorageConstruct_ParentAndOffset(cons, paparentCons, offset):-
   IsStorageConstruct(cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); cons = $Variable(parentCons)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
   parentCons = $Offset(paparentCons, offset),
   offset = offset. // suppress warning
 
 StorageConstruct_ParentAndOffset(cons, parentCons, 0):-
   IsStorageConstruct(cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); cons = $Variable(parentCons)),
-  (parentCons = $Array(paparentCons) ; parentCons = $Mapping(paparentCons); parentCons = $Variable(paparentCons)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
+  (parentCons = $Array(paparentCons) ; parentCons = $Mapping(paparentCons); (parentCons = $ConstArray(paparentCons, arraySize2), arraySize2=arraySize2); parentCons = $Variable(paparentCons)),
   paparentCons = paparentCons. // suppress warning
 
 DataStructure_ElemNum(cons, elemNum):-
@@ -436,6 +448,9 @@ DataStructure_Type($Array(parentCons), "string"):-
   IsDataStructureConstruct($Array(parentCons)),
   BytesOrStringLengthV2($Array(parentCons), _).
 
+DataStructure_Type($ConstArray(parentCons, arraySize), cat(type, cat("[", cat(to_string(arraySize), "]")))):-
+  DataStructure_ValueOrElementType($ConstArray(parentCons, arraySize), type).
+
 StorageVariable_IntermTypeDone(numOfFacts):-
   numOfFacts = count : StorageVariable_IntermType(_, _).
 
@@ -443,6 +458,28 @@ StorageVariable_Type(var, type):-
   StorageVariable_IntermTypeDone(_),
   StorageVariable_IntermType(var, type).
 
+.decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
+DEBUG_OUTPUT(StorageVariableToAlias)
+
+StorageVariableToAlias(storVar, alias):-
+  ProcessedStorageVariable(storVar, storVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  uint256AliasFlowAnalysis.GlobalFlows(var, alias).
+
+StorageVariableToAlias(storVar, alias):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  (
+    uint256AliasFlowAnalysis.GlobalFlows(alias, var);
+    uint256AliasFlowAnalysis.GlobalFlows(var, alias)
+  ).
+
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  instances = count : StorageVariableToAlias(storVar, _),
+  instances < 4.
+
 StorageVariable_IntermType(var, "bytes32"):-
   IsStorageConstruct(var),
   var = $Variable(cons), cons = cons,
@@ -579,6 +616,14 @@ UintVar(var):-
   ActualBinArithStmt(stmt),
   Statement_Defines(stmt, var, _).
 
+UintVar(var):-
+  GAS(_, var);
+  CALLVALUE(_, var);
+  TIMESTAMP(_, var);
+  DIFFICULTY(_, var);
+  NUMBER(_, var);
+  BALANCE(_, _, var).
+
 .decl ActualBinArithStmt(stmt: Statement)
 
 ActualBinArithStmt(stmt):-
@@ -733,7 +778,7 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
 
 StorageOffset_Type(offset, type):-
   DataStructure_Type(cons, type),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize)),
   parentCons = $Constant(offset).
 
 

From 86ffff0ad143d48339e49d35f0e86691472667e9 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 6 Nov 2024 01:37:46 +0200
Subject: [PATCH 19/53] Hack to increase coverage for const arrays

---
 clientlib/casts_shifts.dl | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/clientlib/casts_shifts.dl b/clientlib/casts_shifts.dl
index 40b22771..4439c3b7 100644
--- a/clientlib/casts_shifts.dl
+++ b/clientlib/casts_shifts.dl
@@ -382,4 +382,10 @@ RevertEnforcesEnum(checkedVar, smallNum, checkBlock):-
   JUMPI(jumpi, _, newCond),
   Statement_Block(jumpi, checkBlock),
   FallthroughEdge(checkBlock, revertBlock),
-  ThrowBlock(revertBlock).
\ No newline at end of file
+  ThrowBlock(revertBlock).
+
+// Hack, need a better way to get PHI aliases
+RevertEnforcesEnum(checkedVarAlias, smallNum, checkBlock):-
+  RevertEnforcesEnum(checkedVar, smallNum, checkBlock),
+  PHIStmtTwoUses(_, var1, var2, checkedVar),
+  PHIStmtTwoUses(_, var1, var2, checkedVarAlias).
\ No newline at end of file

From 5af7efac2f2c89053ae5008fc806d7e075c89ab6 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 6 Nov 2024 04:02:09 +0200
Subject: [PATCH 20/53] Support packed arrays, only for static ones for now

---
 clientlib/casts_shifts.dl                     | 11 ++++
 clientlib/storage_modeling/data_structures.dl | 52 ++++++++++++++++++-
 2 files changed, 61 insertions(+), 2 deletions(-)

diff --git a/clientlib/casts_shifts.dl b/clientlib/casts_shifts.dl
index 4439c3b7..b28169bc 100644
--- a/clientlib/casts_shifts.dl
+++ b/clientlib/casts_shifts.dl
@@ -147,6 +147,17 @@ CastedAndShiftedVar(checkedVar, toVar, shiftedBy, 1):-
 HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy, castedTo):-
   HighBytesMaskOp(originVar, castedVar, castedTo),
   RShiftBytes(castedVar, toVar, shiftedBy).
+
+// TODO: Bounds check
+HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy + moreShift, castedTo):-
+  HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
+  RShiftBytes(tmpVar, toVar, moreShift).
+
+// TODO: Bounds check
+HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy - moreShift, castedTo):-
+  HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
+  LShiftBytes(tmpVar, toVar, moreShift).
+
 /**
   Optimized pattern like so:
     0xa4: va4 = SHL v9f(0xa0), v84
diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 8323a93a..28d1056d 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -199,6 +199,13 @@ Variable_StorageIndex(def, $ConstArrayAccessIndex(parentIndex, arraySize, checke
   ADDFix(_, var, checkedVar, def),
   RevertEnforcesEnum(checkedVar, arraySize, _).
 
+Variable_StorageIndex(def, $ConstArrayAccessIndex(parentIndex, arraySize, checkedVarDiv)):-
+  Variable_StorageIndex(var, parentIndex),
+  ADDFix(_, var, checkedVarDiv, def),
+  DIV(_, checkedVar, const, checkedVarDiv),
+  Variable_Value(const, _),
+  RevertEnforcesEnum(checkedVar, arraySize, _).
+
 StorageIndex_StorageConstruct($ConstantIndex(val), $Constant(val)):-
   ActualStorageIndex($ConstantIndex(val)).
 
@@ -454,9 +461,21 @@ DataStructure_Type($ConstArray(parentCons, arraySize), cat(type, cat("[", cat(to
 StorageVariable_IntermTypeDone(numOfFacts):-
   numOfFacts = count : StorageVariable_IntermType(_, _).
 
-StorageVariable_Type(var, type):-
+StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
+
+StorageVariable_Type($Variable(cons), type):-
   StorageVariable_IntermTypeDone(_),
-  StorageVariable_IntermType(var, type).
+  StorageVariable_IntermType($Variable(cons), type),
+  !IsPackedArray(cons, _).
+
+// Hack for PackedArrays, to fix at a later point!
+// Should perhaps handle these with a special Variable construct type
+StorageVariable_Type($Variable(cons), cat("uint", to_string(8*width))):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($Variable(cons), _),
+  IsPackedArray(cons, width).
 
 .decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
 DEBUG_OUTPUT(StorageVariableToAlias)
@@ -924,3 +943,32 @@ ArrayDeleteLoop(loop, sstore, array):-
   StorageStmtToIndexAndConstruct(lenDefStmt, "LENGTH", _, array),
   SSTORE(sstore, phiVar, zeroVar),
   Variable_Value(zeroVar, "0x0").
+
+.decl IsPackedArray(cons: StorageConstruct, byteWidth: number)
+DEBUG_OUTPUT(IsPackedArray)
+
+IsPackedArray(cons, byteWidth):-
+  SLOAD(_, sindexVar, loadedVar),
+  Variable_StorageIndex(sindexVar, $ConstArrayAccessIndex(parIndex, arraySize, indexVar)),
+  StorageIndex_StorageConstruct($ConstArrayAccessIndex(parIndex, arraySize, indexVar), cons),
+  VarDivByConstant(actualIndex, const, indexVar),
+  MOD(_, actualIndex, constVar, modVar),
+  Variable_Value(constVar, const),
+  VarTimesConstant(modVar, const2, modTimesVar),
+  EXP(_, expConst, modTimesVar, shiftVal),
+  Variable_Value(expConst, "0x100"),
+  DIV(_, loadedVar, shiftVal, shiftedVar),
+  const2 = as(@div_256("0x20", const), Value),
+  LowBytesMaskOp(shiftedVar, castedVar, byteWidth).
+
+IsPackedArray(cons, @hex_to_number(@div_256("0x20", const))):-
+  SLOAD(_, sindexVar, loadedVar),
+  Variable_StorageIndex(sindexVar, $ConstArrayAccessIndex(parIndex, arraySize, indexVar)),
+  StorageIndex_StorageConstruct($ConstArrayAccessIndex(parIndex, arraySize, indexVar), cons),
+  VarDivByConstant(actualIndex, const, indexVar),
+  AND(_, actualIndex, constVar, tmp),
+  Variable_Value(constVar, as(@sub_256(const, "0x1"), Value)),
+  EXP(_, expConst, tmp, shiftVal),
+  Variable_Value(expConst, "0x100"),
+  DIV(_, loadedVar, shiftVal, shiftedVar),
+  LowBytesMaskOp(shiftedVar, castedVar, @hex_to_number(@div_256("0x20", const))).
\ No newline at end of file

From 1912c627d17261daf33a00190fde80f148c14360 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 6 Nov 2024 04:19:09 +0200
Subject: [PATCH 21/53] support packed arrays

---
 clientlib/storage_modeling/data_structures.dl | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 28d1056d..9c1bd5c6 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -949,8 +949,10 @@ DEBUG_OUTPUT(IsPackedArray)
 
 IsPackedArray(cons, byteWidth):-
   SLOAD(_, sindexVar, loadedVar),
-  Variable_StorageIndex(sindexVar, $ConstArrayAccessIndex(parIndex, arraySize, indexVar)),
-  StorageIndex_StorageConstruct($ConstArrayAccessIndex(parIndex, arraySize, indexVar), cons),
+  Variable_StorageIndex(sindexVar, sindex),
+  ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
+  sindex = $ArrayAccessIndex(parIndex, indexVar)),
+  StorageIndex_StorageConstruct(sindex, cons),
   VarDivByConstant(actualIndex, const, indexVar),
   MOD(_, actualIndex, constVar, modVar),
   Variable_Value(constVar, const),
@@ -963,8 +965,10 @@ IsPackedArray(cons, byteWidth):-
 
 IsPackedArray(cons, @hex_to_number(@div_256("0x20", const))):-
   SLOAD(_, sindexVar, loadedVar),
-  Variable_StorageIndex(sindexVar, $ConstArrayAccessIndex(parIndex, arraySize, indexVar)),
-  StorageIndex_StorageConstruct($ConstArrayAccessIndex(parIndex, arraySize, indexVar), cons),
+  Variable_StorageIndex(sindexVar, sindex),
+  ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
+  sindex = $ArrayAccessIndex(parIndex, indexVar)),
+  StorageIndex_StorageConstruct(sindex, cons),
   VarDivByConstant(actualIndex, const, indexVar),
   AND(_, actualIndex, constVar, tmp),
   Variable_Value(constVar, as(@sub_256(const, "0x1"), Value)),

From 261f6a5f217d320a766e05a2873c3309f6bc2732 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 6 Nov 2024 13:07:54 +0200
Subject: [PATCH 22/53] commnt out imprecise rules

---
 clientlib/casts_shifts.dl | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/clientlib/casts_shifts.dl b/clientlib/casts_shifts.dl
index b28169bc..5b7d376a 100644
--- a/clientlib/casts_shifts.dl
+++ b/clientlib/casts_shifts.dl
@@ -149,14 +149,14 @@ HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy, castedTo):-
   RShiftBytes(castedVar, toVar, shiftedBy).
 
 // TODO: Bounds check
-HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy + moreShift, castedTo):-
-  HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
-  RShiftBytes(tmpVar, toVar, moreShift).
+// HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy + moreShift, castedTo):-
+//   HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
+//   RShiftBytes(tmpVar, toVar, moreShift).
 
 // TODO: Bounds check
-HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy - moreShift, castedTo):-
-  HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
-  LShiftBytes(tmpVar, toVar, moreShift).
+// HighBytesCastedAndRightShiftedVar(originVar, toVar, shiftedBy - moreShift, castedTo):-
+//   HighBytesCastedAndRightShiftedVar(originVar, tmpVar, shiftedBy, castedTo),
+//   LShiftBytes(tmpVar, toVar, moreShift).
 
 /**
   Optimized pattern like so:

From 08069dadc167791d5b261230a92017bab5f9982d Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 13:13:16 +0200
Subject: [PATCH 23/53] remove warn

---
 clientlib/storage_modeling/data_structures.dl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 9c1bd5c6..dec95d79 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -952,6 +952,7 @@ IsPackedArray(cons, byteWidth):-
   Variable_StorageIndex(sindexVar, sindex),
   ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
   sindex = $ArrayAccessIndex(parIndex, indexVar)),
+  parIndex=parIndex,
   StorageIndex_StorageConstruct(sindex, cons),
   VarDivByConstant(actualIndex, const, indexVar),
   MOD(_, actualIndex, constVar, modVar),
@@ -968,6 +969,7 @@ IsPackedArray(cons, @hex_to_number(@div_256("0x20", const))):-
   Variable_StorageIndex(sindexVar, sindex),
   ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
   sindex = $ArrayAccessIndex(parIndex, indexVar)),
+  parIndex=parIndex,
   StorageIndex_StorageConstruct(sindex, cons),
   VarDivByConstant(actualIndex, const, indexVar),
   AND(_, actualIndex, constVar, tmp),

From 8756a6ef327da9baeccdac4bbf959bfb4ae030b6 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 16:05:41 +0200
Subject: [PATCH 24/53] Break type_inference into a different file

---
 clientlib/storage_modeling/data_structures.dl | 277 -----------------
 .../storage_modeling/storage_modeling.dl      |   1 +
 clientlib/storage_modeling/type_inference.dl  | 282 ++++++++++++++++++
 3 files changed, 283 insertions(+), 277 deletions(-)
 create mode 100644 clientlib/storage_modeling/type_inference.dl

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index dec95d79..f5fcd5aa 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -84,13 +84,6 @@
 
 // Note: Can probably be unified with `StorageVariable_Type`
 .decl DataStructure_Type(cons: StorageConstruct, type: symbol)
-// Note: Can probably be unified with `DataStructure_Type`
-.decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
-
-// Added interm relation that can results removed via subsumption
-.decl StorageVariable_IntermType(cons: StorageConstruct, type: symbol) btree_delete
-
-.decl StorageVariable_IntermTypeDone(numOfFacts: number)
 
 // Doesn't contain TightlyPackedVariable, maybe revisit
 .decl StorageConstruct_ParentAndOffset(cons: StorageConstruct, parentCons: StorageConstruct, offset: number)
@@ -458,276 +451,6 @@ DataStructure_Type($Array(parentCons), "string"):-
 DataStructure_Type($ConstArray(parentCons, arraySize), cat(type, cat("[", cat(to_string(arraySize), "]")))):-
   DataStructure_ValueOrElementType($ConstArray(parentCons, arraySize), type).
 
-StorageVariable_IntermTypeDone(numOfFacts):-
-  numOfFacts = count : StorageVariable_IntermType(_, _).
-
-StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
-  StorageVariable_IntermTypeDone(_),
-  StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
-
-StorageVariable_Type($Variable(cons), type):-
-  StorageVariable_IntermTypeDone(_),
-  StorageVariable_IntermType($Variable(cons), type),
-  !IsPackedArray(cons, _).
-
-// Hack for PackedArrays, to fix at a later point!
-// Should perhaps handle these with a special Variable construct type
-StorageVariable_Type($Variable(cons), cat("uint", to_string(8*width))):-
-  StorageVariable_IntermTypeDone(_),
-  StorageVariable_IntermType($Variable(cons), _),
-  IsPackedArray(cons, width).
-
-.decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
-DEBUG_OUTPUT(StorageVariableToAlias)
-
-StorageVariableToAlias(storVar, alias):-
-  ProcessedStorageVariable(storVar, storVar),
-  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  uint256AliasFlowAnalysis.GlobalFlows(var, alias).
-
-StorageVariableToAlias(storVar, alias):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  (
-    uint256AliasFlowAnalysis.GlobalFlows(alias, var);
-    uint256AliasFlowAnalysis.GlobalFlows(var, alias)
-  ).
-
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  instances = count : StorageVariableToAlias(storVar, _),
-  instances < 4.
-
-StorageVariable_IntermType(var, "bytes32"):-
-  IsStorageConstruct(var),
-  var = $Variable(cons), cons = cons,
-  ProcessedStorageVariable(var, var).
-
-StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes != 20,
-  widthBytes != 1,
-  type = cat("uint", to_string(widthBytes * 8)).
-
-StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  widthBytes = 1 + byteHigh - byteLow,
-  widthBytes = 20.
-
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-// IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
-  StorageVariable_IntermType(storVar2, "uint256").
-  .plan 0:(6,5,4,3,2,1)
-
-// IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  StorageVariable_IntermType(storVar2, "uint256"),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar2),
-  SSTORE(store, _, uintVar),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  ProcessedStorageVariable(storVar, storVar).
-
-
-// IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  ConstWrittenToBytesOfStorVar(_, constVal, _, _, storVar, 0, 31),
-  strlen(constVal) < 60. //is right aligned
-
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
-
-StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
-
-StorageVariable_IntermType(storVar, "bytes32") <= StorageVariable_IntermType(storVar, "uint256"):- 1=1.
-
-StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
-
-IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
-StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
-  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
-  uint8AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-.decl IsUint(storVar: StorageConstruct, uintVar: Variable)
-.output IsUint
-
-IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), uintVar),
-StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),
-  20 = 1 + byteHigh - byteLow,
-  uint160flowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar).
-
-StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
-  ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),
-  constVal != "0x0", constVal != "0x1".
-
-StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
-  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
-  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  Variable_Value(uintVar, constVal),
-  constVal != "0x0", constVal != "0x1".
-
-IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
-StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
-  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
-  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-StorageVariable_IntermType(var, type):-
-  StorageVariable_IntermType(packedVar, type),
-  ProcessedStorageVariable(var, packedVar),
-  IsStorageConstruct(var),
-  1 = count: ProcessedStorageVariable(var, _).
-
-.decl UintVar(var: Variable)
-UintVar(var):-
-  Statement_Uses(stmt, var, _),
-  (
-    ActualBinArithStmt(stmt);
-    (Statement_Opcode(stmt, op),
-    (op = "LT"; op = "GT"))
-  ).
-
-UintVar(var):-
-  ActualBinArithStmt(stmt),
-  Statement_Defines(stmt, var, _).
-
-UintVar(var):-
-  GAS(_, var);
-  CALLVALUE(_, var);
-  TIMESTAMP(_, var);
-  DIFFICULTY(_, var);
-  NUMBER(_, var);
-  BALANCE(_, _, var).
-
-.decl ActualBinArithStmt(stmt: Statement)
-
-ActualBinArithStmt(stmt):-
-  Statement_Opcode(stmt, op),
-  (op = "MOD" ; op = "EXP"; op = "ADDMOD"; op = "MULMOD").
-
-ActualBinArithStmt(stmt):-
-  (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),
-  Statement_Defines(stmt, to, 0),
-  !LShiftBytes(_, to, _).
-
-ActualBinArithStmt(stmt):-
-  (Statement_Opcode(stmt, "DIV"); Statement_Opcode(stmt, "SHR")),
-  Statement_Defines(stmt, to, 0),
-  !RShiftBytes(_, to, _).
-
-ActualBinArithStmt(stmt):-
-  SUB(stmt, _, _, to),
-  !ISZERO(_, to, _),
-  !JUMPI(_, _, to).
-
-ActualBinArithStmt(stmt):-
-  ADD(stmt, _, _, to),
-  !ISZERO(_, to, _),
-  !JUMPI(_, _, to).
-
-.decl GlobalStructFlowsBase(from: Variable, to: Variable)
-GlobalStructFlowsBase(storedVar, loadedVar):-
-  StructLoad(_, structBase, wordOffset, loadedVar),
-  VarPointsToStruct(_, structBase, heapCtx, structId),
-  VarPointsToStruct(_, structBaseAlias, heapCtx, structId),
-  StructStore(_, structBaseAlias, wordOffset, storedVar).
-
-.init uint8AliasFlowAnalysis = GlobalFlowAnalysis
-uint8AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
-uint8AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
-
-uint8AliasFlowAnalysis.TransferStmt(stmt):-
-  Statement_Defines(stmt, to, 0),
-  LowBytesMaskOp(_, to, castedTo),
-  // allow things to be upcasted for completeness
-  castedTo >= 1.
-
-uint8AliasFlowAnalysis.TransferStmt(stmt):-
-  PHI(stmt, _, to),
-  nUses = count: PHITrans(_, to),
-  nUses < 4.
-
-uint8AliasFlowAnalysis.FlowsBase(from, to):-
-  GlobalStructFlowsBase(from, to).
-
-.init uint160flowAnalysis = GlobalFlowAnalysis
-uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
-uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
-
-// uint160flowAnalysis.TransferStmt(stmt):- ActualBinArithStmt(stmt).
-
-uint160flowAnalysis.TransferStmt(stmt):-
-  Statement_Defines(stmt, to, 0),
-  LowBytesMaskOp(_, to, castedTo),
-  // allow things to be upcasted for completeness
-  castedTo >= 20.
-
-uint160flowAnalysis.TransferStmt(stmt):-
-  PHI(stmt, _, to),
-  nUses = count: PHITrans(_, to),
-  nUses < 4.
-
-.output uint256AliasFlowAnalysis.GlobalFlows
-
-.init uint256AliasFlowAnalysis = GlobalFlowAnalysis
-uint256AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
-uint256AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
-
-uint256AliasFlowAnalysis.TransferStmt(stmt):-
-  Statement_Defines(stmt, to, 0),
-  LowBytesMaskOp(_, to, castedTo),
-  // allow things to be upcasted for completeness
-  castedTo >= 30.
-
-uint256AliasFlowAnalysis.TransferStmt(stmt):-
-  PHI(stmt, _, to),
-  nUses = count: PHITrans(_, to),
-  nUses < 4.
-
 // // Disable general rule for now
 // StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $Variable(cons)):-
 //   LikelyVariableLoadingStorageIndex(index),
diff --git a/clientlib/storage_modeling/storage_modeling.dl b/clientlib/storage_modeling/storage_modeling.dl
index cb00332a..1f461795 100644
--- a/clientlib/storage_modeling/storage_modeling.dl
+++ b/clientlib/storage_modeling/storage_modeling.dl
@@ -13,5 +13,6 @@
 
 #include "data_structures.dl"
 #include "tight_packing.dl"
+#include "type_inference.dl"
 #include "legacy_data_structures.dl"
 #include "metrics.dl"
\ No newline at end of file
diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
new file mode 100644
index 00000000..0bd19b3e
--- /dev/null
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -0,0 +1,282 @@
+
+// Note: Can probably be unified with `DataStructure_Type`
+.decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
+
+// Added interm relation that can results removed via subsumption
+.decl StorageVariable_IntermType(cons: StorageConstruct, type: symbol) btree_delete
+
+// This relation is needed to ensure that the propagation of allsou
+.decl StorageVariable_IntermTypeDone(numOfFacts: number)
+
+
+
+StorageVariable_IntermTypeDone(numOfFacts):-
+  numOfFacts = count : StorageVariable_IntermType(_, _).
+
+StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type).
+
+StorageVariable_Type($Variable(cons), type):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($Variable(cons), type),
+  !IsPackedArray(cons, _).
+
+// Hack for PackedArrays, to fix at a later point!
+// Should perhaps handle these with a special Variable construct type
+StorageVariable_Type($Variable(cons), cat("uint", to_string(8*width))):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($Variable(cons), _),
+  IsPackedArray(cons, width).
+
+
+.decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
+DEBUG_OUTPUT(StorageVariableToAlias)
+
+StorageVariableToAlias(storVar, alias):-
+  ProcessedStorageVariable(storVar, storVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  uint256AliasFlowAnalysis.GlobalFlows(var, alias).
+
+StorageVariableToAlias(storVar, alias):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  (
+    uint256AliasFlowAnalysis.GlobalFlows(alias, var);
+    uint256AliasFlowAnalysis.GlobalFlows(var, alias)
+  ).
+
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  instances = count : StorageVariableToAlias(storVar, _),
+  instances < 4.
+
+StorageVariable_IntermType(var, "bytes32"):-
+  IsStorageConstruct(var),
+  var = $Variable(cons), cons = cons,
+  ProcessedStorageVariable(var, var).
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  widthBytes = 1 + byteHigh - byteLow,
+  widthBytes != 20,
+  widthBytes != 1,
+  type = cat("uint", to_string(widthBytes * 8)).
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  widthBytes = 1 + byteHigh - byteLow,
+  widthBytes = 20.
+
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
+  StorageVariable_IntermType(storVar2, "uint256").
+  .plan 0:(6,5,4,3,2,1)
+
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  StorageVariable_IntermType(storVar2, "uint256"),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar2),
+  SSTORE(store, _, uintVar),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+  ProcessedStorageVariable(storVar, storVar).
+
+
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  ConstWrittenToBytesOfStorVar(_, constVal, _, _, storVar, 0, 31),
+  strlen(constVal) < 60. //is right aligned
+
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageStmtToIndexAndConstruct(store, _, _, storVar),
+  SSTORE(store, _, var),
+  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
+StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
+
+StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
+
+StorageVariable_IntermType(storVar, "bytes32") <= StorageVariable_IntermType(storVar, "uint256"):- 1=1.
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
+
+IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
+  uint8AliasFlowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
+.decl IsUint(storVar: StorageConstruct, uintVar: Variable)
+.output IsUint
+
+IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), uintVar),
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh),
+  20 = 1 + byteHigh - byteLow,
+  uint160flowAnalysis.GlobalFlows(var, uintVar),
+  UintVar(uintVar).
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),
+  constVal != "0x0", constVal != "0x1".
+
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
+  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  Variable_Value(uintVar, constVal),
+  constVal != "0x0", constVal != "0x1".
+
+IsUint($TightlyPackedVariable(cons, singleByte, singleByte), uintVar),
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
+  uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
+
+StorageVariable_IntermType(var, type):-
+  StorageVariable_IntermType(packedVar, type),
+  ProcessedStorageVariable(var, packedVar),
+  IsStorageConstruct(var),
+  1 = count: ProcessedStorageVariable(var, _).
+
+.decl UintVar(var: Variable)
+UintVar(var):-
+  Statement_Uses(stmt, var, _),
+  (
+    ActualBinArithStmt(stmt);
+    (Statement_Opcode(stmt, op),
+    (op = "LT"; op = "GT"))
+  ).
+
+UintVar(var):-
+  ActualBinArithStmt(stmt),
+  Statement_Defines(stmt, var, _).
+
+UintVar(var):-
+  GAS(_, var);
+  CALLVALUE(_, var);
+  TIMESTAMP(_, var);
+  DIFFICULTY(_, var);
+  NUMBER(_, var);
+  BALANCE(_, _, var).
+
+.decl ActualBinArithStmt(stmt: Statement)
+
+ActualBinArithStmt(stmt):-
+  Statement_Opcode(stmt, op),
+  (op = "MOD" ; op = "EXP"; op = "ADDMOD"; op = "MULMOD").
+
+ActualBinArithStmt(stmt):-
+  (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),
+  Statement_Defines(stmt, to, 0),
+  !LShiftBytes(_, to, _).
+
+ActualBinArithStmt(stmt):-
+  (Statement_Opcode(stmt, "DIV"); Statement_Opcode(stmt, "SHR")),
+  Statement_Defines(stmt, to, 0),
+  !RShiftBytes(_, to, _).
+
+ActualBinArithStmt(stmt):-
+  SUB(stmt, _, _, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+ActualBinArithStmt(stmt):-
+  ADD(stmt, _, _, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+.decl GlobalStructFlowsBase(from: Variable, to: Variable)
+GlobalStructFlowsBase(storedVar, loadedVar):-
+  StructLoad(_, structBase, wordOffset, loadedVar),
+  VarPointsToStruct(_, structBase, heapCtx, structId),
+  VarPointsToStruct(_, structBaseAlias, heapCtx, structId),
+  StructStore(_, structBaseAlias, wordOffset, storedVar).
+
+.init uint8AliasFlowAnalysis = GlobalFlowAnalysis
+uint8AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint8AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint8AliasFlowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
+  castedTo >= 1.
+
+uint8AliasFlowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
+uint8AliasFlowAnalysis.FlowsBase(from, to):-
+  GlobalStructFlowsBase(from, to).
+
+.init uint160flowAnalysis = GlobalFlowAnalysis
+uint160flowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+// uint160flowAnalysis.TransferStmt(stmt):- ActualBinArithStmt(stmt).
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
+  castedTo >= 20.
+
+uint160flowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
+.output uint256AliasFlowAnalysis.GlobalFlows
+
+.init uint256AliasFlowAnalysis = GlobalFlowAnalysis
+uint256AliasFlowAnalysis.InitialFlowVar(v) :- isVariable(v).
+uint256AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
+
+uint256AliasFlowAnalysis.TransferStmt(stmt):-
+  Statement_Defines(stmt, to, 0),
+  LowBytesMaskOp(_, to, castedTo),
+  // allow things to be upcasted for completeness
+  castedTo >= 30.
+
+uint256AliasFlowAnalysis.TransferStmt(stmt):-
+  PHI(stmt, _, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.

From 72bef3366b6ea7edf8b59598e5751f30cfc9e527 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 16:32:00 +0200
Subject: [PATCH 25/53] Make alias propagation more precise

---
 clientlib/storage_modeling/type_inference.dl | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 0bd19b3e..105eadb7 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -236,6 +236,7 @@ uint8AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
 uint8AliasFlowAnalysis.TransferStmt(stmt):-
   Statement_Defines(stmt, to, 0),
   LowBytesMaskOp(_, to, castedTo),
+  !SignedIntCast(_, to, castedTo), // needed because its contained in the prior
   // allow things to be upcasted for completeness
   castedTo >= 1.
 
@@ -256,6 +257,7 @@ uint160flowAnalysis.TransferBoundary(b) :- IsBlock(b).
 uint160flowAnalysis.TransferStmt(stmt):-
   Statement_Defines(stmt, to, 0),
   LowBytesMaskOp(_, to, castedTo),
+  !SignedIntCast(_, to, castedTo), // needed because its contained in the prior
   // allow things to be upcasted for completeness
   castedTo >= 20.
 
@@ -273,6 +275,7 @@ uint256AliasFlowAnalysis.TransferBoundary(b) :- IsBlock(b).
 uint256AliasFlowAnalysis.TransferStmt(stmt):-
   Statement_Defines(stmt, to, 0),
   LowBytesMaskOp(_, to, castedTo),
+  !SignedIntCast(_, to, castedTo), // needed because its contained in the prior
   // allow things to be upcasted for completeness
   castedTo >= 30.
 

From cc0d1995289e7ecf88ea449f84d0e9f7bbd84450 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 17:08:21 +0200
Subject: [PATCH 26/53] Infer intX types

---
 clientlib/storage_modeling/type_inference.dl | 66 +++++++++++++++++---
 1 file changed, 59 insertions(+), 7 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 105eadb7..8a19ed2d 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -1,4 +1,32 @@
 
+.type Type <: symbol
+
+.decl Type_Kind(type: Type, kind: symbol)
+
+.decl Type_Width(type: Type, width: number)
+DEBUG_OUTPUT(Type_Width)
+
+Type_Kind("bool", "bool").
+Type_Width("bool", 1).
+Type_Kind("address", "uint").
+Type_Width("address", 20).
+
+Type_Kind(type, "uint"),
+Type_Width(type, byteWidth):-
+  byteWidth = range(1, 33),
+  type = cat("uint", to_string(byteWidth*8)).
+
+Type_Kind(type, "int"),
+Type_Width(type, byteWidth):-
+  byteWidth = range(1, 33),
+  type = cat("int", to_string(byteWidth*8)).
+
+Type_Kind(type, "bytes"),
+Type_Width(type, byteWidth):-
+  byteWidth = range(1, 33),
+  type = cat("bytes", to_string(byteWidth)).
+
+
 // Note: Can probably be unified with `DataStructure_Type`
 .decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
 
@@ -30,6 +58,17 @@ StorageVariable_Type($Variable(cons), cat("uint", to_string(8*width))):-
   IsPackedArray(cons, width).
 
 
+StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
+
+StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
+
+StorageVariable_IntermType(storVar, "bytes32") <= StorageVariable_IntermType(storVar, "uint256"):- 1=1.
+
+StorageVariable_IntermType(storVar, uintType) <= StorageVariable_IntermType(storVar, intType):-
+  Type_Kind(uintType, "uint"),
+  Type_Kind(intType, "int").
+
+
 .decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
 DEBUG_OUTPUT(StorageVariableToAlias)
 
@@ -52,6 +91,18 @@ StorageVariable_IntermType(storVar, "uint256"):-
   instances = count : StorageVariableToAlias(storVar, _),
   instances < 4.
 
+
+StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), alias):-
+  ProcessedStorageVariable(storVar, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, byteLow, byteHigh),
+  uint256AliasFlowAnalysis.GlobalFlows(var, alias).
+
+StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), alias):-
+  ProcessedStorageVariable(storVar, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  VarWrittenToBytesOfStorVarFinal(var, _, storVar, byteLow, byteHigh),
+  (uint256AliasFlowAnalysis.GlobalFlows(var, alias);
+  uint256AliasFlowAnalysis.GlobalFlows(alias, var)).
+
 StorageVariable_IntermType(var, "bytes32"):-
   IsStorageConstruct(var),
   var = $Variable(cons), cons = cons,
@@ -64,6 +115,13 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type
   widthBytes != 1,
   type = cat("uint", to_string(widthBytes * 8)).
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), aliasVar),
+  SignedIntCast(aliasVar, _, _),
+  widthBytes = 1 + byteHigh - byteLow,
+  type = cat("int", to_string(widthBytes * 8)).
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,
@@ -121,12 +179,6 @@ StorageVariable_IntermType(storVar, "uint256"):-
   UintVar(uintVar),
   !Variable_Value(uintVar, _).
 
-StorageVariable_IntermType(storVar, "bool") <= StorageVariable_IntermType(storVar, "uint8"):- 1=1.
-
-StorageVariable_IntermType(storVar, "address") <= StorageVariable_IntermType(storVar, "uint160"):- 1=1.
-
-StorageVariable_IntermType(storVar, "bytes32") <= StorageVariable_IntermType(storVar, "uint256"):- 1=1.
-
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
 
@@ -277,7 +329,7 @@ uint256AliasFlowAnalysis.TransferStmt(stmt):-
   LowBytesMaskOp(_, to, castedTo),
   !SignedIntCast(_, to, castedTo), // needed because its contained in the prior
   // allow things to be upcasted for completeness
-  castedTo >= 30.
+  castedTo >= 2.
 
 uint256AliasFlowAnalysis.TransferStmt(stmt):-
   PHI(stmt, _, to),

From 8bf9253d3e00e3e0038e371f54652998369de6e2 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 18:26:28 +0200
Subject: [PATCH 27/53] better support for int256

---
 clientlib/storage_modeling/type_inference.dl | 25 ++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 8a19ed2d..d727d2c9 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -122,6 +122,19 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type
   widthBytes = 1 + byteHigh - byteLow,
   type = cat("int", to_string(widthBytes * 8)).
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), aliasVar),
+  SignedIntVar(aliasVar),
+  widthBytes = 1 + byteHigh - byteLow,
+  type = cat("int", to_string(widthBytes * 8)).
+
+StorageVariable_IntermType(storVar, "int256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageVariableToAlias(storVar, aliasVar),
+  SignedIntVar(aliasVar).
+
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,
@@ -274,6 +287,18 @@ ActualBinArithStmt(stmt):-
   !ISZERO(_, to, _),
   !JUMPI(_, _, to).
 
+.decl SignedIntVar(intVar: Variable)
+
+SignedIntVar(intVar):-
+  Statement_Opcode(stmt, op),
+  (op = "SMOD" ; op = "SDIV"; op = "SGT"; op = "SLT"),
+  Statement_Uses(stmt, intVar, _).
+
+SignedIntVar(intVar):-
+  Statement_Opcode(stmt, op),
+  (op = "SMOD" ; op = "SDIV"),
+  Statement_Defines(stmt, intVar, _).
+
 .decl GlobalStructFlowsBase(from: Variable, to: Variable)
 GlobalStructFlowsBase(storedVar, loadedVar):-
   StructLoad(_, structBase, wordOffset, loadedVar),

From 5aa27eb7a4dcd909573081012578f642c02a3afb Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 19:56:15 +0200
Subject: [PATCH 28/53] Resolve type conflicts

---
 clientlib/storage_modeling/type_inference.dl | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index d727d2c9..2dbf031d 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -68,6 +68,13 @@ StorageVariable_IntermType(storVar, uintType) <= StorageVariable_IntermType(stor
   Type_Kind(uintType, "uint"),
   Type_Kind(intType, "int").
 
+StorageVariable_IntermType(storVar, bytesType) <= StorageVariable_IntermType(storVar, intType):-
+  Type_Kind(bytesType, "bytes"),
+  Type_Kind(intType, "int").
+
+StorageVariable_IntermType(storVar, bytesType) <= StorageVariable_IntermType(storVar, uintType):-
+  Type_Kind(bytesType, "bytes"),
+  Type_Kind(uintType, "uint").
 
 .decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
 DEBUG_OUTPUT(StorageVariableToAlias)

From f8a9a841990906ab136ab80f6de1ba9c6fd05f42 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 7 Nov 2024 19:57:21 +0200
Subject: [PATCH 29/53] Refine uint8, uint160 inference

---
 clientlib/storage_modeling/type_inference.dl | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 2dbf031d..517cb043 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -207,7 +207,7 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte),
   uint8AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
+  Uint8Var(uintVar),
   !Variable_Value(uintVar, _).
 
 .decl IsUint(storVar: StorageConstruct, uintVar: Variable)
@@ -238,7 +238,7 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte),
   uint8AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  UintVar(uintVar),
+  Uint8Var(uintVar),
   !Variable_Value(uintVar, _).
 
 StorageVariable_IntermType(var, type):-
@@ -250,11 +250,7 @@ StorageVariable_IntermType(var, type):-
 .decl UintVar(var: Variable)
 UintVar(var):-
   Statement_Uses(stmt, var, _),
-  (
-    ActualBinArithStmt(stmt);
-    (Statement_Opcode(stmt, op),
-    (op = "LT"; op = "GT"))
-  ).
+  ActualBinArithStmt(stmt).
 
 UintVar(var):-
   ActualBinArithStmt(stmt),
@@ -268,6 +264,16 @@ UintVar(var):-
   NUMBER(_, var);
   BALANCE(_, _, var).
 
+// Added comparizons to UintVar results, as they're useful to distinguish bool and uint8
+.decl Uint8Var(var: Variable)
+Uint8Var(var):-
+  Statement_Uses(stmt, var, _),
+  Statement_Opcode(stmt, op),
+  (op = "LT"; op= "GT").
+
+Uint8Var(var):-
+  UintVar(var).
+
 .decl ActualBinArithStmt(stmt: Statement)
 
 ActualBinArithStmt(stmt):-

From 5a162710cc8d2aa460d84d4e438ecee4cfc0c1b7 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 8 Nov 2024 03:31:49 +0200
Subject: [PATCH 30/53] make uint160 and uint256 type inf more general

---
 clientlib/storage_modeling/type_inference.dl | 23 ++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 517cb043..75944686 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -141,6 +141,23 @@ StorageVariable_IntermType(storVar, "int256"):-
   StorageVariableToAlias(storVar, aliasVar),
   SignedIntVar(aliasVar).
 
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageVariableToAlias(storVar, aliasVar),
+  Statement_Uses(stmt, aliasVar, i),
+  Statement_Uses(stmt, uintVar, 1 - i),
+  UintVar(uintVar),
+  Statement_Opcode(stmt, op),
+  (op = "LT"; op= "GT"; op = "EQ"),
+  !Variable_Value(uintVar, _).
+
+IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageVariableToAlias(storVar, uintVar),
+  UintVar(uintVar),
+  !Variable_Value(uintVar, _).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
@@ -356,6 +373,9 @@ uint160flowAnalysis.TransferStmt(stmt):-
   nUses = count: PHITrans(_, to),
   nUses < 4.
 
+uint160flowAnalysis.FlowsBase(from, to):-
+  GlobalStructFlowsBase(from, to).
+
 .output uint256AliasFlowAnalysis.GlobalFlows
 
 .init uint256AliasFlowAnalysis = GlobalFlowAnalysis
@@ -373,3 +393,6 @@ uint256AliasFlowAnalysis.TransferStmt(stmt):-
   PHI(stmt, _, to),
   nUses = count: PHITrans(_, to),
   nUses < 4.
+
+uint256AliasFlowAnalysis.FlowsBase(from, to):-
+  GlobalStructFlowsBase(from, to).
\ No newline at end of file

From 97a87fd0f838cd2b7d16873519dfe0d6f53a5b91 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 8 Nov 2024 04:23:51 +0200
Subject: [PATCH 31/53] minor improvement

---
 clientlib/storage_modeling/type_inference.dl | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 75944686..d022d725 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -152,6 +152,18 @@ StorageVariable_IntermType(storVar, "uint256"):-
   (op = "LT"; op= "GT"; op = "EQ"),
   !Variable_Value(uintVar, _).
 
+// IsUint(storVar, uintVar),
+StorageVariable_IntermType(storVar, "uint256"):-
+  ProcessedStorageVariable(storVar, storVar),
+  StorageVariableToAlias(storVar, aliasVar),
+  Statement_Uses(stmt, aliasVar, i),
+  Statement_Uses(stmt, otherAliasVar, 1 - i),
+  StorageVariableToAlias(storVar2, otherAliasVar),
+  StorageVariable_IntermType(storVar2, "uint256"),
+  Statement_Opcode(stmt, op),
+  (op = "LT"; op= "GT"; op = "EQ").
+
+
 IsUint(storVar, uintVar),
 StorageVariable_IntermType(storVar, "uint256"):-
   ProcessedStorageVariable(storVar, storVar),

From 1a057a0a960a97e54512c9220ccc98c7b970984f Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 8 Nov 2024 04:59:15 +0200
Subject: [PATCH 32/53] increase completeness of UintVar

---
 clientlib/storage_modeling/type_inference.dl | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index d022d725..c92d5cf2 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -149,8 +149,7 @@ StorageVariable_IntermType(storVar, "uint256"):-
   Statement_Uses(stmt, uintVar, 1 - i),
   UintVar(uintVar),
   Statement_Opcode(stmt, op),
-  (op = "LT"; op= "GT"; op = "EQ"),
-  !Variable_Value(uintVar, _).
+  (op = "LT"; op= "GT"; op = "EQ").
 
 // IsUint(storVar, uintVar),
 StorageVariable_IntermType(storVar, "uint256"):-
@@ -293,6 +292,11 @@ UintVar(var):-
   NUMBER(_, var);
   BALANCE(_, _, var).
 
+UintVar(var):-
+  Variable_Value(var, value),
+  value != "0x0", value != "0x1",
+  strlen(value) < 30.
+
 // Added comparizons to UintVar results, as they're useful to distinguish bool and uint8
 .decl Uint8Var(var: Variable)
 Uint8Var(var):-

From b955e4f2d8ee55a16a7f7f1c8b406dc5bfdacbc8 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 11 Nov 2024 19:31:32 +0200
Subject: [PATCH 33/53] init commit of rewrite

---
 clientlib/storage_modeling/type_inference.dl | 250 ++++++++++++++-----
 1 file changed, 183 insertions(+), 67 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index c92d5cf2..ce19c4c7 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -141,66 +141,66 @@ StorageVariable_IntermType(storVar, "int256"):-
   StorageVariableToAlias(storVar, aliasVar),
   SignedIntVar(aliasVar).
 
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageVariableToAlias(storVar, aliasVar),
-  Statement_Uses(stmt, aliasVar, i),
-  Statement_Uses(stmt, uintVar, 1 - i),
-  UintVar(uintVar),
-  Statement_Opcode(stmt, op),
-  (op = "LT"; op= "GT"; op = "EQ").
-
 // IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageVariableToAlias(storVar, aliasVar),
-  Statement_Uses(stmt, aliasVar, i),
-  Statement_Uses(stmt, otherAliasVar, 1 - i),
-  StorageVariableToAlias(storVar2, otherAliasVar),
-  StorageVariable_IntermType(storVar2, "uint256"),
-  Statement_Opcode(stmt, op),
-  (op = "LT"; op= "GT"; op = "EQ").
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageVariableToAlias(storVar, aliasVar),
+//   Statement_Uses(stmt, aliasVar, i),
+//   Statement_Uses(stmt, uintVar, 1 - i),
+//   UintVar(uintVar),
+//   Statement_Opcode(stmt, op),
+//   (op = "LT"; op= "GT"; op = "EQ").
+
+// // IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageVariableToAlias(storVar, aliasVar),
+//   Statement_Uses(stmt, aliasVar, i),
+//   Statement_Uses(stmt, otherAliasVar, 1 - i),
+//   StorageVariableToAlias(storVar2, otherAliasVar),
+//   StorageVariable_IntermType(storVar2, "uint256"),
+//   Statement_Opcode(stmt, op),
+//   (op = "LT"; op= "GT"; op = "EQ").
 
 
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageVariableToAlias(storVar, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
+// IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageVariableToAlias(storVar, uintVar),
+//   UintVar(uintVar),
+//   !Variable_Value(uintVar, _).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,
   widthBytes = 20.
 
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
-
-// IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
-  StorageVariable_IntermType(storVar2, "uint256").
-  .plan 0:(6,5,4,3,2,1)
-
 // IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  StorageVariable_IntermType(storVar2, "uint256"),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar2),
-  SSTORE(store, _, uintVar),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  ProcessedStorageVariable(storVar, storVar).
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+//   UintVar(uintVar),
+//   !Variable_Value(uintVar, _).
+
+// // IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
+//   SSTORE(store, _, var),
+//   uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+//   VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
+//   StorageVariable_IntermType(storVar2, "uint256").
+//   .plan 0:(6,5,4,3,2,1)
+
+// // IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   StorageVariable_IntermType(storVar2, "uint256"),
+//   StorageStmtToIndexAndConstruct(store, _, _, storVar2),
+//   SSTORE(store, _, uintVar),
+//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+//   VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
+//   ProcessedStorageVariable(storVar, storVar).
 
 
 // IsUint(storVar, uintVar),
@@ -209,23 +209,23 @@ StorageVariable_IntermType(storVar, "uint256"):-
   ConstWrittenToBytesOfStorVar(_, constVal, _, _, storVar, 0, 31),
   strlen(constVal) < 60. //is right aligned
 
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
+// IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
+//   SSTORE(store, _, var),
+//   uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
+//   UintVar(uintVar),
+//   !Variable_Value(uintVar, _).
 
-IsUint(storVar, uintVar),
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-  UintVar(uintVar),
-  !Variable_Value(uintVar, _).
+// IsUint(storVar, uintVar),
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
+//   SSTORE(store, _, var),
+//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
+//   UintVar(uintVar),
+//   !Variable_Value(uintVar, _).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
@@ -411,4 +411,120 @@ uint256AliasFlowAnalysis.TransferStmt(stmt):-
   nUses < 4.
 
 uint256AliasFlowAnalysis.FlowsBase(from, to):-
-  GlobalStructFlowsBase(from, to).
\ No newline at end of file
+  GlobalStructFlowsBase(from, to).
+
+.decl ComparisonOperation(stmt: Statement, var1: Variable, var2: Variable)
+DEBUG_OUTPUT(ComparisonOperation)
+
+ComparisonOperation(stmt, var1, var2):-
+  Statement_Opcode(stmt, op),
+  (op = "LT"; op= "GT"; op = "EQ"),
+  Statement_Uses(stmt, var1, i),
+  Statement_Uses(stmt, var2, 1 - i).
+
+.decl VariableUsedAs(var: Variable, typeKind: symbol)
+DEBUG_OUTPUT(VariableUsedAs)
+
+.decl VariableUsedAsBase(var: Variable, typeKind: symbol)
+DEBUG_OUTPUT(VariableUsedAsBase)
+
+VariableUsedAsBase(var, "uint"):-
+  GAS(_, var);
+  CALLVALUE(_, var);
+  TIMESTAMP(_, var);
+  DIFFICULTY(_, var);
+  NUMBER(_, var);
+  BALANCE(_, _, var).
+
+VariableUsedAsBase(var, "uint"):-
+  ActualBinArithStmt(stmt),
+  Statement_Uses(stmt, var, _).
+
+VariableUsedAsBase(var, "uint"):-
+  ActualBinArithStmt(stmt),
+  Statement_Defines(stmt, var, _).
+
+VariableUsedAsBase(lenVar, "uint"):-
+  ArrayLengthVar(_, lenVar);
+  ArrayAllocation(_, _, lenVar).
+
+VariableUsedAsBase(var, "bytes"):-
+  SHA3(_, _, _, var),
+  BLOCKHASH(_, _, var);
+  EXTCODEHASH(_, _, var).
+
+VariableUsedAsBase(var, "uint"):-
+  ComparisonOperation(_, var, otherVar),
+  Variable_Value(otherVar, val),
+  val != "0x0", val != "0x1",
+  strlen(val) < 30. // right aligned val
+
+VariableUsedAsBase(var, "bytes"):-
+  ComparisonOperation(_, var, otherVar),
+  Variable_Value(otherVar, val),
+  strlen(val) >= 65. // left aligned val (65 or 66 chars in our repr)
+
+VariableUsedAs(var, "bytes") <= VariableUsedAs(var, "uint"):- 1=1.
+
+VariableUsedAs(var, "uint") <= VariableUsedAs(var, "int"):- 1=1.
+
+VariableUsedAs(var, typeKind):-
+  VariableUsedAsBase(var, typeKind).
+
+VariableUsedAs(var, typeKind):-
+  VariableUsedAs(otherVar, typeKind),
+  ComparisonOperation(_, var, otherVar).
+
+VariableUsedAs(var, "uint"):-
+  VariableUsedAs(defVar, "uint"),
+  LowBytesMaskOp(var, defVar, castedTo),
+  !SignedIntCast(var, defVar, castedTo),
+  castedTo > 1.
+
+VariableUsedAs(defVar, "uint"):-
+  VariableUsedAs(useVar, "uint"),
+  LowBytesMaskOp(useVar, defVar, castedTo),
+  !SignedIntCast(useVar, defVar, castedTo),
+  castedTo > 1.
+
+VariableUsedAs(toVar, "bytes"):-
+  VariableUsedAs(useVar, "bytes"),
+  HighBytesMaskOp(useVar, toVar, _).
+
+VariableUsedAs(useVar, "bytes"):-
+  VariableUsedAs(toVar, "bytes"),
+  HighBytesMaskOp(useVar, toVar, _).
+
+VariableUsedAs(formalArg, typeKind):-
+  VariableUsedAs(actualArg, typeKind),
+  ActualArgs(caller, actualArg, pos),
+  CallGraphEdge(caller, fun),
+  FormalArgs(fun, formalArg, pos).
+
+VariableUsedAs(actualRet, typeKind):-
+  VariableUsedAs(formalRet, typeKind),
+  FormalReturnArgs(fun, formalRet, retPos),
+  CallGraphEdge(caller, fun),
+  ActualReturnArgs(caller, actualRet, retPos).
+
+VariableUsedAs(to, typeKind):-
+  VariableUsedAs(from, typeKind),
+  GlobalStructFlowsBase(from, to).
+
+VariableUsedAs(from, typeKind):-
+  VariableUsedAs(to, typeKind),
+  GlobalStructFlowsBase(from, to).
+
+
+
+StorageVariable_IntermType(storVar, type):-
+  VariableUsedAs(alias, typeKind),
+  StorageVariableToAlias(storVar, alias),
+  ProcessedStorageVariable(storVar, storVar),
+  Type_Kind(type, typeKind),
+  Type_Width(type, 32).
+
+VariableUsedAs(alias, typeKind):-
+  StorageVariable_IntermType(storVar, type),
+  StorageVariableToAlias(storVar, alias),
+  Type_Kind(type, typeKind).
\ No newline at end of file

From c6b11e8862aff9b12362faabd65707706b488d3b Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 11 Nov 2024 20:47:25 +0200
Subject: [PATCH 34/53] improve precision

---
 clientlib/storage_modeling/type_inference.dl | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index ce19c4c7..005cde8e 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -473,7 +473,8 @@ VariableUsedAs(var, typeKind):-
 
 VariableUsedAs(var, typeKind):-
   VariableUsedAs(otherVar, typeKind),
-  ComparisonOperation(_, var, otherVar).
+  ComparisonOperation(_, var, otherVar),
+  !Variable_Value(var, _).
 
 VariableUsedAs(var, "uint"):-
   VariableUsedAs(defVar, "uint"),
@@ -524,7 +525,16 @@ StorageVariable_IntermType(storVar, type):-
   Type_Kind(type, typeKind),
   Type_Width(type, 32).
 
+// IsUint(storVar, alias),
+// StorageVariable_IntermType(storVar, type):-
+//   VariableUsedAs(alias, "uint"),
+//   StorageVariableToAlias(storVar, alias),
+//   ProcessedStorageVariable(storVar, storVar),
+//   Type_Kind(type, "uint"),
+//   Type_Width(type, 32).
+
 VariableUsedAs(alias, typeKind):-
   StorageVariable_IntermType(storVar, type),
+  ProcessedStorageVariable(storVar, storVar),
   StorageVariableToAlias(storVar, alias),
   Type_Kind(type, typeKind).
\ No newline at end of file

From 2a6eb30f5ab818b49e8c059ddab74259e0a78688 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 03:09:03 +0200
Subject: [PATCH 35/53] Detect reverting type casts

---
 clientlib/casts_shifts.dl                    | 42 +++++++++++++++++++-
 clientlib/storage_modeling/type_inference.dl |  9 +++--
 2 files changed, 47 insertions(+), 4 deletions(-)

diff --git a/clientlib/casts_shifts.dl b/clientlib/casts_shifts.dl
index 5b7d376a..91c75b60 100644
--- a/clientlib/casts_shifts.dl
+++ b/clientlib/casts_shifts.dl
@@ -399,4 +399,44 @@ RevertEnforcesEnum(checkedVar, smallNum, checkBlock):-
 RevertEnforcesEnum(checkedVarAlias, smallNum, checkBlock):-
   RevertEnforcesEnum(checkedVar, smallNum, checkBlock),
   PHIStmtTwoUses(_, var1, var2, checkedVar),
-  PHIStmtTwoUses(_, var1, var2, checkedVarAlias).
\ No newline at end of file
+  PHIStmtTwoUses(_, var1, var2, checkedVarAlias).
+
+.decl RevertCastsToUint(checkedVar: Variable, jumpiBlock: Block)
+DEBUG_OUTPUT(RevertCastsToUint)
+RevertCastsToUint(checkedVar, checkBlock):-
+  SLT(_, checkedVar, zeroVar, negCont),
+  BasicVariable_Value(zeroVar, "0x0"),
+  ISZERO(_, negCont, cond),
+  JUMPI(jumpi, _, cond),
+  Statement_Block(jumpi, checkBlock),
+  FallthroughEdge(checkBlock, revertBlock),
+  ThrowBlock(revertBlock).
+
+.decl IntMaxConst(const: Value, width: number)
+IntMaxConst(as(@exp_256("0x2", @number_to_hex(typeWidth - 1)), Value), typeWidth):-
+  typeWidth = range(8, 264, 8).
+
+.decl IntMaxConstMinusOne(const: Value, width: number)
+IntMaxConstMinusOne(as(@sub_256(@exp_256("0x2", @number_to_hex(typeWidth - 1)), "0x1"), Value), typeWidth):-
+  typeWidth = range(8, 264, 8).
+
+.decl RevertCastsToInt(checkedVar: Variable, width: number, jumpiBlock: Block)
+DEBUG_OUTPUT(RevertCastsToInt)
+RevertCastsToInt(checkedVar, width, checkBlock):-
+  GT(_, checkedVar, zeroVar, negCont),
+  BasicVariable_Value(zeroVar, const),
+  IntMaxConstMinusOne(const, width),
+  ISZERO(_, negCont, cond),
+  JUMPI(jumpi, _, cond),
+  Statement_Block(jumpi, checkBlock),
+  FallthroughEdge(checkBlock, revertBlock),
+  ThrowBlock(revertBlock).
+
+.decl RevertEnforcesTypeCast(checkedVar: Variable, fromTypeKind: symbol, toTypeKind: symbol, width: number, jumpiBlock: Block)
+DEBUG_OUTPUT(RevertEnforcesTypeCast)
+
+RevertEnforcesTypeCast(checkedVar, "uint", "int", width, checkBlock):-
+  RevertCastsToInt(checkedVar, width, checkBlock).
+
+RevertEnforcesTypeCast(checkedVar, "int", "uint", 256, checkBlock):-
+  RevertCastsToUint(checkedVar, checkBlock).
\ No newline at end of file
diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 005cde8e..96c9b16f 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -500,17 +500,20 @@ VariableUsedAs(formalArg, typeKind):-
   VariableUsedAs(actualArg, typeKind),
   ActualArgs(caller, actualArg, pos),
   CallGraphEdge(caller, fun),
-  FormalArgs(fun, formalArg, pos).
+  FormalArgs(fun, formalArg, pos),
+  !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
 
 VariableUsedAs(actualRet, typeKind):-
   VariableUsedAs(formalRet, typeKind),
   FormalReturnArgs(fun, formalRet, retPos),
   CallGraphEdge(caller, fun),
-  ActualReturnArgs(caller, actualRet, retPos).
+  ActualReturnArgs(caller, actualRet, retPos),
+  !RevertEnforcesTypeCast(actualRet, typeKind, _, _, _).
 
 VariableUsedAs(to, typeKind):-
   VariableUsedAs(from, typeKind),
-  GlobalStructFlowsBase(from, to).
+  GlobalStructFlowsBase(from, to),
+  !RevertEnforcesTypeCast(to, typeKind, _, _, _).
 
 VariableUsedAs(from, typeKind):-
   VariableUsedAs(to, typeKind),

From a6249b57abfbba5fdafd7b258f03fd2700d720ae Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 03:51:15 +0200
Subject: [PATCH 36/53] add phis

---
 clientlib/storage_modeling/type_inference.dl | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 96c9b16f..ddaa4437 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -422,6 +422,13 @@ ComparisonOperation(stmt, var1, var2):-
   Statement_Uses(stmt, var1, i),
   Statement_Uses(stmt, var2, 1 - i).
 
+
+.decl PHIFlowBase(from: Variable, to: Variable)
+PHIFlowBase(from, to):-
+  PHITrans(from, to),
+  nUses = count: PHITrans(_, to),
+  nUses < 4.
+
 .decl VariableUsedAs(var: Variable, typeKind: symbol)
 DEBUG_OUTPUT(VariableUsedAs)
 
@@ -519,7 +526,10 @@ VariableUsedAs(from, typeKind):-
   VariableUsedAs(to, typeKind),
   GlobalStructFlowsBase(from, to).
 
-
+VariableUsedAs(to, typeKind):-
+  VariableUsedAs(from, typeKind),
+  PHIFlowBase(from, to),
+  !RevertEnforcesTypeCast(to, typeKind, _, _, _).
 
 StorageVariable_IntermType(storVar, type):-
   VariableUsedAs(alias, typeKind),

From 0374b95cd07e6133c88237f6641d9fdf3bab2343 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 04:44:15 +0200
Subject: [PATCH 37/53] Treat uint, bytes, int differently

---
 clientlib/storage_modeling/type_inference.dl | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index ddaa4437..6ae7d73e 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -546,8 +546,14 @@ StorageVariable_IntermType(storVar, type):-
 //   Type_Kind(type, "uint"),
 //   Type_Width(type, 32).
 
-VariableUsedAs(alias, typeKind):-
+VariableUsedAs(alias, "uint"):-
   StorageVariable_IntermType(storVar, type),
   ProcessedStorageVariable(storVar, storVar),
   StorageVariableToAlias(storVar, alias),
-  Type_Kind(type, typeKind).
\ No newline at end of file
+  Type_Kind(type, "uint").
+
+VariableUsedAs(alias, "bytes"):-
+  StorageVariable_IntermType(storVar, type),
+  ProcessedStorageVariable(storVar, storVar),
+  StorageVariableToAlias(storVar, alias),
+  Type_Kind(type, "bytes").
\ No newline at end of file

From f001fe2fa6197ad38e35d6547542ce9a0e49122e Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 20:24:25 +0200
Subject: [PATCH 38/53] cleanup

---
 clientlib/storage_modeling/type_inference.dl | 75 --------------------
 1 file changed, 75 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 6ae7d73e..c186c163 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -141,92 +141,17 @@ StorageVariable_IntermType(storVar, "int256"):-
   StorageVariableToAlias(storVar, aliasVar),
   SignedIntVar(aliasVar).
 
-// IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageVariableToAlias(storVar, aliasVar),
-//   Statement_Uses(stmt, aliasVar, i),
-//   Statement_Uses(stmt, uintVar, 1 - i),
-//   UintVar(uintVar),
-//   Statement_Opcode(stmt, op),
-//   (op = "LT"; op= "GT"; op = "EQ").
-
-// // IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageVariableToAlias(storVar, aliasVar),
-//   Statement_Uses(stmt, aliasVar, i),
-//   Statement_Uses(stmt, otherAliasVar, 1 - i),
-//   StorageVariableToAlias(storVar2, otherAliasVar),
-//   StorageVariable_IntermType(storVar2, "uint256"),
-//   Statement_Opcode(stmt, op),
-//   (op = "LT"; op= "GT"; op = "EQ").
-
-
-// IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageVariableToAlias(storVar, uintVar),
-//   UintVar(uintVar),
-//   !Variable_Value(uintVar, _).
-
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,
   widthBytes = 20.
 
-// IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-//   UintVar(uintVar),
-//   !Variable_Value(uintVar, _).
 
-// // IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
-//   SSTORE(store, _, var),
-//   uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-//   VarHoldsBytesOfStorVarPlus(uintVar, _, storVar2, 0, 0, 31),
-//   StorageVariable_IntermType(storVar2, "uint256").
-//   .plan 0:(6,5,4,3,2,1)
-
-// // IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   StorageVariable_IntermType(storVar2, "uint256"),
-//   StorageStmtToIndexAndConstruct(store, _, _, storVar2),
-//   SSTORE(store, _, uintVar),
-//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-//   VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-//   ProcessedStorageVariable(storVar, storVar).
-
-
-// IsUint(storVar, uintVar),
 StorageVariable_IntermType(storVar, "uint256"):-
   ProcessedStorageVariable(storVar, storVar),
   ConstWrittenToBytesOfStorVar(_, constVal, _, _, storVar, 0, 31),
   strlen(constVal) < 60. //is right aligned
 
-// IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
-//   SSTORE(store, _, var),
-//   uint256AliasFlowAnalysis.GlobalFlows(uintVar, var),
-//   UintVar(uintVar),
-//   !Variable_Value(uintVar, _).
-
-// IsUint(storVar, uintVar),
-// StorageVariable_IntermType(storVar, "uint256"):-
-//   ProcessedStorageVariable(storVar, storVar),
-//   StorageStmtToIndexAndConstruct(store, _, _, storVar),
-//   SSTORE(store, _, var),
-//   uint256AliasFlowAnalysis.GlobalFlows(var, uintVar),
-//   UintVar(uintVar),
-//   !Variable_Value(uintVar, _).
-
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "bool"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)).
 

From 9c995c60a3ac2118a3a76685540efce96aaa5f94 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 20:27:08 +0200
Subject: [PATCH 39/53] better support for intx

---
 clientlib/storage_modeling/type_inference.dl | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index c186c163..1165f99b 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -391,6 +391,10 @@ VariableUsedAsBase(var, "uint"):-
   val != "0x0", val != "0x1",
   strlen(val) < 30. // right aligned val
 
+VariableUsedAsBase(var, "int"):-
+  SignedIntVar(var);
+  SignedIntCast(_, var, _).
+
 VariableUsedAsBase(var, "bytes"):-
   ComparisonOperation(_, var, otherVar),
   Variable_Value(otherVar, val),

From 03c19f602081701d4365b26c796600b869da1c7a Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 12 Nov 2024 21:34:39 +0200
Subject: [PATCH 40/53] Add another cast to uint

---
 clientlib/casts_shifts.dl | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/clientlib/casts_shifts.dl b/clientlib/casts_shifts.dl
index 91c75b60..6c6f91f7 100644
--- a/clientlib/casts_shifts.dl
+++ b/clientlib/casts_shifts.dl
@@ -412,6 +412,19 @@ RevertCastsToUint(checkedVar, checkBlock):-
   FallthroughEdge(checkBlock, revertBlock),
   ThrowBlock(revertBlock).
 
+RevertCastsToUint(def, checkBlock):-
+  (EQ(_, checkedVar, maxConst, negCont); EQ(_, maxConst, checkedVar, negCont)),
+  BasicVariable_Value(maxConst, const),
+  IntMaxConst(const, 256),
+  ISZERO(_, negCont, cond),
+  JUMPI(jumpi, _, cond),
+  Statement_Block(jumpi, checkBlock),
+  FallthroughEdge(checkBlock, revertBlock),
+  ThrowBlock(revertBlock),
+  SUB(_, zeroVar, checkedVar, posVar),
+  BasicVariable_Value(zeroVar, "0x0"),
+  PHIStmtTwoUses(_, checkedVar, posVar, def).
+
 .decl IntMaxConst(const: Value, width: number)
 IntMaxConst(as(@exp_256("0x2", @number_to_hex(typeWidth - 1)), Value), typeWidth):-
   typeWidth = range(8, 264, 8).

From e90358d9c5505b9974f4c696b3947b031d660b7b Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 13 Nov 2024 01:25:24 +0200
Subject: [PATCH 41/53] remove redundant rule

---
 clientlib/storage_modeling/type_inference.dl | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 1165f99b..be2b3d6b 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -136,11 +136,6 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type
   widthBytes = 1 + byteHigh - byteLow,
   type = cat("int", to_string(widthBytes * 8)).
 
-StorageVariable_IntermType(storVar, "int256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  StorageVariableToAlias(storVar, aliasVar),
-  SignedIntVar(aliasVar).
-
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "address"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,

From 144d1bcb4901013770cf1baefe7106d133d6a0f0 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 13 Nov 2024 02:05:38 +0200
Subject: [PATCH 42/53] Introduce basic polymorphic functions

---
 clientlib/storage_modeling/type_inference.dl | 42 ++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index be2b3d6b..894df0db 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -253,6 +253,38 @@ ActualBinArithStmt(stmt):-
   !ISZERO(_, to, _),
   !JUMPI(_, _, to).
 
+.decl SharedIntMathOperation(stmt: Statement, use1: Variable, use2: Variable, def: Variable)
+SharedIntMathOperation(stmt, use1, use2, to):-
+  (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),
+  Statement_Uses(stmt, use1, 0),
+  Statement_Uses(stmt, use2, 1),
+  Statement_Defines(stmt, to, 0),
+  !LShiftBytes(_, to, _).
+
+SharedIntMathOperation(stmt, use1, use2, to):-
+  SUB(stmt, use1, use2, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+SharedIntMathOperation(stmt, use1, use2, to):-
+  ADD(stmt, use1, use2, to),
+  !ISZERO(_, to, _),
+  !JUMPI(_, _, to).
+
+
+.init polymorphicFlows = LocalFlowAnalysis
+
+polymorphicFlows.TransferStmt(stmt):- SharedIntMathOperation(stmt, _, _, _).
+polymorphicFlows.TransferBoundary(block) :- IsBlock(block).
+
+.decl PolymorphicMethod(fun: Function, argIndex: number, retIndex: number)
+DEBUG_OUTPUT(PolymorphicMethod)
+
+PolymorphicMethod(fun, argIndex, retIndex):-
+  FormalArgs(fun, arg, argIndex),
+  polymorphicFlows.Flows(arg, ret),
+  FormalReturnArgs(fun, ret, retIndex).
+
 .decl SignedIntVar(intVar: Variable)
 
 SignedIntVar(intVar):-
@@ -432,6 +464,16 @@ VariableUsedAs(formalArg, typeKind):-
   ActualArgs(caller, actualArg, pos),
   CallGraphEdge(caller, fun),
   FormalArgs(fun, formalArg, pos),
+  !PolymorphicMethod(fun, pos, _),
+  !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
+
+VariableUsedAs(actualRet, typeKind):-
+  VariableUsedAs(actualArg, typeKind),
+  ActualArgs(caller, actualArg, pos),
+  CallGraphEdge(caller, fun),
+  PolymorphicMethod(fun, pos, retIndex),
+  ActualReturnArgs(caller, actualRet, retIndex),
+  FormalArgs(fun, formalArg, pos),
   !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
 
 VariableUsedAs(actualRet, typeKind):-

From e6b2857550e4129acedf6a54ce9d7ccb56679e33 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 13 Nov 2024 03:35:31 +0200
Subject: [PATCH 43/53] improve precision

---
 clientlib/storage_modeling/type_inference.dl | 27 +++++++++++++-------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 894df0db..7660c622 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -82,16 +82,17 @@ DEBUG_OUTPUT(StorageVariableToAlias)
 StorageVariableToAlias(storVar, alias):-
   ProcessedStorageVariable(storVar, storVar),
   VarHoldsBytesOfStorVarPlus(var, _, storVar, 0, 0, 31),
-  uint256AliasFlowAnalysis.GlobalFlows(var, alias).
+  var = alias.
+  // uint256AliasFlowAnalysis.GlobalFlows(var, alias).
 
 StorageVariableToAlias(storVar, alias):-
   ProcessedStorageVariable(storVar, storVar),
   StorageStmtToIndexAndConstruct(store, _, _, storVar),
-  SSTORE(store, _, var),
-  (
-    uint256AliasFlowAnalysis.GlobalFlows(alias, var);
-    uint256AliasFlowAnalysis.GlobalFlows(var, alias)
-  ).
+  SSTORE(store, _, var), var=alias.
+  // (
+  //   uint256AliasFlowAnalysis.GlobalFlows(alias, var);
+  //   uint256AliasFlowAnalysis.GlobalFlows(var, alias)
+  // ).
 
 StorageVariable_IntermType(storVar, "uint256"):-
   ProcessedStorageVariable(storVar, storVar),
@@ -286,7 +287,7 @@ PolymorphicMethod(fun, argIndex, retIndex):-
   FormalReturnArgs(fun, ret, retIndex).
 
 .decl SignedIntVar(intVar: Variable)
-
+DEBUG_OUTPUT(SignedIntVar)
 SignedIntVar(intVar):-
   Statement_Opcode(stmt, op),
   (op = "SMOD" ; op = "SDIV"; op = "SGT"; op = "SLT"),
@@ -419,8 +420,9 @@ VariableUsedAsBase(var, "uint"):-
   strlen(val) < 30. // right aligned val
 
 VariableUsedAsBase(var, "int"):-
-  SignedIntVar(var);
-  SignedIntCast(_, var, _).
+  (SignedIntVar(var);
+  SignedIntCast(_, var, _)),
+  !RevertEnforcesTypeCast(var, "int", _, _, _).
 
 VariableUsedAsBase(var, "bytes"):-
   ComparisonOperation(_, var, otherVar),
@@ -483,6 +485,13 @@ VariableUsedAs(actualRet, typeKind):-
   ActualReturnArgs(caller, actualRet, retPos),
   !RevertEnforcesTypeCast(actualRet, typeKind, _, _, _).
 
+VariableUsedAs(formalArg, toTypeKind):-
+  VariableUsedAs(actualArg, typeKind),
+  ActualArgs(caller, actualArg, pos),
+  CallGraphEdge(caller, fun),
+  FormalArgs(fun, formalArg, pos),
+  RevertEnforcesTypeCast(formalArg, typeKind, toTypeKind, _, _).
+
 VariableUsedAs(to, typeKind):-
   VariableUsedAs(from, typeKind),
   GlobalStructFlowsBase(from, to),

From a7f4c028c28116274d279848c8da0d7659bb569f Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 13 Nov 2024 04:04:23 +0200
Subject: [PATCH 44/53] Add any type for 32 byte vals

---
 clientlib/storage_modeling/type_inference.dl | 37 +++++++++++++++-----
 1 file changed, 28 insertions(+), 9 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 7660c622..e171e8a9 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -6,6 +6,10 @@
 .decl Type_Width(type: Type, width: number)
 DEBUG_OUTPUT(Type_Width)
 
+// Top type for 32 bytes, to compare against VarLifter
+Type_Kind("bytes32/(u)int256", "any").
+Type_Width("bytes32/(u)int256", 32).
+
 Type_Kind("bool", "bool").
 Type_Width("bool", 1).
 Type_Kind("address", "uint").
@@ -76,6 +80,11 @@ StorageVariable_IntermType(storVar, bytesType) <= StorageVariable_IntermType(sto
   Type_Kind(bytesType, "bytes"),
   Type_Kind(uintType, "uint").
 
+StorageVariable_IntermType(storVar, anyType) <= StorageVariable_IntermType(storVar, type):-
+  Type_Kind(anyType, "any"),
+  Type_Kind(type, typeKind),
+  (typeKind = "bytes"; typeKind = "uint"; typeKind = "int").
+
 .decl StorageVariableToAlias(storVar: StorageConstruct, alias: Variable)
 DEBUG_OUTPUT(StorageVariableToAlias)
 
@@ -94,11 +103,24 @@ StorageVariableToAlias(storVar, alias):-
   //   uint256AliasFlowAnalysis.GlobalFlows(var, alias)
   // ).
 
-StorageVariable_IntermType(storVar, "uint256"):-
-  ProcessedStorageVariable(storVar, storVar),
-  instances = count : StorageVariableToAlias(storVar, _),
-  instances < 4.
 
+// OLD handling of 32 byte vals
+
+// StorageVariable_IntermType(storVar, "uint256"):-
+//   ProcessedStorageVariable(storVar, storVar),
+//   instances = count : StorageVariableToAlias(storVar, _),
+//   instances < 4.
+
+// StorageVariable_IntermType(var, "bytes32"):-
+//   IsStorageConstruct(var),
+//   var = $Variable(cons), cons = cons,
+//   ProcessedStorageVariable(var, var).
+
+// VarLifter compatible handling of 32 byte vals
+StorageVariable_IntermType(var, "bytes32/(u)int256"):-
+  IsStorageConstruct(var),
+  var = $Variable(cons), cons = cons,
+  ProcessedStorageVariable(var, var).
 
 StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), alias):-
   ProcessedStorageVariable(storVar, $TightlyPackedVariable(cons, byteLow, byteHigh)),
@@ -111,11 +133,6 @@ StorageVariableToAlias($TightlyPackedVariable(cons, byteLow, byteHigh), alias):-
   (uint256AliasFlowAnalysis.GlobalFlows(var, alias);
   uint256AliasFlowAnalysis.GlobalFlows(alias, var)).
 
-StorageVariable_IntermType(var, "bytes32"):-
-  IsStorageConstruct(var),
-  var = $Variable(cons), cons = cons,
-  ProcessedStorageVariable(var, var).
-
 StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
   widthBytes = 1 + byteHigh - byteLow,
@@ -433,6 +450,8 @@ VariableUsedAs(var, "bytes") <= VariableUsedAs(var, "uint"):- 1=1.
 
 VariableUsedAs(var, "uint") <= VariableUsedAs(var, "int"):- 1=1.
 
+VariableUsedAs(var, "any") <= VariableUsedAs(var, typeKind):- typeKind = "bytes"; typeKind = "uint"; typeKind = "int".
+
 VariableUsedAs(var, typeKind):-
   VariableUsedAsBase(var, typeKind).
 

From 52e769962f1859299e6bcff976d146e4fb70ed7d Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 13 Nov 2024 04:29:39 +0200
Subject: [PATCH 45/53] Improve type constraint propagation

---
 clientlib/storage_modeling/type_inference.dl | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index e171e8a9..8f8d78a9 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -497,6 +497,16 @@ VariableUsedAs(actualRet, typeKind):-
   FormalArgs(fun, formalArg, pos),
   !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
 
+// Backwards from actualRet to actualArg
+VariableUsedAs(actualArg, typeKind):-
+  VariableUsedAs(actualRet, typeKind),
+  ActualReturnArgs(caller, actualRet, retIndex),
+  CallGraphEdge(caller, fun),
+  ActualArgs(caller, actualArg, pos),
+  PolymorphicMethod(fun, pos, retIndex),
+  FormalArgs(fun, formalArg, pos),
+  !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
+
 VariableUsedAs(actualRet, typeKind):-
   VariableUsedAs(formalRet, typeKind),
   FormalReturnArgs(fun, formalRet, retPos),
@@ -511,6 +521,16 @@ VariableUsedAs(formalArg, toTypeKind):-
   FormalArgs(fun, formalArg, pos),
   RevertEnforcesTypeCast(formalArg, typeKind, toTypeKind, _, _).
 
+// Flow from formalArg to actualArg
+// TODO: Disabled
+VariableUsedAs(actualArg, typeKind):-
+  VariableUsedAs(formalArg, typeKind),1=0,
+  FormalArgs(fun, formalArg, pos),
+  CallGraphEdge(caller, fun),
+  ActualArgs(caller, actualArg, pos),
+  !PolymorphicMethod(fun, pos, _),
+  !RevertEnforcesTypeCast(formalArg, typeKind, _, _, _).
+
 VariableUsedAs(to, typeKind):-
   VariableUsedAs(from, typeKind),
   GlobalStructFlowsBase(from, to),

From 4c9c43f8f2895b9f1e54ddc15b9594d0c87e84a2 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 14 Nov 2024 03:07:32 +0200
Subject: [PATCH 46/53] Fix bug with bytes32, refactor any32

---
 clientlib/storage_modeling/type_inference.dl | 26 ++++++++++++++++----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 8f8d78a9..62c6d3cf 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -7,8 +7,8 @@
 DEBUG_OUTPUT(Type_Width)
 
 // Top type for 32 bytes, to compare against VarLifter
-Type_Kind("bytes32/(u)int256", "any").
-Type_Width("bytes32/(u)int256", 32).
+Type_Kind("any32", "any").
+Type_Width("any32", 32).
 
 Type_Kind("bool", "bool").
 Type_Width("bool", 1).
@@ -40,7 +40,7 @@ Type_Width(type, byteWidth):-
 // This relation is needed to ensure that the propagation of allsou
 .decl StorageVariable_IntermTypeDone(numOfFacts: number)
 
-
+DEBUG_OUTPUT(StorageVariable_IntermType)
 
 StorageVariable_IntermTypeDone(numOfFacts):-
   numOfFacts = count : StorageVariable_IntermType(_, _).
@@ -52,6 +52,14 @@ StorageVariable_Type($TightlyPackedVariable(cons, byteLow, byteHigh), type):-
 StorageVariable_Type($Variable(cons), type):-
   StorageVariable_IntermTypeDone(_),
   StorageVariable_IntermType($Variable(cons), type),
+  Type_Kind(type, typeKind),
+  typeKind != "any",
+  !IsPackedArray(cons, _).
+
+StorageVariable_Type($Variable(cons), "uint256"):-
+  StorageVariable_IntermTypeDone(_),
+  StorageVariable_IntermType($Variable(cons), type),
+  Type_Kind(type, "any"),
   !IsPackedArray(cons, _).
 
 // Hack for PackedArrays, to fix at a later point!
@@ -117,7 +125,7 @@ StorageVariableToAlias(storVar, alias):-
 //   ProcessedStorageVariable(var, var).
 
 // VarLifter compatible handling of 32 byte vals
-StorageVariable_IntermType(var, "bytes32/(u)int256"):-
+StorageVariable_IntermType(var, "any32"):-
   IsStorageConstruct(var),
   var = $Variable(cons), cons = cons,
   ProcessedStorageVariable(var, var).
@@ -392,6 +400,14 @@ ComparisonOperation(stmt, var1, var2):-
   Statement_Uses(stmt, var1, i),
   Statement_Uses(stmt, var2, 1 - i).
 
+ComparisonOperation(stmt, var1, var2):-
+  (SUB(stmt, var1, var2, def); SUB(stmt, var2, var1, def)),
+  JUMPI(_, _, def).
+
+ComparisonOperation(stmt, var1, var2):-
+  (SUB(stmt, var1, var2, def); SUB(stmt, var2, var1, def)),
+  ISZERO(_, def, cond),
+  JUMPI(_, _, cond).
 
 .decl PHIFlowBase(from: Variable, to: Variable)
 PHIFlowBase(from, to):-
@@ -426,7 +442,7 @@ VariableUsedAsBase(lenVar, "uint"):-
   ArrayAllocation(_, _, lenVar).
 
 VariableUsedAsBase(var, "bytes"):-
-  SHA3(_, _, _, var),
+  SHA3(_, _, _, var);
   BLOCKHASH(_, _, var);
   EXTCODEHASH(_, _, var).
 

From f13bab8a4814c53a1710663480408af8f9166edc Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 14 Nov 2024 03:35:28 +0200
Subject: [PATCH 47/53] make uint8 inference more complete

---
 clientlib/storage_modeling/type_inference.dl | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 62c6d3cf..4983f1f5 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -184,6 +184,13 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Uint8Var(uintVar),
   !Variable_Value(uintVar, _).
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
+  (VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte);
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), singleByte, singleByte)),
+  VariableUsedAs(var, "uint"),
+  !Variable_Value(var, _).
+
 .decl IsUint(storVar: StorageConstruct, uintVar: Variable)
 .output IsUint
 
@@ -279,6 +286,7 @@ ActualBinArithStmt(stmt):-
   !ISZERO(_, to, _),
   !JUMPI(_, _, to).
 
+// math operations used by both uintX and intX types
 .decl SharedIntMathOperation(stmt: Statement, use1: Variable, use2: Variable, def: Variable)
 SharedIntMathOperation(stmt, use1, use2, to):-
   (Statement_Opcode(stmt, "MUL"); Statement_Opcode(stmt, "SHL")),

From 9a8480fd2209777bee029254782261a1005b2cd8 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 14 Nov 2024 04:58:25 +0200
Subject: [PATCH 48/53] fix imprecision of reused constants

---
 clientlib/storage_modeling/type_inference.dl | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index 4983f1f5..e5ab6f15 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -184,6 +184,7 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte),
   Uint8Var(uintVar),
   !Variable_Value(uintVar, _).
 
+// IsUint($TightlyPackedVariable(cons, singleByte, singleByte), var):-
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   (VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, singleByte, singleByte);
@@ -477,7 +478,8 @@ VariableUsedAs(var, "uint") <= VariableUsedAs(var, "int"):- 1=1.
 VariableUsedAs(var, "any") <= VariableUsedAs(var, typeKind):- typeKind = "bytes"; typeKind = "uint"; typeKind = "int".
 
 VariableUsedAs(var, typeKind):-
-  VariableUsedAsBase(var, typeKind).
+  VariableUsedAsBase(var, typeKind),
+  !Variable_Value(var, _).
 
 VariableUsedAs(var, typeKind):-
   VariableUsedAs(otherVar, typeKind),

From 49d1e94b04949104786eaa6aad298628ed40e8f1 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 14 Nov 2024 14:34:49 +0200
Subject: [PATCH 49/53] Try to increase completeness of uint160

---
 clientlib/storage_modeling/type_inference.dl | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index e5ab6f15..b0f2da41 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -203,6 +203,14 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uin
   uint160flowAnalysis.GlobalFlows(var, uintVar),
   UintVar(uintVar).
 
+StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
+  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+  (VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh);
+  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh)),
+  20 = 1 + byteHigh - byteLow,
+  VariableUsedAs(var, "uint"),
+  !Variable_Value(var, _).
+
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),
   ConstWrittenToBytesOfStorVarProcessed(_, constVal, _, _, $Variable(cons), singleByte, singleByte),

From 70fe3306b303c40ae38d49409dd5f86dcdcfd8e4 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 14 Nov 2024 15:13:57 +0200
Subject: [PATCH 50/53] remove new rule

---
 clientlib/storage_modeling/type_inference.dl | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index b0f2da41..d97c79b5 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -203,13 +203,15 @@ StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uin
   uint160flowAnalysis.GlobalFlows(var, uintVar),
   UintVar(uintVar).
 
-StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
-  ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
-  (VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh);
-  VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh)),
-  20 = 1 + byteHigh - byteLow,
-  VariableUsedAs(var, "uint"),
-  !Variable_Value(var, _).
+// Removed due to imprecision caused by comparisons/uses of mock address consts
+// IsUint($TightlyPackedVariable(cons, byteLow, byteHigh), var):-
+// StorageVariable_IntermType($TightlyPackedVariable(cons, byteLow, byteHigh), "uint160"):-
+//   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, byteLow, byteHigh)),
+//   (VarHoldsBytesOfStorVarPlus(var, _, $Variable(cons), 0, byteLow, byteHigh);
+//   VarWrittenToBytesOfStorVarFinal(var, _, $Variable(cons), byteLow, byteHigh)),
+//   20 = 1 + byteHigh - byteLow,
+//   VariableUsedAs(var, "uint"),
+//   !Variable_Value(var, _).
 
 StorageVariable_IntermType($TightlyPackedVariable(cons, singleByte, singleByte), "uint8"):-
   ProcessedStorageVariable(_, $TightlyPackedVariable(cons, singleByte, singleByte)),

From bfb12ad24a0396a5e67d9933dbc1eb14501862d5 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 15 Nov 2024 14:55:05 +0200
Subject: [PATCH 51/53] rename

---
 clientlib/storage_modeling/data_structures.dl | 38 +++++++++----------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index f5fcd5aa..9d02c4b2 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -9,7 +9,7 @@
   used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
 */
 .type StorageIndex = ConstantIndex {value: Value}
-                    | ConstArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
+                    | StaticArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
                     | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
                     | ArrayDataStartIndex {parIndex: StorageIndex}
                     | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
@@ -19,7 +19,7 @@
   `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
 */
 .type StorageConstruct = Constant {value: Value}
-                        | ConstArray {parConstruct: StorageConstruct, arraySize: number}
+                        | StaticArray {parConstruct: StorageConstruct, arraySize: number}
                         | Array {parConstruct: StorageConstruct}
                         | Mapping {parConstruct: StorageConstruct}
                         | Offset {parConstruct: StorageConstruct, offset: number}
@@ -187,12 +187,12 @@ Variable_StorageIndex(def, $ArrayAccessIndex(parentIndex, newIndexVar)):-
   ADDFix(_, indexVar, minusOneConstVar2, newIndexVar),
   Variable_Value(minusOneConstVar2, "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff").
 
-Variable_StorageIndex(def, $ConstArrayAccessIndex(parentIndex, arraySize, checkedVar)):-
+Variable_StorageIndex(def, $StaticArrayAccessIndex(parentIndex, arraySize, checkedVar)):-
   Variable_StorageIndex(var, parentIndex),
   ADDFix(_, var, checkedVar, def),
   RevertEnforcesEnum(checkedVar, arraySize, _).
 
-Variable_StorageIndex(def, $ConstArrayAccessIndex(parentIndex, arraySize, checkedVarDiv)):-
+Variable_StorageIndex(def, $StaticArrayAccessIndex(parentIndex, arraySize, checkedVarDiv)):-
   Variable_StorageIndex(var, parentIndex),
   ADDFix(_, var, checkedVarDiv, def),
   DIV(_, checkedVar, const, checkedVarDiv),
@@ -218,8 +218,8 @@ StorageIndex_StorageConstruct($OffsetIndex(parentIndex, offset), $Offset(parentC
   ActualStorageIndex($OffsetIndex(parentIndex, offset)), offset != 0,
   StorageIndex_StorageConstruct(parentIndex, parentCons).
 
-StorageIndex_StorageConstruct($ConstArrayAccessIndex(parentIndex, arraySize, indexVar), $ConstArray(parentCons, arraySize)):-
-  ActualStorageIndex($ConstArrayAccessIndex(parentIndex, arraySize, indexVar)),
+StorageIndex_StorageConstruct($StaticArrayAccessIndex(parentIndex, arraySize, indexVar), $StaticArray(parentCons, arraySize)):-
+  ActualStorageIndex($StaticArrayAccessIndex(parentIndex, arraySize, indexVar)),
   StorageIndex_StorageConstruct(parentIndex, parentCons).
 
 /**
@@ -244,7 +244,7 @@ StorageIndex_ParentIndex(index, parentIndex):-
   (
     (index = $ArrayAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $ArrayDataStartIndex(parentIndex));
-    (index = $ConstArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
+    (index = $StaticArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
     (index = $MappingAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $OffsetIndex(parentIndex, offset), offset = offset) // suppress warning
   ).
@@ -254,7 +254,7 @@ StorageIndex_ParentIndexExclOffset(index, parentIndex):-
   (
     (index = $ArrayAccessIndex(parentIndex, indexVar), indexVar = indexVar); // suppress warning
     (index = $ArrayDataStartIndex(parentIndex));
-    (index = $ConstArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
+    (index = $StaticArrayAccessIndex(parentIndex, arraySize, indexVar), indexVar = indexVar, arraySize = arraySize); // suppress warning
     (index = $MappingAccessIndex(parentIndex, indexVar), indexVar = indexVar) // suppress warning
     // commenting this out for now, helps some cases but is not right
     // ;(index = $OffsetIndex(parentIndex, offset), offset > 0) // suppress warning
@@ -289,13 +289,13 @@ ActualStorageIndex(parentIndex):-
 
 StorageIndex_HighLevelUses(index, accessVar, 0, 0, 1):-
   ActualStorageIndex(index),
-  (index = $ArrayAccessIndex($ConstantIndex(const), accessVar); (index = $ConstArrayAccessIndex($ConstantIndex(const), arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex($ConstantIndex(const), accessVar)),
+  (index = $ArrayAccessIndex($ConstantIndex(const), accessVar); (index = $StaticArrayAccessIndex($ConstantIndex(const), arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex($ConstantIndex(const), accessVar)),
   const = const.
 
 StorageIndex_HighLevelUses(index, otherVar, prevOffset, i, prevNestedness + 1),
 StorageIndex_HighLevelUses(index, accessVar, 0, prevNestedness, prevNestedness + 1):-
   ActualStorageIndex(index),
-  (index = $ArrayAccessIndex(parIndex, accessVar); (index = $ConstArrayAccessIndex(parIndex, arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex(parIndex, accessVar)),
+  (index = $ArrayAccessIndex(parIndex, accessVar); (index = $StaticArrayAccessIndex(parIndex, arraySize, accessVar), arraySize=arraySize); index = $MappingAccessIndex(parIndex, accessVar)),
   StorageIndex_HighLevelUses(parIndex, otherVar, prevOffset, i, prevNestedness).
 
 StorageIndex_HighLevelUses($OffsetIndex(parentIndex, offset), accessVar, prevOffset, i, prevNestedness):-
@@ -331,19 +331,19 @@ IsStorageConstruct(cons),
 IsDataStructureConstruct(cons):-
   ActualStorageIndex(index),
   StorageIndex_StorageConstruct(index, cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize)), // filter intermediate constructs
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $StaticArray(parentCons, arraySize), arraySize=arraySize)), // filter intermediate constructs
   parentCons = parentCons. // suppress warning
 
 StorageConstruct_ParentAndOffset(cons, paparentCons, offset):-
   IsStorageConstruct(cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $StaticArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
   parentCons = $Offset(paparentCons, offset),
   offset = offset. // suppress warning
 
 StorageConstruct_ParentAndOffset(cons, parentCons, 0):-
   IsStorageConstruct(cons),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
-  (parentCons = $Array(paparentCons) ; parentCons = $Mapping(paparentCons); (parentCons = $ConstArray(paparentCons, arraySize2), arraySize2=arraySize2); parentCons = $Variable(paparentCons)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $StaticArray(parentCons, arraySize), arraySize=arraySize); cons = $Variable(parentCons)),
+  (parentCons = $Array(paparentCons) ; parentCons = $Mapping(paparentCons); (parentCons = $StaticArray(paparentCons, arraySize2), arraySize2=arraySize2); parentCons = $Variable(paparentCons)),
   paparentCons = paparentCons. // suppress warning
 
 DataStructure_ElemNum(cons, elemNum):-
@@ -448,8 +448,8 @@ DataStructure_Type($Array(parentCons), "string"):-
   IsDataStructureConstruct($Array(parentCons)),
   BytesOrStringLengthV2($Array(parentCons), _).
 
-DataStructure_Type($ConstArray(parentCons, arraySize), cat(type, cat("[", cat(to_string(arraySize), "]")))):-
-  DataStructure_ValueOrElementType($ConstArray(parentCons, arraySize), type).
+DataStructure_Type($StaticArray(parentCons, arraySize), cat(type, cat("[", cat(to_string(arraySize), "]")))):-
+  DataStructure_ValueOrElementType($StaticArray(parentCons, arraySize), type).
 
 // // Disable general rule for now
 // StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $Variable(cons)):-
@@ -520,7 +520,7 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
 
 StorageOffset_Type(offset, type):-
   DataStructure_Type(cons, type),
-  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $ConstArray(parentCons, arraySize), arraySize=arraySize)),
+  (cons = $Array(parentCons); cons = $Mapping(parentCons); (cons = $StaticArray(parentCons, arraySize), arraySize=arraySize)),
   parentCons = $Constant(offset).
 
 
@@ -673,7 +673,7 @@ DEBUG_OUTPUT(IsPackedArray)
 IsPackedArray(cons, byteWidth):-
   SLOAD(_, sindexVar, loadedVar),
   Variable_StorageIndex(sindexVar, sindex),
-  ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
+  ((sindex = $StaticArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
   sindex = $ArrayAccessIndex(parIndex, indexVar)),
   parIndex=parIndex,
   StorageIndex_StorageConstruct(sindex, cons),
@@ -690,7 +690,7 @@ IsPackedArray(cons, byteWidth):-
 IsPackedArray(cons, @hex_to_number(@div_256("0x20", const))):-
   SLOAD(_, sindexVar, loadedVar),
   Variable_StorageIndex(sindexVar, sindex),
-  ((sindex = $ConstArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
+  ((sindex = $StaticArrayAccessIndex(parIndex, arraySize, indexVar), arraySize=arraySize);
   sindex = $ArrayAccessIndex(parIndex, indexVar)),
   parIndex=parIndex,
   StorageIndex_StorageConstruct(sindex, cons),

From ba16a3609d28c6849677a8276ca5211523a3ec74 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 15 Nov 2024 15:48:03 +0200
Subject: [PATCH 52/53] fix tests

---
 tests/storage/Storage.sol         | 3 +++
 tests/storage/array-merged.json   | 2 +-
 tests/storage/array1-iropt.json   | 2 +-
 tests/storage/array1.json         | 2 +-
 tests/storage/map1.json           | 2 +-
 tests/storage/mapping-merged.json | 2 +-
 6 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/tests/storage/Storage.sol b/tests/storage/Storage.sol
index 043cd62e..5f57cac2 100644
--- a/tests/storage/Storage.sol
+++ b/tests/storage/Storage.sol
@@ -87,6 +87,9 @@ contract SimpleArray {
         return false;
     }
 
+    function setOwners(address[] memory _owners) external {
+        owners = _owners;
+    }
 }
 
 contract SimpleMapping {
diff --git a/tests/storage/array-merged.json b/tests/storage/array-merged.json
index 387b35f2..c9f0118f 100644
--- a/tests/storage/array-merged.json
+++ b/tests/storage/array-merged.json
@@ -3,5 +3,5 @@
     "gigahorse_args": ["-i", "--disable_inline", "--disable_scalable_fallback"],
     "expected_analytics": [ ["Analytics_NonModeledSSTORE", 0, 0], ["Analytics_NonModeledSLOAD", 0, 0]],
     "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tstruct_[0-9]*\\[\\]\n"],
-                            ["Verbatim_StructToString", "struct_[0-9]*\tstruct struct_[0-9]* { uint160 field0_0_19; uint8 field0_20_20; uint8 field0_21_21; }\n"]]
+                            ["Verbatim_StructToString", "struct_[0-9]*\tstruct struct_[0-9]* { address field0_0_19; bool field0_20_20; bool field0_21_21; }\n"]]
 }
\ No newline at end of file
diff --git a/tests/storage/array1-iropt.json b/tests/storage/array1-iropt.json
index 7b4ff0a4..6d5314b8 100644
--- a/tests/storage/array1-iropt.json
+++ b/tests/storage/array1-iropt.json
@@ -2,5 +2,5 @@
     "client_path": "clients/analytics_client.dl",
     "gigahorse_args": ["-i", "--disable_scalable_fallback"],
     "expected_analytics": [["Analytics_NonModeledSSTORE", 0, 0], ["Analytics_NonModeledSLOAD", 0, 0], ["Analytics_ArrayDeleteOp", 1, 0]],
-    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tuint160[]\n"]]
+    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\taddress[]\n"]]
 }
\ No newline at end of file
diff --git a/tests/storage/array1.json b/tests/storage/array1.json
index d29beb24..7354bde2 100644
--- a/tests/storage/array1.json
+++ b/tests/storage/array1.json
@@ -3,5 +3,5 @@
     "gigahorse_args": ["-i", "--disable_scalable_fallback"],
     "expected_analytics": [["Analytics_StorageArray", 1, 0], ["Analytics_NonModeledSSTORE", 0, 0],
                             ["Analytics_NonModeledSLOAD", 0, 0], ["Analytics_ArrayDeleteOp", 1, 0]],
-    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tuint160[]\n"]]
+    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\taddress[]\n"]]
 }
\ No newline at end of file
diff --git a/tests/storage/map1.json b/tests/storage/map1.json
index f81f146e..970b8cd5 100644
--- a/tests/storage/map1.json
+++ b/tests/storage/map1.json
@@ -2,5 +2,5 @@
     "client_path": "clients/analytics_client.dl",
     "gigahorse_args": ["-i", "--disable_inline", "--disable_scalable_fallback"],
     "expected_analytics": [["Analytics_Map", 1, 0], ["Analytics_NonModeledSSTORE", 0, 0], ["Analytics_NonModeledSLOAD", 0, 0]],
-    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tmapping (uint256 => uint8)\n"]]
+    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tmapping (uint256 => bool)\n"]]
 }
\ No newline at end of file
diff --git a/tests/storage/mapping-merged.json b/tests/storage/mapping-merged.json
index 44e48824..ca86e902 100644
--- a/tests/storage/mapping-merged.json
+++ b/tests/storage/mapping-merged.json
@@ -3,5 +3,5 @@
     "gigahorse_args": ["-i", "--disable_inline", "--disable_scalable_fallback"],
     "expected_analytics": [ ["Analytics_NonModeledSSTORE", 0, 0], ["Analytics_NonModeledSLOAD", 0, 0]],
     "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tmapping \\(uint256 => struct_[0-9]*\\)\n"],
-                            ["Verbatim_StructToString", "struct_[0-9]*\tstruct struct_[0-9]* { uint160 field0_0_19; uint8 field0_20_20; uint8 field0_21_21; uint256 field1; }\n"]]
+                            ["Verbatim_StructToString", "struct_[0-9]*\tstruct struct_[0-9]* { address field0_0_19; bool field0_20_20; bool field0_21_21; uint256 field1; }\n"]]
 }
\ No newline at end of file

From 6dac54caf9766b3fe559d8ab18633ff142c0a059 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 15 Nov 2024 15:56:09 +0200
Subject: [PATCH 53/53] fix forgotten test

---
 tests/storage/array1-opt.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/storage/array1-opt.json b/tests/storage/array1-opt.json
index 7b4ff0a4..6d5314b8 100644
--- a/tests/storage/array1-opt.json
+++ b/tests/storage/array1-opt.json
@@ -2,5 +2,5 @@
     "client_path": "clients/analytics_client.dl",
     "gigahorse_args": ["-i", "--disable_scalable_fallback"],
     "expected_analytics": [["Analytics_NonModeledSSTORE", 0, 0], ["Analytics_NonModeledSLOAD", 0, 0], ["Analytics_ArrayDeleteOp", 1, 0]],
-    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\tuint160[]\n"]]
+    "expected_verbatim": [["Verbatim_StorageOffset_Type", "0x0\taddress[]\n"]]
 }
\ No newline at end of file