From 3fdbf24b77937c43ec4ee4995b7be17306d37b34 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Wed, 6 Dec 2023 18:03:02 +0200 Subject: [PATCH 01/28] Initial version of analysis with unsound pre-global analysis --- logic/global.dl | 51 ++++++++++++++++++++++++++++++++----- logic/local.dl | 2 +- logic/statement_insertor.dl | 7 +---- 3 files changed, 46 insertions(+), 14 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index 0e9eabab..878e29a3 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -40,7 +40,15 @@ .type Statement <: symbol .type FunctionSignature <: symbol -.init global = OptimizedGlobalAnalysis +.init incompleteGlobal = IncompleteOptimizedGlobalAnalysis + +COPY_CODE(incompleteGlobal, postTrans) + +.init global = ExperimentalCompleteOptimizedGlobalAnalysis + +global.StatementPushesUsedLabel(stmt):- + incompleteGlobal.VariableAlwaysUsedAsJumpTarget(pushedVar), + postTrans.Statement_Defines(stmt, pushedVar). COPY_CODE(global, postTrans) @@ -83,12 +91,8 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- // Stack contents at end of a `block`, given its calling `context`. .decl BlockOutputContents(context: sens.Context, block: Block, index: StackIndex, var: Variable) - #ifdef ENABLE_LIMITSIZE - .limitsize BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) - #endif - DEBUG_OUTPUT(BlockOutputContents) - + /** Stack contents at start of a `block`, given its calling `context`. Added overridable flag to override it in the optimized variant of the component @@ -261,9 +265,42 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .plan 1:(2,1) } + +/** + Used whenever a best effort is good enough +*/ +.comp IncompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { + .limitsize BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) +} + +/** + Used for the main global analysis. Only has a limitsize if the `--enable_limitsize` flag is set. +*/ +.comp CompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { + #ifdef ENABLE_LIMITSIZE + .limitsize BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) + #endif +} + +.comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { + + .decl StatementPushesUsedLabel(stmt: Statement) + + .override BlockPushesLabel + BlockPushesLabel(block, val) :- + JUMPDEST(as(val, symbol)), + Variable_Value(var, val), + Statement_Defines(stmt, var), + StatementPushesUsedLabel(stmt), + Statement_Block(stmt, block), + BasicBlock_Tail(block, call), + LocalStackContents(call, _, var), + !BlockUsesLocal(block, var). +} + /** Declared just so it can be used as a parameter in another component */ -.comp DefaultOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { +.comp DefaultIncompleteOptimizedGlobalAnalysis : IncompleteOptimizedGlobalAnalysis { } \ No newline at end of file diff --git a/logic/local.dl b/logic/local.dl index 8d7fc560..11a7abe5 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -555,7 +555,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- caller != caller2. // pushes a label for later use. A return addr? - .decl BlockPushesLabel(block: Block, val: Value) + .decl BlockPushesLabel(block: Block, val: Value) overridable BlockPushesLabel(block, val) :- JUMPDEST(as(val, symbol)), Variable_Value(var, val), diff --git a/logic/statement_insertor.dl b/logic/statement_insertor.dl index 6ee87b3b..f602f9b0 100644 --- a/logic/statement_insertor.dl +++ b/logic/statement_insertor.dl @@ -449,12 +449,7 @@ INITIALIZE_STATEMENT_INSERTOR(_insertor, to) BlockCloner using an underlying global analysis to ensure that the program's semantics will not break. To be used in most cases. */ -.comp SafeBlockCloner : AbstractBlockCloner { - - // We want this enabled all the time. This ifndef is just to avoid double limitsize definition - #ifndef ENABLE_LIMITSIZE - .limitsize analysis.BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) - #endif +.comp SafeBlockCloner : AbstractBlockCloner { BlockPushedToStack(pushStmt, pushedVar, as(pushedBlock, Block)):- analysis.Variable_Value(pushedVar, pushedBlock), From d761c652b4575c8144bb6d046a4777a45a7132d4 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 7 Dec 2023 00:16:04 +0200 Subject: [PATCH 02/28] should be working n --- logic/global.dl | 10 +++++----- logic/local.dl | 7 +++++-- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index 878e29a3..da6dede8 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -7,8 +7,8 @@ #define MAX_NUM_PRIVATE_FUNCTION_ARGS 50 #define MAX_NUM_PRIVATE_FUNCTION_RETS 50 - -#define LIMITSIZE_BLOCK_OUTPUT_CONTENTS 5000000 +// #define ENABLE_LIMITSIZE +#define LIMITSIZE_BLOCK_OUTPUT_CONTENTS 1000000 #define CheckIsVariable(v) ((v) < 0) #define CheckIsStackIndex(v) ((v) >= 0, (v) < MAX_STACK_HEIGHT) @@ -285,9 +285,9 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { .decl StatementPushesUsedLabel(stmt: Statement) - - .override BlockPushesLabel - BlockPushesLabel(block, val) :- + .output sens.local.BlockPushesLabel, StatementPushesUsedLabel, sens.local.PrivateFunctionCall + + sens.local.ExtBlockPushesLabel(block, val) :- JUMPDEST(as(val, symbol)), Variable_Value(var, val), Statement_Defines(stmt, var), diff --git a/logic/local.dl b/logic/local.dl index 11a7abe5..e83123d8 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -554,8 +554,10 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- StaticBlockJumpTarget(caller2, target), caller != caller2. + .decl ExtBlockPushesLabel(block: Block, val: Value) + // pushes a label for later use. A return addr? - .decl BlockPushesLabel(block: Block, val: Value) overridable + .decl BlockPushesLabel(block: Block, val: Value) BlockPushesLabel(block, val) :- JUMPDEST(as(val, symbol)), Variable_Value(var, val), @@ -563,7 +565,8 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- Statement_Block(stmt, block), BasicBlock_Tail(block, call), LocalStackContents(call, _, var), - !BlockUsesLocal(block, var). + !BlockUsesLocal(block, var), + !ExtBlockPushesLabel(_, _). // Same reasoning, with more detail. In very rare cases, the continuation will not be found, // even though BlockPushesLabel is true. From e912e6d3a3e07e0dd63e7a2a72a39e8a0a3a816e Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 7 Dec 2023 01:01:57 +0200 Subject: [PATCH 03/28] Added missing rule --- logic/local.dl | 3 +++ 1 file changed, 3 insertions(+) diff --git a/logic/local.dl b/logic/local.dl index e83123d8..938eb537 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -568,6 +568,9 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- !BlockUsesLocal(block, var), !ExtBlockPushesLabel(_, _). + BlockPushesLabel(block, val):- + ExtBlockPushesLabel(block, val). + // Same reasoning, with more detail. In very rare cases, the continuation will not be found, // even though BlockPushesLabel is true. .decl CallBlockPushesContinuation(caller: Block, callee: Block, cont: Block, index: number) From 49c45d8e44150b3724c5e34122c294844ac92c01 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 7 Dec 2023 18:55:40 +0200 Subject: [PATCH 04/28] Tweak StatementPushesUsedLabel, favoring completeness --- logic/global.dl | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index da6dede8..f9b42b86 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -47,7 +47,7 @@ COPY_CODE(incompleteGlobal, postTrans) .init global = ExperimentalCompleteOptimizedGlobalAnalysis global.StatementPushesUsedLabel(stmt):- - incompleteGlobal.VariableAlwaysUsedAsJumpTarget(pushedVar), + incompleteGlobal.VariableUsedInAsJumpdest(pushedVar), postTrans.Statement_Defines(stmt, pushedVar). COPY_CODE(global, postTrans) @@ -232,6 +232,14 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- op != "JUMP", op != "JUMPI". + .decl VariableUsedInAsJumpdest(var: Variable) + + VariableUsedInAsJumpdest(var):- + Statement_Uses(stmt, var, 0), + Statement_Opcode(stmt, op), + (op = "JUMP"; op = "JUMPI"). + + VariableUsedInOperation(var):- Statement_Uses(stmt, var, 1), Statement_Opcode(stmt, "JUMPI"). @@ -285,8 +293,8 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { .decl StatementPushesUsedLabel(stmt: Statement) - .output sens.local.BlockPushesLabel, StatementPushesUsedLabel, sens.local.PrivateFunctionCall - + // .output sens.local.BlockPushesLabel, StatementPushesUsedLabel, sens.local.PrivateFunctionCall + // .output BlockPushesLabel sens.local.ExtBlockPushesLabel(block, val) :- JUMPDEST(as(val, symbol)), Variable_Value(var, val), From 55474238541ce1eac92ff8810d12a19d9e985d6a Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Fri, 8 Dec 2023 17:50:08 +0200 Subject: [PATCH 05/28] Refactor global and local analysis components. Makes uses of the local component more clear. --- logic/global.dl | 28 ++++++++++++---------- logic/local.dl | 46 +++++++++++++++++++------------------ logic/statement_insertor.dl | 6 +++++ 3 files changed, 46 insertions(+), 34 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index f9b42b86..ed358777 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -40,9 +40,9 @@ .type Statement <: symbol .type FunctionSignature <: symbol -.init incompleteGlobal = IncompleteOptimizedGlobalAnalysis +.init incompleteGlobal = IncompleteOptimizedGlobalAnalysis -COPY_CODE(incompleteGlobal, postTrans) +COPY_CODE_FULL(incompleteGlobal, postTrans) .init global = ExperimentalCompleteOptimizedGlobalAnalysis @@ -50,7 +50,7 @@ global.StatementPushesUsedLabel(stmt):- incompleteGlobal.VariableUsedInAsJumpdest(pushedVar), postTrans.Statement_Defines(stmt, pushedVar). -COPY_CODE(global, postTrans) +COPY_CODE_FULL(global, postTrans) // Masks with all 1s .decl Mask_Length(mask: Value, bytes: number) @@ -73,18 +73,20 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- bytes < 32. -.comp GlobalAnalysis : PreTransLocalAnalysis { +.comp GlobalAnalysis : LocalAnalysis { /* *********** * Key dataflow definitions *********** */ - .init sens = AbstractContextSensitivity + .init sens = AbstractContextSensitivity sens.local.PushValue(push, val):- PushValue(push, val). sens.local.Statement_Opcode(stmt, op):- Statement_Opcode(stmt, op). sens.local.Statement_Next(stmt, stmtNext):- Statement_Next(stmt, stmtNext). + sens.local.PublicFunction(block, hex):- PublicFunction(block, hex). + sens.local.PublicFunctionJump(block, hex):- PublicFunctionJump(block, hex). // `block` is reachable under `context` .decl ReachableContext(context: sens.Context, block: Block) @@ -254,7 +256,7 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- /** A global analysis component optimized by only modeling the stack locations containing jump targets */ -.comp OptimizedGlobalAnalysis : GlobalAnalysis { +.comp OptimizedGlobalAnalysis : GlobalAnalysis { .override BlockInputContents @@ -277,25 +279,26 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- /** Used whenever a best effort is good enough */ -.comp IncompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { +.comp IncompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { .limitsize BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) } /** Used for the main global analysis. Only has a limitsize if the `--enable_limitsize` flag is set. */ -.comp CompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { +.comp CompleteOptimizedGlobalAnalysis : OptimizedGlobalAnalysis { #ifdef ENABLE_LIMITSIZE .limitsize BlockOutputContents(n=LIMITSIZE_BLOCK_OUTPUT_CONTENTS) #endif } -.comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { +.comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { .decl StatementPushesUsedLabel(stmt: Statement) // .output sens.local.BlockPushesLabel, StatementPushesUsedLabel, sens.local.PrivateFunctionCall // .output BlockPushesLabel - sens.local.ExtBlockPushesLabel(block, val) :- + ExtBlockPushesLabel(block, val), + sens.local.ExtBlockPushesLabel(block, val):- JUMPDEST(as(val, symbol)), Variable_Value(var, val), Statement_Defines(stmt, var), @@ -307,8 +310,9 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- } /** - Declared just so it can be used as a parameter in another component + Declared just so it can be used as a parameter in another component. + Used by the SafeBlockCloner so it uses `PreTransLocalAnalysis` */ -.comp DefaultIncompleteOptimizedGlobalAnalysis : IncompleteOptimizedGlobalAnalysis { +.comp DefaultIncompleteOptimizedGlobalAnalysis : IncompleteOptimizedGlobalAnalysis { } \ No newline at end of file diff --git a/logic/local.dl b/logic/local.dl index 938eb537..048f8fb3 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -554,10 +554,8 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- StaticBlockJumpTarget(caller2, target), caller != caller2. - .decl ExtBlockPushesLabel(block: Block, val: Value) - // pushes a label for later use. A return addr? - .decl BlockPushesLabel(block: Block, val: Value) + .decl BlockPushesLabel(block: Block, val: Value) overridable BlockPushesLabel(block, val) :- JUMPDEST(as(val, symbol)), Variable_Value(var, val), @@ -565,11 +563,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- Statement_Block(stmt, block), BasicBlock_Tail(block, call), LocalStackContents(call, _, var), - !BlockUsesLocal(block, var), - !ExtBlockPushesLabel(_, _). - - BlockPushesLabel(block, val):- - ExtBlockPushesLabel(block, val). + !BlockUsesLocal(block, var). // Same reasoning, with more detail. In very rare cases, the continuation will not be found, // even though BlockPushesLabel is true. @@ -625,6 +619,20 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- .output MultiplePrivateFunctionCall .output PrivateFunctionCall // .output CallBlockEarliestContinuation + + .decl CODECOPYStatement(stmt: Statement, offset: Value, size: Value) + + CODECOPYStatement(codeCopy, codeOffsetNumHex, smallNumHex) :- + Statement_Opcode(codeCopy, "CODECOPY"), + BeforeLocalStackContents(codeCopy, 2, lenVar), + CheckIsVariable(lenVar), + Statement_Defines(pushLen, lenVar), + PushValue(pushLen, smallNumHex), + BeforeLocalStackContents(codeCopy, 1, codeOffsetVar), + CheckIsVariable(codeOffsetVar), + Statement_Defines(pushCodeOffset, codeOffsetVar), + PushValue(pushCodeOffset, codeOffsetNumHex). + } .comp PreTransLocalAnalysis : LocalAnalysis { @@ -656,20 +664,6 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- ByteCodeHex(bytecodeStr), const = cat("0x", substr(bytecodeStr, 2*codeOffsetNum, 2*smallNum)). - .decl CODECOPYStatement(stmt: Statement, offset: Value, size: Value) - - CODECOPYStatement(codeCopy, codeOffsetNumHex, smallNumHex) :- - Statement_Opcode(codeCopy, "CODECOPY"), - BeforeLocalStackContents(codeCopy, 2, lenVar), - CheckIsVariable(lenVar), - Statement_Defines(pushLen, lenVar), - PushValue(pushLen, smallNumHex), - BeforeLocalStackContents(codeCopy, 1, codeOffsetVar), - CheckIsVariable(codeOffsetVar), - Statement_Defines(pushCodeOffset, codeOffsetVar), - PushValue(pushCodeOffset, codeOffsetNumHex). - - .decl BlockComparesSigVyper(block: Block, sigHash: Value) BlockComparesSigVyper(block, sigHash) :- @@ -762,6 +756,14 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- } +.comp PostIncompleteGlobalLocalAnalysis : LocalAnalysis { + .decl ExtBlockPushesLabel(block: Block, val: Value) + + .override BlockPushesLabel + + BlockPushesLabel(block, val):- + ExtBlockPushesLabel(block, val). +} /** Preprocessing of decompiler input, to yield convenient relations diff --git a/logic/statement_insertor.dl b/logic/statement_insertor.dl index f602f9b0..c5257406 100644 --- a/logic/statement_insertor.dl +++ b/logic/statement_insertor.dl @@ -21,6 +21,12 @@ to.PushValue(stmt, value) :- _insertor.Out_PushValue(stmt, value). COPY_CODE(_insertor, from)\ INITIALIZE_STATEMENT_INSERTOR(_insertor, to) +#define COPY_CODE_FULL(to, from)\ +COPY_CODE(to, from)\ +to.PublicFunctionJump(block, funHex):- from.PublicFunctionJump(block, funHex).\ +to.PublicFunction(block, funHex):- from.PublicFunction(block, funHex). + + #define ISLABEL(value) (substr(value, 0, 9) = "JUMPDEST:") #define MAKE_LABEL_REFERENCE(value) cat("JUMPDEST:", value) #define GET_LABEL_REFERENCE(value) substr(value, 9, 30) From ee694a2e2b6322e15730cfa7d8ee5e3f5d0c3fa8 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 9 Dec 2023 15:02:08 +0200 Subject: [PATCH 06/28] Refactor, filter out invalid PublicFunction inferences --- logic/context-sensitivity/abstract_context.dl | 8 +- logic/context-sensitivity/callsite_context.dl | 2 +- .../finite_precise_context.dl | 14 +-- .../finite_shrinking_context.dl | 18 +-- .../hybrid_precise_context.dl | 16 +-- .../context-sensitivity/selective_context.dl | 6 +- .../transactional_context.dl | 6 +- .../transactional_shrinking_context.dl | 10 +- logic/functions.dl | 8 +- logic/global.dl | 41 ++++++- logic/local.dl | 114 ++++++++++++------ logic/statement_insertor.dl | 4 +- 12 files changed, 160 insertions(+), 87 deletions(-) diff --git a/logic/context-sensitivity/abstract_context.dl b/logic/context-sensitivity/abstract_context.dl index 5b2dc138..b9abdfbc 100644 --- a/logic/context-sensitivity/abstract_context.dl +++ b/logic/context-sensitivity/abstract_context.dl @@ -50,13 +50,13 @@ .input InputMaxContextDepth(filename="MaxContextDepth.csv") MaxContextDepth(sigHash, d) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), InputMaxContextDepth(d). MaxContextDepth(sigHash, 10) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), !InputMaxContextDepth(_). } @@ -282,14 +282,14 @@ #ifndef NO_PUBLIC_CONTEXT MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. .plan 1:(3,1,2) MergeContext(ctx, caller, newContext):- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, pri), prevSigHash = FALLBACK_FUNCTION_SIGHASH, diff --git a/logic/context-sensitivity/callsite_context.dl b/logic/context-sensitivity/callsite_context.dl index 2e1b1f43..abe0c474 100644 --- a/logic/context-sensitivity/callsite_context.dl +++ b/logic/context-sensitivity/callsite_context.dl @@ -20,7 +20,7 @@ ReachableContext(ctx, caller), DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), newPrivateContext = [caller, cutDownPri]. .plan 1:(2,1,3), 2:(3,2,1) } \ No newline at end of file diff --git a/logic/context-sensitivity/finite_precise_context.dl b/logic/context-sensitivity/finite_precise_context.dl index 70064ebd..5aae2546 100644 --- a/logic/context-sensitivity/finite_precise_context.dl +++ b/logic/context-sensitivity/finite_precise_context.dl @@ -13,13 +13,13 @@ .input InputMaxContextDepth(filename="MaxContextDepth.csv") MaxContextDepth(sigHash, d) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), InputMaxContextDepth(d). // HERE: much deeper MaxContextDepth(sigHash, 27) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), !InputMaxContextDepth(_). @@ -135,14 +135,14 @@ #ifndef NO_PUBLIC_CONTEXT MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. .plan 1:(3,1,2) MergeContext(ctx, caller, newContext):- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, pri), prevSigHash = FALLBACK_FUNCTION_SIGHASH, @@ -163,14 +163,14 @@ MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). @@ -184,7 +184,7 @@ DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif newPrivateContext = [caller, cutDownPri]. .plan 1:(3,1,2,4), 2:(4,3,1,2) diff --git a/logic/context-sensitivity/finite_shrinking_context.dl b/logic/context-sensitivity/finite_shrinking_context.dl index 04b56bec..0367d60d 100644 --- a/logic/context-sensitivity/finite_shrinking_context.dl +++ b/logic/context-sensitivity/finite_shrinking_context.dl @@ -13,13 +13,13 @@ .input InputMaxContextDepth(filename="MaxContextDepth.csv") MaxContextDepth(sigHash, d) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), InputMaxContextDepth(d). // HERE: much deeper MaxContextDepth(sigHash, 10) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), !InputMaxContextDepth(_). @@ -97,14 +97,14 @@ #ifndef NO_PUBLIC_CONTEXT MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. .plan 1:(3,1,2) MergeContext(ctx, caller, newContext):- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, pri), prevSigHash = FALLBACK_FUNCTION_SIGHASH, @@ -123,12 +123,12 @@ // Split into two rules to add plan. MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). .plan 1:(2,3,1) @@ -147,7 +147,7 @@ ReachableContext(ctx, caller), local.PrivateFunctionCall(caller, _, _, _), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), newPrivateContext = [caller, cutDownAtEndPri]. .plan 1:(3,1,2) @@ -196,7 +196,7 @@ MergeContextRequest(ctx, block, cont), PrivateFunctionReturn(block), DecomposeContext(ctx, pub, priCtx), - !local.PublicFunction(block, _), + !local.PublicFunction(block, _, _), CutToCaller(priCtx, cont, cutPri). .plan 1:(3,1,2,4), 2:(4,3,1,2) @@ -207,7 +207,7 @@ DecomposeContext(ctx, pub, priCtx), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), NoCutToCaller(priCtx, cont), - !local.PublicFunction(block, _), + !local.PublicFunction(block, _, _), newPrivateContext = [block, cutDownAtEndPri]. .plan 1:(3,1,2,4,5), 2:(4,3,1,2,5), 3:(5,3,1,2,4) diff --git a/logic/context-sensitivity/hybrid_precise_context.dl b/logic/context-sensitivity/hybrid_precise_context.dl index 1196d79d..5b4a03a7 100644 --- a/logic/context-sensitivity/hybrid_precise_context.dl +++ b/logic/context-sensitivity/hybrid_precise_context.dl @@ -16,19 +16,19 @@ .input InputMaxImpreciseContextDepth(filename="MaxContextDepth.csv") MaxImpreciseContextDepth(sigHash, d) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), InputMaxImpreciseContextDepth(d). MaxImpreciseContextDepth(sigHash, 7) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH), !InputMaxImpreciseContextDepth(_). // Not yet configurable via input file .decl MaxPreciseContextDepth(sigHash: symbol, d: number) MaxPreciseContextDepth(sigHash, 27) :- - (local.PublicFunction(_, sigHash); + (local.PublicFunction(_, sigHash, _); sigHash = FALLBACK_FUNCTION_SIGHASH). // @@ -253,14 +253,14 @@ #ifndef NO_PUBLIC_CONTEXT MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxImpreciseContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. .plan 1:(3,1,2) MergeContext(ctx, caller, newContext) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxImpreciseContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, pri), prevSigHash = FALLBACK_FUNCTION_SIGHASH, @@ -280,14 +280,14 @@ MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif DecomposeContext(ctx, pub, _), MaxImpreciseContextDepth(pub, 0). @@ -301,7 +301,7 @@ DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif newPrivateContext = [caller, cutDownPri]. .plan 1:(3,1,2,4), 2:(4,3,1,2) diff --git a/logic/context-sensitivity/selective_context.dl b/logic/context-sensitivity/selective_context.dl index a5e2502b..425851fb 100644 --- a/logic/context-sensitivity/selective_context.dl +++ b/logic/context-sensitivity/selective_context.dl @@ -23,20 +23,20 @@ MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), local.BlockHasTrivialControl(caller), - !local.PublicFunction(caller, _). + !local.PublicFunction(caller, _, _). MergeContext(ctx, caller, [pub, newPrivateContext]):- ReachableContext(ctx, caller), DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), !local.BlockHasTrivialControl(caller), newPrivateContext = [caller, cutDownPri]. .plan 1:(2,1,3), 2:(3,2,1) MergeContext(ctx, caller, newContext) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash), + local.PublicFunction(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, _, callCtx), newContext = [sigHash, callCtx]. diff --git a/logic/context-sensitivity/transactional_context.dl b/logic/context-sensitivity/transactional_context.dl index e82a92f8..72a9bcdc 100644 --- a/logic/context-sensitivity/transactional_context.dl +++ b/logic/context-sensitivity/transactional_context.dl @@ -5,14 +5,14 @@ MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). @@ -26,7 +26,7 @@ DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), #endif newPrivateContext = [caller, cutDownPri]. .plan 1:(3,1,2,4), 2:(4,3,1,2) diff --git a/logic/context-sensitivity/transactional_shrinking_context.dl b/logic/context-sensitivity/transactional_shrinking_context.dl index 8c2bec0f..a5ba4521 100644 --- a/logic/context-sensitivity/transactional_shrinking_context.dl +++ b/logic/context-sensitivity/transactional_shrinking_context.dl @@ -5,12 +5,12 @@ // Split into two rules to add plan. MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). .plan 1:(2,3,1) @@ -29,7 +29,7 @@ ReachableContext(ctx, caller), local.PrivateFunctionCall(caller, _, _, _), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), - !local.PublicFunction(caller, _), + !local.PublicFunction(caller, _, _), newPrivateContext = [caller, cutDownAtEndPri]. .plan 1:(3,1,2) @@ -78,7 +78,7 @@ MergeContextRequest(ctx, block, cont), PrivateFunctionReturn(block), DecomposeContext(ctx, pub, priCtx), - !local.PublicFunction(block, _), + !local.PublicFunction(block, _, _), CutToCaller(priCtx, cont, cutPri). .plan 1:(3,1,2,4), 2:(4,3,1,2) @@ -89,7 +89,7 @@ DecomposeContext(ctx, pub, priCtx), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), NoCutToCaller(priCtx, cont), - !local.PublicFunction(block, _), + !local.PublicFunction(block, _, _), newPrivateContext = [block, cutDownAtEndPri]. .plan 1:(3,1,2,4,5), 2:(4,3,1,2,5), 3:(5,3,1,2,4) diff --git a/logic/functions.dl b/logic/functions.dl index 6b870f48..36a25b1c 100644 --- a/logic/functions.dl +++ b/logic/functions.dl @@ -262,8 +262,8 @@ IsFunctionCallReturn(ctx, caller, func, retCtx, retBlock, retTarget) :- .decl PublicFunctionFiltered(block: Block, sigHash: Value) PublicFunctionFiltered(func, sigHash):- - postTrans.PublicFunctionJump(prev, sigHash), - postTrans.PublicFunction(func, sigHash), + postTrans.PublicFunctionJump(prev, sigHash, _), + postTrans.PublicFunction(func, sigHash, _), global.BlockEdge(_, prev, _, func). // NOTE the philosophy! MaybeFunctionCallReturn intends to be @@ -284,7 +284,7 @@ IsFunctionEntry(func) :- IsFunctionCallReturn(_, _, func, _, _, _). IsFunctionCall(prev, func), IsPublicFunctionCall(prev, func) :- - postTrans.PublicFunctionJump(prev, sigHash), + postTrans.PublicFunctionJump(prev, sigHash, _), PublicFunctionFiltered(func, sigHash), global.BlockEdge(_, prev, _, func). @@ -1078,7 +1078,7 @@ SighashIntermediate(sigIn, cat("0x0",substr(sigOut,2,8))) :- strlen(sigOut) < 10. SighashIntermediate(sig, sig) :- - postTrans.PublicFunction(_, sig). + postTrans.PublicFunction(_, sig, _). .decl IRPublicFunction(irfunc: IRFunction, sigHash: Value) IRPublicFunction(irfunc, sigHash) :- diff --git a/logic/global.dl b/logic/global.dl index ed358777..fba8fff9 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -7,7 +7,7 @@ #define MAX_NUM_PRIVATE_FUNCTION_ARGS 50 #define MAX_NUM_PRIVATE_FUNCTION_RETS 50 -// #define ENABLE_LIMITSIZE +#define ENABLE_LIMITSIZE #define LIMITSIZE_BLOCK_OUTPUT_CONTENTS 1000000 #define CheckIsVariable(v) ((v) < 0) #define CheckIsStackIndex(v) ((v) >= 0, (v) < MAX_STACK_HEIGHT) @@ -40,6 +40,10 @@ .type Statement <: symbol .type FunctionSignature <: symbol +.type OptionalSelector = NoSelector{} + | SelectorVariable{selector: Variable} + | SelectorStackIndex{block: Block, selector: StackIndex} + .init incompleteGlobal = IncompleteOptimizedGlobalAnalysis COPY_CODE_FULL(incompleteGlobal, postTrans) @@ -50,7 +54,13 @@ global.StatementPushesUsedLabel(stmt):- incompleteGlobal.VariableUsedInAsJumpdest(pushedVar), postTrans.Statement_Defines(stmt, pushedVar). -COPY_CODE_FULL(global, postTrans) +COPY_CODE(global, postTrans) +global.PublicFunctionJump(block, hex, selector):- + incompleteGlobal.ValidPublicFunctionJump(block, hex, selector). + +global.PublicFunction(block, hex, selector):- + incompleteGlobal.ValidPublicFunctionJump(_, hex, selector), + incompleteGlobal.PublicFunction(block, hex, selector). // Masks with all 1s .decl Mask_Length(mask: Value, bytes: number) @@ -85,8 +95,8 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- sens.local.PushValue(push, val):- PushValue(push, val). sens.local.Statement_Opcode(stmt, op):- Statement_Opcode(stmt, op). sens.local.Statement_Next(stmt, stmtNext):- Statement_Next(stmt, stmtNext). - sens.local.PublicFunction(block, hex):- PublicFunction(block, hex). - sens.local.PublicFunctionJump(block, hex):- PublicFunctionJump(block, hex). + sens.local.PublicFunction(block, hex, selector):- PublicFunction(block, hex, selector). + sens.local.PublicFunctionJump(block, hex, selector):- PublicFunctionJump(block, hex, selector). // `block` is reachable under `context` .decl ReachableContext(context: sens.Context, block: Block) @@ -251,6 +261,23 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- VariableAlwaysUsedAsJumpTarget(var):- VariableContainsJumpTarget(var), !VariableUsedInOperation(var). + + .decl ValidPublicFunctionJump(jumpBlock: Block, hex: Value, selector: OptionalSelector) + .decl ValidPublicFunction(startBlock: Block, hex: Value, selector: OptionalSelector) + DEBUG_OUTPUT(ValidPublicFunctionJump) + + ValidPublicFunctionJump(jumpBlock, hex, $SelectorStackIndex(block, selectorStackIndex)):- + PublicFunctionJump(jumpBlock, hex, $SelectorStackIndex(block, selectorStackIndex)), + BlockInputContents(_, block, selectorStackIndex, selectorVariable), + FunctionSelectorVariable(selectorVariable). + + ValidPublicFunctionJump(jumpBlock, hex, $SelectorVariable(selectorVariable)):- + PublicFunctionJump(jumpBlock, hex, $SelectorVariable(selectorVariable)), + FunctionSelectorVariable(selectorVariable). + + ValidPublicFunctionJump(jumpBlock, hex, $NoSelector()):- + PublicFunctionJump(jumpBlock, hex, $NoSelector()). + } /** @@ -261,13 +288,13 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .override BlockInputContents /** - Cut down `BlockOutputContents`, only containing jump targets. + Cut down `BlockOutputContents`, only containing jump targets (and the function selector var). Stack contents at end of a `block`, given its calling `context`. */ .decl AuxBlockOutputContentsJumpTarget(context:sens.Context, block:Block, index:StackIndex, var:Variable) AuxBlockOutputContentsJumpTarget(context, block, index, var) :- BlockOutputContents(context, block, index, var), - VariableContainsJumpTarget(var). + (VariableContainsJumpTarget(var); FunctionSelectorVariable(var)). BlockInputContents(calleeCtx, callee, index, variable) :- AuxBlockOutputContentsJumpTarget(callerCtx, caller, index, variable), @@ -292,6 +319,8 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- #endif } +// copying of PublicFunction from postTrans causes issues. Need to filter imprecision of the local function inference. +// Perhaps post incomplete would be the best place to do that. .comp ExperimentalCompleteOptimizedGlobalAnalysis : CompleteOptimizedGlobalAnalysis { .decl StatementPushesUsedLabel(stmt: Statement) diff --git a/logic/local.dl b/logic/local.dl index 048f8fb3..a5000372 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -466,20 +466,23 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- Statement_Opcode(stmt, opcode), OpcodeGas(opcode, gas). - .decl PublicFunctionJump(block:Block, funHex: Value) - .decl PublicFunction(block:Block, funHex: Value) + .decl PublicFunctionJump(block:Block, funHex: Value, optionalSelector: OptionalSelector) + .decl PublicFunction(block:Block, funHex: Value, optionalSelector: OptionalSelector) // Code inserted by compiler to compare function signature - .decl BlockComparesSig(block: Block, sigHash: Value) + .decl BlockComparesSig(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) // Compares label from stack to a constant: common public function dispatch pattern - BlockComparesSig(block, sigHash) :- + BlockComparesSig(block, sigHash, selector) :- Statement_Block(pushStmt, block), ImmediateBlockJumpTarget(block, _), (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), Statement_Defines(pushStmt, sigHashVar), EQ(eqStmt), - Statement_Uses_Local(eqStmt, sigHashVar, _), + Statement_Uses_Local(eqStmt, sigHashVar, n), + Statement_Uses_Local(eqStmt, selectorVarOrIndex, 1 - n), + ((CheckIsStackIndex(selectorVarOrIndex), selector = $SelectorStackIndex(block, selectorVarOrIndex)); + (CheckIsVariable(selectorVarOrIndex), selector = $SelectorVariable(selectorVarOrIndex))), Statement_Defines(eqStmt, pred), JUMPI(jumpiStmt), Statement_Uses_Local(jumpiStmt, pred, 1). @@ -633,6 +636,24 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- Statement_Defines(pushCodeOffset, codeOffsetVar), PushValue(pushCodeOffset, codeOffsetNumHex). + .decl FunctionSelectorVariable(variable: Variable) + FunctionSelectorVariable(selector):- + CALLDATALOAD(stmt), + Statement_Uses_Local(stmt, zeroVar, 0), + Variable_Value(zeroVar, "0x0"), + Statement_Defines(stmt, selector). + + FunctionSelectorVariable(selector):- + CALLDATALOAD(stmt), + Statement_Uses_Local(stmt, zeroVar, 0), + Variable_Value(zeroVar, "0x0"), + Statement_Defines(stmt, variable), + Statement_Uses_Local(shift, variable, 1), + Statement_Uses_Local(shift, shiftConst, 0), + Variable_Value(shiftConst, "0xe0"), + SHR(shift), + Statement_Defines(shift, selector). + } .comp PreTransLocalAnalysis : LocalAnalysis { @@ -664,13 +685,16 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- ByteCodeHex(bytecodeStr), const = cat("0x", substr(bytecodeStr, 2*codeOffsetNum, 2*smallNum)). - .decl BlockComparesSigVyper(block: Block, sigHash: Value) + .decl BlockComparesSigVyper(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) + + .decl BlockComparesSigVyperBase(block: Block, sigHash: Value, selectorVarOrIndex: VariableOrStackIndex) - BlockComparesSigVyper(block, sigHash) :- + BlockComparesSigVyperBase(block, sigHash, selectorVarOrIndex) :- Statement_Block(pushStmt, block), (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), Statement_Defines(pushStmt, sigHashVar), - Statement_Uses_Local(eqStmt, sigHashVar, _), + Statement_Uses_Local(eqStmt, sigHashVar, n), + Statement_Uses_Local(eqStmt, selectorVarOrIndex, 1 - n), EQ(eqStmt), Statement_Defines(eqStmt, pred), Statement_Uses_Local(isZeroStmt, pred, 0), @@ -680,33 +704,45 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- JUMPI(jumpiStmt). // New vyper pattern - BlockComparesSigVyper(block, sigHash) :- + BlockComparesSigVyperBase(block, sigHash, selectorVarOrIndex):- Statement_Block(pushStmt, block), (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), Statement_Defines(pushStmt, sigHashVar), - Statement_Uses_Local(xorStmt, sigHashVar, _), + Statement_Uses_Local(xorStmt, sigHashVar, n), + Statement_Uses_Local(xorStmt, selectorVarOrIndex, 1 - n), XOR(xorStmt), Statement_Defines(xorStmt, pred), Statement_Uses_Local(jumpiStmt, pred, 1), JUMPI(jumpiStmt). + BlockComparesSigVyper(block, sigHash, $SelectorVariable(selectorVar)):- + BlockComparesSigVyperBase(block, sigHash, selectorVar), + CheckIsVariable(selectorVar). + + BlockComparesSigVyper(block, sigHash, $SelectorStackIndex(block, selectorIndex)):- + BlockComparesSigVyperBase(block, sigHash, selectorIndex), + CheckIsStackIndex(selectorIndex). + // pattern in via-ir contracts, public function start is the block's fallthrough - .decl BlockComparesSigFallthroughSolidity(block: Block, sigHash: Value) - BlockComparesSigFallthroughSolidity(block, sigHash) :- + .decl BlockComparesSigFallthroughSolidity(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) + BlockComparesSigFallthroughSolidity(block, sigHash, selector) :- Statement_Block(pushStmt, block), ImmediateBlockJumpTarget(block, _), (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), Statement_Defines(pushStmt, sigHashVar), SUB(subStmt), - Statement_Uses_Local(subStmt, sigHashVar, _), + Statement_Uses_Local(subStmt, sigHashVar, n), + Statement_Uses_Local(subStmt, selectorVarOrIndex, 1 - n), + ((CheckIsStackIndex(selectorVarOrIndex), selector = $SelectorStackIndex(block, selectorVarOrIndex)); + (CheckIsVariable(selectorVarOrIndex), selector = $SelectorVariable(selectorVarOrIndex))), Statement_Defines(subStmt, pred), JUMPI(jumpiStmt), Statement_Uses_Local(jumpiStmt, pred, 1). - PublicFunctionJump(block, sigHash) :- BlockComparesSig(block, sigHash). + PublicFunctionJump(block, sigHash, selectorVarOrIndex) :- BlockComparesSig(block, sigHash, selectorVarOrIndex). - PublicFunction(as(targetValue, Block), sigHash) :- - BlockComparesSig(block, sigHash), + PublicFunction(as(targetValue, Block), sigHash, selectorVarOrIndex) :- + BlockComparesSig(block, sigHash, selectorVarOrIndex), ImmediateBlockJumpTarget(block, var), Statement_Defines(push, var), PushValue(push, targetValue), @@ -739,8 +775,8 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- JUMPDEST(as(fallthrough, Statement)). // Fallback functions - PublicFunctionJump(block, FALLBACK_FUNCTION_SIGHASH), - PublicFunction(fallbackStart, FALLBACK_FUNCTION_SIGHASH):- + PublicFunctionJump(block, FALLBACK_FUNCTION_SIGHASH, $NoSelector()), + PublicFunction(fallbackStart, FALLBACK_FUNCTION_SIGHASH, $NoSelector()):- BlockComparesCallDataSizeToFour(block, _, fallbackStart), 1 = count : BlockComparesCallDataSizeToFour(_, _, _), !BlockJumpsOnCallDataSize(fallbackStart, _, _). @@ -842,8 +878,8 @@ insertor.insertOps(jumpDestStmt, STMT(JUMP, cat("PublicFunctionJump:", hash)) ) ) :- - preTrans.PublicFunctionJump(block, hash), - preTrans.PublicFunction(start, hash), + preTrans.PublicFunctionJump(block, hash, selector), + preTrans.PublicFunction(start, hash, selector), preTrans.Statement_Block(jumpDestStmt, start), preTrans.JUMPDEST(jumpDestStmt), preTrans.PushValue(pushStmt, as(jumpDestStmt, symbol)), @@ -860,10 +896,10 @@ insertor.insertOps(functionStartStmt, STMT(JUMPDEST, MAKE_LABEL_REFERENCE(hash)) ) ) :- - preTrans.BlockComparesSigVyper(block, hash), + preTrans.BlockComparesSigVyper(block, hash, _), preTrans.BasicBlock_Tail(block, tail), preTrans.Statement_Next(tail, functionStartStmt), - !preTrans.BlockComparesSig(_, _). + !preTrans.BlockComparesSig(_, _, _). // transformation for pattern in via-ir contracts insertor.insertOps(functionStartStmt, @@ -873,10 +909,10 @@ insertor.insertOps(functionStartStmt, STMT(JUMPDEST, MAKE_LABEL_REFERENCE(hash)) ) ) :- - preTrans.BlockComparesSigFallthroughSolidity(block, hash), + preTrans.BlockComparesSigFallthroughSolidity(block, hash, _), preTrans.BasicBlock_Tail(block, tail), preTrans.Statement_Next(tail, functionStartStmt), - !preTrans.BlockComparesSig(_, hash). + !preTrans.BlockComparesSig(_, hash, _). // Receive transformation insertor.insertOps(functionStartStmt, @@ -969,30 +1005,37 @@ insertor.insertOps(codeCopy, .init postTrans = PostTransLocalAnalysis // For Solidity, Vyper -postTrans.PublicFunctionJump(block, substr(meta, 19, 30)) :- +postTrans.PublicFunctionJump(block, hash, selector) :- insertor.MetaData(stmt, meta), STARTSWITH(meta, "PublicFunctionJump:"), - postTrans.Statement_Block(stmt, block). + postTrans.Statement_Block(stmt, block), + hash = substr(meta, 19, 30), + (preTrans.PublicFunctionJump(_, hash, selector); + preTrans.BlockComparesSigVyper(_, hash, selector); + preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); + (preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = "0x00000000", selector = $NoSelector()) + ). + // we may lose some precision here when two blocks have the same hex // For Vyper -postTrans.PublicFunction(block, hash) :- +postTrans.PublicFunction(block, hash, selector):- insertor.MetaData(stmt, meta), postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block), - preTrans.BlockComparesSigVyper(_, hash), - !preTrans.BlockComparesSig(_, _), + preTrans.BlockComparesSigVyper(_, hash, selector), + !preTrans.BlockComparesSig(_, _, _), ISLABEL(meta), hash = GET_LABEL_REFERENCE(meta). -postTrans.PublicFunction(block, hash) :- +postTrans.PublicFunction(block, hash, selector) :- insertor.MetaData(stmt, meta), postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block), - preTrans.BlockComparesSigFallthroughSolidity(_, hash), - !preTrans.BlockComparesSig(_, hash), + preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector), + !preTrans.BlockComparesSig(_, hash, _), ISLABEL(meta), hash = GET_LABEL_REFERENCE(meta). // For receive functions -postTrans.PublicFunction(block, hash) :- +postTrans.PublicFunction(block, hash, $NoSelector()) :- preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = "0x00000000", hash = GET_LABEL_REFERENCE(meta), ISLABEL(meta), @@ -1000,8 +1043,9 @@ postTrans.PublicFunction(block, hash) :- postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block). -postTrans.PublicFunction(b, h) :- preTrans.PublicFunction(b, h). - +postTrans.PublicFunction(b, h, s) :- preTrans.PublicFunction(b, h, s). +.output postTrans.PublicFunction, preTrans.PublicFunction, preTrans.BlockComparesSigFallthroughSolidity, preTrans.BlockComparesSigVyper, insertor.MetaData +.output postTrans.PublicFunctionJump // Code chunking logic reserved for future EIP #define CHUNK_SIZE 31 diff --git a/logic/statement_insertor.dl b/logic/statement_insertor.dl index c5257406..e5f910be 100644 --- a/logic/statement_insertor.dl +++ b/logic/statement_insertor.dl @@ -23,8 +23,8 @@ INITIALIZE_STATEMENT_INSERTOR(_insertor, to) #define COPY_CODE_FULL(to, from)\ COPY_CODE(to, from)\ -to.PublicFunctionJump(block, funHex):- from.PublicFunctionJump(block, funHex).\ -to.PublicFunction(block, funHex):- from.PublicFunction(block, funHex). +to.PublicFunctionJump(block, funHex, selector):- from.PublicFunctionJump(block, funHex, selector).\ +to.PublicFunction(block, funHex, selector):- from.PublicFunction(block, funHex, selector). #define ISLABEL(value) (substr(value, 0, 9) = "JUMPDEST:") From 67a69d2b8cfcb419e5ac5c75fcfb22c77b8a06c3 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 9 Dec 2023 15:29:40 +0200 Subject: [PATCH 07/28] Filter out incorrect public functions --- logic/functions.dl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/logic/functions.dl b/logic/functions.dl index 36a25b1c..9a54799b 100644 --- a/logic/functions.dl +++ b/logic/functions.dl @@ -262,8 +262,9 @@ IsFunctionCallReturn(ctx, caller, func, retCtx, retBlock, retTarget) :- .decl PublicFunctionFiltered(block: Block, sigHash: Value) PublicFunctionFiltered(func, sigHash):- - postTrans.PublicFunctionJump(prev, sigHash, _), + postTrans.PublicFunctionJump(prev, sigHash, selector), postTrans.PublicFunction(func, sigHash, _), + global.ValidPublicFunctionJump(prev, sigHash, selector), global.BlockEdge(_, prev, _, func). // NOTE the philosophy! MaybeFunctionCallReturn intends to be From 402ec17a5707ba71cd3569633dc056c6d0790015 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sat, 9 Dec 2023 19:03:29 +0200 Subject: [PATCH 08/28] Improve completeness of FunctionSelectorVariable --- logic/local.dl | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/logic/local.dl b/logic/local.dl index a5000372..002af766 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -654,6 +654,17 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- SHR(shift), Statement_Defines(shift, selector). + FunctionSelectorVariable(selector):- + CALLDATALOAD(stmt), + Statement_Uses_Local(stmt, zeroVar, 0), + Variable_Value(zeroVar, "0x0"), + Statement_Defines(stmt, variable), + Statement_Uses_Local(shift, variable, 0), + Statement_Uses_Local(shift, shiftConst, 1), + Variable_Value(shiftConst, "0x100000000000000000000000000000000000000000000000000000000"), + DIV(shift), + Statement_Defines(shift, selector). + } .comp PreTransLocalAnalysis : LocalAnalysis { From ee73d434f7e785b85231746349cedee9946abaff Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sun, 10 Dec 2023 02:08:25 +0200 Subject: [PATCH 09/28] oops --- logic/global.dl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/logic/global.dl b/logic/global.dl index fba8fff9..5cfb3885 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -7,7 +7,7 @@ #define MAX_NUM_PRIVATE_FUNCTION_ARGS 50 #define MAX_NUM_PRIVATE_FUNCTION_RETS 50 -#define ENABLE_LIMITSIZE + #define LIMITSIZE_BLOCK_OUTPUT_CONTENTS 1000000 #define CheckIsVariable(v) ((v) < 0) #define CheckIsStackIndex(v) ((v) >= 0, (v) < MAX_STACK_HEIGHT) From 8a81a641f3889d84df656c9ac35d730bac06b2a4 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sun, 10 Dec 2023 12:05:05 +0200 Subject: [PATCH 10/28] use ValidPublicFunction. remove warning --- logic/global.dl | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index 5cfb3885..28ab9c15 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -58,9 +58,8 @@ COPY_CODE(global, postTrans) global.PublicFunctionJump(block, hex, selector):- incompleteGlobal.ValidPublicFunctionJump(block, hex, selector). -global.PublicFunction(block, hex, selector):- - incompleteGlobal.ValidPublicFunctionJump(_, hex, selector), - incompleteGlobal.PublicFunction(block, hex, selector). +global.PublicFunction(start, hex, selector):- + incompleteGlobal.ValidPublicFunction(start, hex, selector). // Masks with all 1s .decl Mask_Length(mask: Value, bytes: number) @@ -278,6 +277,10 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- ValidPublicFunctionJump(jumpBlock, hex, $NoSelector()):- PublicFunctionJump(jumpBlock, hex, $NoSelector()). + ValidPublicFunction(startBlock, hex, selector):- + ValidPublicFunctionJump(_, hex, selector), + PublicFunction(startBlock, hex, selector). + } /** From 688e3631a9b7b853a1e4a6000c9311de9e2ed43e Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Sun, 10 Dec 2023 15:10:34 +0200 Subject: [PATCH 11/28] differentiate receive and fallback selector --- logic/local.dl | 58 ++++++++++++++++++++++++++++++-------------------- logic/main.dl | 2 +- 2 files changed, 36 insertions(+), 24 deletions(-) diff --git a/logic/local.dl b/logic/local.dl index 002af766..b6a6687a 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -466,26 +466,14 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- Statement_Opcode(stmt, opcode), OpcodeGas(opcode, gas). - .decl PublicFunctionJump(block:Block, funHex: Value, optionalSelector: OptionalSelector) - .decl PublicFunction(block:Block, funHex: Value, optionalSelector: OptionalSelector) + .decl PublicFunctionJump(block: Block, funHex: Value, optionalSelector: OptionalSelector) + .decl PublicFunction(block: Block, funHex: Value, optionalSelector: OptionalSelector) - // Code inserted by compiler to compare function signature - .decl BlockComparesSig(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) + .decl IsOptionalSelector(optionalSelector: OptionalSelector) - // Compares label from stack to a constant: common public function dispatch pattern - BlockComparesSig(block, sigHash, selector) :- - Statement_Block(pushStmt, block), - ImmediateBlockJumpTarget(block, _), - (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), - Statement_Defines(pushStmt, sigHashVar), - EQ(eqStmt), - Statement_Uses_Local(eqStmt, sigHashVar, n), - Statement_Uses_Local(eqStmt, selectorVarOrIndex, 1 - n), - ((CheckIsStackIndex(selectorVarOrIndex), selector = $SelectorStackIndex(block, selectorVarOrIndex)); - (CheckIsVariable(selectorVarOrIndex), selector = $SelectorVariable(selectorVarOrIndex))), - Statement_Defines(eqStmt, pred), - JUMPI(jumpiStmt), - Statement_Uses_Local(jumpiStmt, pred, 1). + IsOptionalSelector(optionalSelector):- + PublicFunctionJump(_, _, optionalSelector); + PublicFunction(_, _, optionalSelector). .decl SWAPDUPPOPJUMPJUMPDESTOP(op: Opcode) SWAPDUPPOPJUMPJUMPDESTOP(opcode):- @@ -696,6 +684,30 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- ByteCodeHex(bytecodeStr), const = cat("0x", substr(bytecodeStr, 2*codeOffsetNum, 2*smallNum)). + IsOptionalSelector(selectorVarOrIndex):- + BlockComparesSig(_, _, selectorVarOrIndex); + BlockComparesSigFallthroughSolidity(_, _, selectorVarOrIndex); + BlockComparesSigVyper(_, _, selectorVarOrIndex). + + // Code inserted by compiler to compare function signature + .decl BlockComparesSig(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) + + // Compares label from stack to a constant: common public function dispatch pattern + BlockComparesSig(block, sigHash, selector) :- + Statement_Block(pushStmt, block), + ImmediateBlockJumpTarget(block, _), + (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), + Statement_Defines(pushStmt, sigHashVar), + EQ(eqStmt), + Statement_Uses_Local(eqStmt, sigHashVar, n), + Statement_Uses_Local(eqStmt, selectorVarOrIndex, 1 - n), + ((CheckIsStackIndex(selectorVarOrIndex), selector = $SelectorStackIndex(block, selectorVarOrIndex)); + (CheckIsVariable(selectorVarOrIndex), selector = $SelectorVariable(selectorVarOrIndex))), + Statement_Defines(eqStmt, pred), + JUMPI(jumpiStmt), + Statement_Uses_Local(jumpiStmt, pred, 1). + + .decl BlockComparesSigVyper(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) .decl BlockComparesSigVyperBase(block: Block, sigHash: Value, selectorVarOrIndex: VariableOrStackIndex) @@ -928,9 +940,9 @@ insertor.insertOps(functionStartStmt, // Receive transformation insertor.insertOps(functionStartStmt, LIST( - STMT(PUSH4, MAKE_LABEL_REFERENCE("0x00000000")), - STMT(JUMP, cat("PublicFunctionJump:", "0x00000000")), - STMT(JUMPDEST, MAKE_LABEL_REFERENCE("0x00000000")) + STMT(PUSH4, MAKE_LABEL_REFERENCE(RECEIVE_FUNCTION_SIGHASH)), + STMT(JUMP, cat("PublicFunctionJump:", RECEIVE_FUNCTION_SIGHASH)), + STMT(JUMPDEST, MAKE_LABEL_REFERENCE(RECEIVE_FUNCTION_SIGHASH)) ) ) :- preTrans.BlockHasReceiveAsFallThrough(_, _, functionStartStmt, _). @@ -1024,7 +1036,7 @@ postTrans.PublicFunctionJump(block, hash, selector) :- (preTrans.PublicFunctionJump(_, hash, selector); preTrans.BlockComparesSigVyper(_, hash, selector); preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); - (preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = "0x00000000", selector = $NoSelector()) + (preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = RECEIVE_FUNCTION_SIGHASH, selector = $NoSelector()) ). // we may lose some precision here when two blocks have the same hex @@ -1048,7 +1060,7 @@ postTrans.PublicFunction(block, hash, selector) :- // For receive functions postTrans.PublicFunction(block, hash, $NoSelector()) :- preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), - hash = "0x00000000", + hash = RECEIVE_FUNCTION_SIGHASH, hash = GET_LABEL_REFERENCE(meta), ISLABEL(meta), insertor.MetaData(stmt, meta), postTrans.JUMPDEST(stmt), diff --git a/logic/main.dl b/logic/main.dl index 0627174c..815f0e08 100644 --- a/logic/main.dl +++ b/logic/main.dl @@ -1,5 +1,5 @@ #define FALLBACK_FUNCTION_SIGHASH "0x00000000" - +#define RECEIVE_FUNCTION_SIGHASH "0xeeeeeeee" /* From 2fee34270c1976ea1165891abab468611c8ee1c5 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Mon, 11 Dec 2023 15:54:19 +0200 Subject: [PATCH 12/28] Refactor receive logic to support viaIr pattern --- logic/local.dl | 64 +++++++++++++++++++++++++++---------- logic/statement_insertor.dl | 7 +++- 2 files changed, 53 insertions(+), 18 deletions(-) diff --git a/logic/local.dl b/logic/local.dl index b6a6687a..47115dc1 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -771,43 +771,70 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- PushValue(push, targetValue), JUMPDEST(as(targetValue, symbol)). - .decl BlockComparesCallDataSizeToFour(block: Block, jumpi: Statement, target: Block) - .decl BlockJumpsOnCallDataSize(block: Block, jumpi: Statement, target: Block) - .decl BlockHasReceiveAsFallThrough(block: Block, jumpi: Statement, fallthrough:Statement, target: Block) + .decl BlockComparesCallDataSizeToFour(block: Block, jumpi: Statement, lessThanFourTarget: Block) + .decl BlockJumpsOnCallDataSize(block: Block, jumpi: Statement, noCallDataBranch: Block, callDataBranch: Block) + .decl BlockHasReceiveAsFallThrough(block: Block, jumpi: Statement, fallthrough: Block, target: Block) - BlockComparesCallDataSizeToFour(block, stmt5, as(fallthrough, Block)):- + BlockComparesCallDataSizeToFour(block, stmt5, as(target, Block)):- PushValue(stmt, "0x4"), Statement_Next(stmt, stmt2), CALLDATASIZE(stmt2), Statement_Next(stmt2, stmt3), LT(stmt3), Statement_Next(stmt3, stmt4), - PushValue(stmt4, fallthrough), + PushValue(stmt4, target), Statement_Next(stmt4, stmt5), JUMPI(stmt5), Statement_Block(stmt5, block), - JUMPDEST(as(fallthrough, Statement)). + JUMPDEST(as(target, Statement)). - BlockJumpsOnCallDataSize(block, jumpi, as(fallthrough, Block)):- + BlockComparesCallDataSizeToFour(block, stmt6, as(fallthrough, Block)):- + PushValue(stmt, "0x4"), + Statement_Next(stmt, stmt2), + CALLDATASIZE(stmt2), + Statement_Next(stmt2, stmt3), + LT(stmt3), + Statement_Next(stmt3, stmt4), + ISZERO(stmt4), + Statement_Next(stmt4, stmt5), + PushValue(stmt5, _), + Statement_Next(stmt5, stmt6), + JUMPI(stmt6), + Statement_Block(stmt6, block), + Statement_Next(stmt6, fallthrough). + + BlockJumpsOnCallDataSize(block, jumpi, as(fallthrough, Block), as(callDataSizeBranch, Block)):- CALLDATASIZE(cds), Statement_Next(cds, push), - PushValue(push, fallthrough), + PushValue(push, callDataSizeBranch), Statement_Next(push, jumpi), JUMPI(jumpi), Statement_Block(jumpi, block), - JUMPDEST(as(fallthrough, Statement)). + Statement_Next(jumpi, fallthrough), + JUMPDEST(as(callDataSizeBranch, Statement)). + + BlockJumpsOnCallDataSize(block, jumpi, as(noCallDataSizeBranch, Block), as(fallthrough, Block)):- + CALLDATASIZE(cds), + Statement_Next(cds, isZero), + ISZERO(isZero), + Statement_Next(isZero, push), + PushValue(push, noCallDataSizeBranch), + Statement_Next(push, jumpi), + JUMPI(jumpi), + Statement_Block(jumpi, block), + Statement_Next(jumpi, fallthrough), + JUMPDEST(as(noCallDataSizeBranch, Statement)). // Fallback functions PublicFunctionJump(block, FALLBACK_FUNCTION_SIGHASH, $NoSelector()), PublicFunction(fallbackStart, FALLBACK_FUNCTION_SIGHASH, $NoSelector()):- BlockComparesCallDataSizeToFour(block, _, fallbackStart), 1 = count : BlockComparesCallDataSizeToFour(_, _, _), - !BlockJumpsOnCallDataSize(fallbackStart, _, _). + !BlockJumpsOnCallDataSize(fallbackStart, _, _, _). - BlockHasReceiveAsFallThrough(block, jumpi, fallthrough, target):- + BlockHasReceiveAsFallThrough(block, jumpi, noCallDataSizeBranch, callDataSizeBranch):- BlockComparesCallDataSizeToFour(_, _, block), - BlockJumpsOnCallDataSize(block, jumpi, target), - FallthroughStmt(jumpi, fallthrough). + BlockJumpsOnCallDataSize(block, jumpi, noCallDataSizeBranch, callDataSizeBranch). } @@ -938,14 +965,18 @@ insertor.insertOps(functionStartStmt, !preTrans.BlockComparesSig(_, hash, _). // Receive transformation -insertor.insertOps(functionStartStmt, +insertor.insertOps(insertStmt, LIST( STMT(PUSH4, MAKE_LABEL_REFERENCE(RECEIVE_FUNCTION_SIGHASH)), STMT(JUMP, cat("PublicFunctionJump:", RECEIVE_FUNCTION_SIGHASH)), STMT(JUMPDEST, MAKE_LABEL_REFERENCE(RECEIVE_FUNCTION_SIGHASH)) ) ) :- - preTrans.BlockHasReceiveAsFallThrough(_, _, functionStartStmt, _). + preTrans.BlockHasReceiveAsFallThrough(_, _, functionStart, _), + preTrans.BasicBlock_Head(functionStart, functionStartStmt), + preTrans.Statement_Opcode(functionStartStmt, op), + ((op != "JUMPDEST", insertStmt = functionStartStmt); + (op = "JUMPDEST", preTrans.Statement_Next(functionStartStmt, insertStmt))). // This one removes "throw jumps" insertor.removeOp(jmp), @@ -1030,9 +1061,8 @@ insertor.insertOps(codeCopy, // For Solidity, Vyper postTrans.PublicFunctionJump(block, hash, selector) :- insertor.MetaData(stmt, meta), - STARTSWITH(meta, "PublicFunctionJump:"), + insertor.PublicFunctionJumpMetadata(meta, hash), postTrans.Statement_Block(stmt, block), - hash = substr(meta, 19, 30), (preTrans.PublicFunctionJump(_, hash, selector); preTrans.BlockComparesSigVyper(_, hash, selector); preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); diff --git a/logic/statement_insertor.dl b/logic/statement_insertor.dl index e5f910be..7f8acbb8 100644 --- a/logic/statement_insertor.dl +++ b/logic/statement_insertor.dl @@ -60,7 +60,9 @@ to.PublicFunction(block, funHex, selector):- from.PublicFunction(block, funHex, removeOp(stmt) :- removeOp(stmt). // suppress warning .decl MetaData(newStmt: Statement, value: Value) - + + .decl PublicFunctionJumpMetadata(metadataValue: Value, publicFunctionHex: Value) + // Simple translation .decl insertOp(stmt: Statement, op: Opcode, value: Value, order: number) @@ -133,6 +135,9 @@ to.PublicFunction(block, funHex, selector):- from.PublicFunction(block, funHex, insertOp(stmt, op, value, order), !OpcodeIsPush(op). + PublicFunctionJumpMetadata(meta, substr(meta, 19, 30)):- + MetaData(_, meta), + STARTSWITH(meta, "PublicFunctionJump:"). Out_PushValue(newStmt, value) :- InsertedOpNewStatement(stmt, order, newStmt), From 94f15fcdbcce70afc835c6b33d06a4419ca80bdb Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Mon, 11 Dec 2023 17:35:05 +0200 Subject: [PATCH 13/28] Remove wrong public function inferences before transformations --- logic/global.dl | 20 +++++++++++++++++++- logic/local.dl | 21 ++++++++++++++++++--- 2 files changed, 37 insertions(+), 4 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index 28ab9c15..d8c6a9e3 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -281,6 +281,19 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- ValidPublicFunctionJump(_, hex, selector), PublicFunction(startBlock, hex, selector). + .decl ValidSelector(selector: OptionalSelector) + + ValidSelector($NoSelector()). + + ValidSelector($SelectorVariable(selectorVariable)):- + IsOptionalSelector($SelectorVariable(selectorVariable)), + FunctionSelectorVariable(selectorVariable). + + ValidSelector($SelectorStackIndex(block, selectorStackIndex)):- + IsOptionalSelector($SelectorStackIndex(block, selectorStackIndex)), + BlockInputContents(_, block, selectorStackIndex, selectorVariable), + FunctionSelectorVariable(selectorVariable). + } /** @@ -290,6 +303,11 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .override BlockInputContents + .decl VariableToModel(var: Variable) + VariableToModel(var):- + VariableContainsJumpTarget(var); FunctionSelectorVariable(var). + + /** Cut down `BlockOutputContents`, only containing jump targets (and the function selector var). Stack contents at end of a `block`, given its calling `context`. @@ -297,7 +315,7 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- .decl AuxBlockOutputContentsJumpTarget(context:sens.Context, block:Block, index:StackIndex, var:Variable) AuxBlockOutputContentsJumpTarget(context, block, index, var) :- BlockOutputContents(context, block, index, var), - (VariableContainsJumpTarget(var); FunctionSelectorVariable(var)). + VariableToModel(var). BlockInputContents(calleeCtx, callee, index, variable) :- AuxBlockOutputContentsJumpTarget(callerCtx, caller, index, variable), diff --git a/logic/local.dl b/logic/local.dl index 47115dc1..2e709b08 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -888,6 +888,8 @@ PreTransStatement_OriginalStatement(rvtClStmt, ogStmt) :- .init revertCloner = RevertBlockCloner COPY_CODE(revertCloner, factReader) +.decl ValidSelector(optionalSelector: OptionalSelector) + #ifdef BLOCK_CLONING // Enable the early cloning of blocks to increase precision (sacrificing performance) .init blockCloner = BLOCK_CLONING @@ -903,10 +905,16 @@ PreTransStatement_OriginalStatement(heurClStmt, ogStmt) :- blockCloner.StatementToClonedStatement(_, _, ogStmt, heurClStmt), !revertCloner.StatementToClonedStatement(_, _, _, ogStmt). +ValidSelector(optionalSelector):- + blockCloner.analysis.ValidSelector(optionalSelector). + #else COPY_OUTPUT(preTrans, revertCloner) +ValidSelector(optionalSelector):- + preTrans.IsOptionalSelector(optionalSelector). + #endif INITIALIZE_STATEMENT_INSERTOR_FROM(insertor, preTrans, postTrans) @@ -930,6 +938,7 @@ insertor.insertOps(jumpDestStmt, ) :- preTrans.PublicFunctionJump(block, hash, selector), preTrans.PublicFunction(start, hash, selector), + ValidSelector(selector), preTrans.Statement_Block(jumpDestStmt, start), preTrans.JUMPDEST(jumpDestStmt), preTrans.PushValue(pushStmt, as(jumpDestStmt, symbol)), @@ -946,7 +955,8 @@ insertor.insertOps(functionStartStmt, STMT(JUMPDEST, MAKE_LABEL_REFERENCE(hash)) ) ) :- - preTrans.BlockComparesSigVyper(block, hash, _), + preTrans.BlockComparesSigVyper(block, hash, selector), + ValidSelector(selector), preTrans.BasicBlock_Tail(block, tail), preTrans.Statement_Next(tail, functionStartStmt), !preTrans.BlockComparesSig(_, _, _). @@ -959,7 +969,8 @@ insertor.insertOps(functionStartStmt, STMT(JUMPDEST, MAKE_LABEL_REFERENCE(hash)) ) ) :- - preTrans.BlockComparesSigFallthroughSolidity(block, hash, _), + preTrans.BlockComparesSigFallthroughSolidity(block, hash, selector), + ValidSelector(selector), preTrans.BasicBlock_Tail(block, tail), preTrans.Statement_Next(tail, functionStartStmt), !preTrans.BlockComparesSig(_, hash, _). @@ -1063,6 +1074,7 @@ postTrans.PublicFunctionJump(block, hash, selector) :- insertor.MetaData(stmt, meta), insertor.PublicFunctionJumpMetadata(meta, hash), postTrans.Statement_Block(stmt, block), + ValidSelector(selector), (preTrans.PublicFunctionJump(_, hash, selector); preTrans.BlockComparesSigVyper(_, hash, selector); preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); @@ -1076,6 +1088,7 @@ postTrans.PublicFunction(block, hash, selector):- postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block), preTrans.BlockComparesSigVyper(_, hash, selector), + ValidSelector(selector), !preTrans.BlockComparesSig(_, _, _), ISLABEL(meta), hash = GET_LABEL_REFERENCE(meta). @@ -1084,6 +1097,7 @@ postTrans.PublicFunction(block, hash, selector) :- postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block), preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector), + ValidSelector(selector), !preTrans.BlockComparesSig(_, hash, _), ISLABEL(meta), hash = GET_LABEL_REFERENCE(meta). @@ -1096,7 +1110,8 @@ postTrans.PublicFunction(block, hash, $NoSelector()) :- postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block). -postTrans.PublicFunction(b, h, s) :- preTrans.PublicFunction(b, h, s). +postTrans.PublicFunction(b, h, s) :- preTrans.PublicFunction(b, h, s), ValidSelector(s). + .output postTrans.PublicFunction, preTrans.PublicFunction, preTrans.BlockComparesSigFallthroughSolidity, preTrans.BlockComparesSigVyper, insertor.MetaData .output postTrans.PublicFunctionJump // Code chunking logic reserved for future EIP From 7ce1b2286508ee668e387b4e1ea5c7c9c8f16c3f Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Mon, 11 Dec 2023 22:50:06 +0200 Subject: [PATCH 14/28] remove 2nd check for wrongly infered public functions --- logic/global.dl | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index d8c6a9e3..1cac6844 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -54,12 +54,12 @@ global.StatementPushesUsedLabel(stmt):- incompleteGlobal.VariableUsedInAsJumpdest(pushedVar), postTrans.Statement_Defines(stmt, pushedVar). -COPY_CODE(global, postTrans) -global.PublicFunctionJump(block, hex, selector):- - incompleteGlobal.ValidPublicFunctionJump(block, hex, selector). +COPY_CODE_FULL(global, postTrans) +// global.PublicFunctionJump(block, hex, selector):- +// incompleteGlobal.ValidPublicFunctionJump(block, hex, selector). -global.PublicFunction(start, hex, selector):- - incompleteGlobal.ValidPublicFunction(start, hex, selector). +// global.PublicFunction(start, hex, selector):- +// incompleteGlobal.ValidPublicFunction(start, hex, selector). // Masks with all 1s .decl Mask_Length(mask: Value, bytes: number) From 129c9134a2ee87e0c81547f5b28320e438c3cb4e Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 10:16:59 +0200 Subject: [PATCH 15/28] remove more --- logic/functions.dl | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/logic/functions.dl b/logic/functions.dl index 9a54799b..36a25b1c 100644 --- a/logic/functions.dl +++ b/logic/functions.dl @@ -262,9 +262,8 @@ IsFunctionCallReturn(ctx, caller, func, retCtx, retBlock, retTarget) :- .decl PublicFunctionFiltered(block: Block, sigHash: Value) PublicFunctionFiltered(func, sigHash):- - postTrans.PublicFunctionJump(prev, sigHash, selector), + postTrans.PublicFunctionJump(prev, sigHash, _), postTrans.PublicFunction(func, sigHash, _), - global.ValidPublicFunctionJump(prev, sigHash, selector), global.BlockEdge(_, prev, _, func). // NOTE the philosophy! MaybeFunctionCallReturn intends to be From 44178dd3aaad25073a95300a151834911e2967d6 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 10:43:21 +0200 Subject: [PATCH 16/28] cleanup --- logic/global.dl | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/logic/global.dl b/logic/global.dl index 1cac6844..556e1f4d 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -55,11 +55,6 @@ global.StatementPushesUsedLabel(stmt):- postTrans.Statement_Defines(stmt, pushedVar). COPY_CODE_FULL(global, postTrans) -// global.PublicFunctionJump(block, hex, selector):- -// incompleteGlobal.ValidPublicFunctionJump(block, hex, selector). - -// global.PublicFunction(start, hex, selector):- -// incompleteGlobal.ValidPublicFunction(start, hex, selector). // Masks with all 1s .decl Mask_Length(mask: Value, bytes: number) @@ -261,26 +256,6 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- VariableContainsJumpTarget(var), !VariableUsedInOperation(var). - .decl ValidPublicFunctionJump(jumpBlock: Block, hex: Value, selector: OptionalSelector) - .decl ValidPublicFunction(startBlock: Block, hex: Value, selector: OptionalSelector) - DEBUG_OUTPUT(ValidPublicFunctionJump) - - ValidPublicFunctionJump(jumpBlock, hex, $SelectorStackIndex(block, selectorStackIndex)):- - PublicFunctionJump(jumpBlock, hex, $SelectorStackIndex(block, selectorStackIndex)), - BlockInputContents(_, block, selectorStackIndex, selectorVariable), - FunctionSelectorVariable(selectorVariable). - - ValidPublicFunctionJump(jumpBlock, hex, $SelectorVariable(selectorVariable)):- - PublicFunctionJump(jumpBlock, hex, $SelectorVariable(selectorVariable)), - FunctionSelectorVariable(selectorVariable). - - ValidPublicFunctionJump(jumpBlock, hex, $NoSelector()):- - PublicFunctionJump(jumpBlock, hex, $NoSelector()). - - ValidPublicFunction(startBlock, hex, selector):- - ValidPublicFunctionJump(_, hex, selector), - PublicFunction(startBlock, hex, selector). - .decl ValidSelector(selector: OptionalSelector) ValidSelector($NoSelector()). From 66bd7d0059eb07eac888c04c4244f12b3ab03c44 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 12:11:29 +0200 Subject: [PATCH 17/28] Allow for selectors smaller than 3 bytes --- logic/local.dl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/logic/local.dl b/logic/local.dl index 2e709b08..890acbf0 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -689,6 +689,14 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- BlockComparesSigFallthroughSolidity(_, _, selectorVarOrIndex); BlockComparesSigVyper(_, _, selectorVarOrIndex). + // All pushes of values up to 4 bytes, can be used as selectors + .decl SmallValuePush(pushStmt: Statement, value: Value) + SmallValuePush(pushStmt, value):- + PUSH4(pushStmt, value); + PUSH3(pushStmt, value); + PUSH2(pushStmt, value); + PUSH1(pushStmt, value). + // Code inserted by compiler to compare function signature .decl BlockComparesSig(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector) @@ -696,7 +704,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- BlockComparesSig(block, sigHash, selector) :- Statement_Block(pushStmt, block), ImmediateBlockJumpTarget(block, _), - (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), + SmallValuePush(pushStmt, sigHash), Statement_Defines(pushStmt, sigHashVar), EQ(eqStmt), Statement_Uses_Local(eqStmt, sigHashVar, n), From 7e50c3a5f985aa550e0ba0771bb7aaf883d8362a Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 14:36:13 +0200 Subject: [PATCH 18/28] remove heavy relations from debug.dl --- logic/debug.dl | 78 +++++++++++++++++++++++++------------------------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/logic/debug.dl b/logic/debug.dl index 1cbafc5c..03fc2014 100644 --- a/logic/debug.dl +++ b/logic/debug.dl @@ -82,55 +82,55 @@ MaybeInFunctionUnderContextOrd(ord(ctx), block, func):- MaybeInFunctionUnderContext(ctx, block, func). -.decl CFGImprecisionPersists(srcCtx: global.sens.Context, srcBlk: Block, currCtx: global.sens.Context, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) -.output CFGImprecisionPersists +// .decl CFGImprecisionPersists(srcCtx: global.sens.Context, srcBlk: Block, currCtx: global.sens.Context, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) +// .output CFGImprecisionPersists -.decl CFGImprecisionInstance(ctx: global.sens.Context, blk: Block, targetVar1: Variable, targetVar2: Variable) +// .decl CFGImprecisionInstance(ctx: global.sens.Context, blk: Block, targetVar1: Variable, targetVar2: Variable) -CFGImprecisionPersists(ctx, block, ctx, block, targetVar1, targetVar2, 0), -CFGImprecisionInstance(ctx, block, targetVar1, targetVar2):- - global.BlockJumpValidTarget(ctx, block, targetVar1, _), - global.BlockJumpValidTarget(ctx, block, targetVar2, _), - targetVar1 < targetVar2. +// CFGImprecisionPersists(ctx, block, ctx, block, targetVar1, targetVar2, 0), +// CFGImprecisionInstance(ctx, block, targetVar1, targetVar2):- +// global.BlockJumpValidTarget(ctx, block, targetVar1, _), +// global.BlockJumpValidTarget(ctx, block, targetVar2, _), +// targetVar1 < targetVar2. -CFGImprecisionPersists(srcCtx, srcBlock, prevCtx, prevBlock, targetVar1, targetVar2, pathLen + 1):- - CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen), - global.BlockEdge(prevCtx, prevBlock, ctx, block), - global.BlockInputContents(prevCtx, prevBlock, someIndex, targetVar1), - global.BlockInputContents(prevCtx, prevBlock, someIndex, targetVar2), - pathLen < 30. +// CFGImprecisionPersists(srcCtx, srcBlock, prevCtx, prevBlock, targetVar1, targetVar2, pathLen + 1):- +// CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen), +// global.BlockEdge(prevCtx, prevBlock, ctx, block), +// global.BlockInputContents(prevCtx, prevBlock, someIndex, targetVar1), +// global.BlockInputContents(prevCtx, prevBlock, someIndex, targetVar2), +// pathLen < 30. -.decl CFGImprecisionPersistsOrd(srcCtx: number, srcBlk: Block, currCtx: number, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) -.output CFGImprecisionPersistsOrd +// .decl CFGImprecisionPersistsOrd(srcCtx: number, srcBlk: Block, currCtx: number, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) +// .output CFGImprecisionPersistsOrd -CFGImprecisionPersistsOrd(ord(srcCtx), srcBlock, ord(ctx), block, targetVar1, targetVar2, pathLen):- - CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen). +// CFGImprecisionPersistsOrd(ord(srcCtx), srcBlock, ord(ctx), block, targetVar1, targetVar2, pathLen):- +// CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen). -.decl CFGImprecisionIntroducedOrd(srcCtx: number, srcBlk: Block, prevCtx: number, prevBlock: Block, currCtx: number, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) -.output CFGImprecisionIntroducedOrd +// .decl CFGImprecisionIntroducedOrd(srcCtx: number, srcBlk: Block, prevCtx: number, prevBlock: Block, currCtx: number, currBlk: Block, targetVar1: Variable, targetVar2: Variable, pathLen: number) +// .output CFGImprecisionIntroducedOrd -CFGImprecisionIntroducedOrd(ord(srcCtx), srcBlock, ord(prevCtx), prevBlock, ord(ctx), block, targetVar1, targetVar2, pathLen):- - CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen), - global.BlockEdge(prevCtx, prevBlock, ctx, block), - pathLen != 30, - !CFGImprecisionPersists(srcCtx, srcBlock, prevCtx, prevBlock, targetVar1, targetVar2, _). +// CFGImprecisionIntroducedOrd(ord(srcCtx), srcBlock, ord(prevCtx), prevBlock, ord(ctx), block, targetVar1, targetVar2, pathLen):- +// CFGImprecisionPersists(srcCtx, srcBlock, ctx, block, targetVar1, targetVar2, pathLen), +// global.BlockEdge(prevCtx, prevBlock, ctx, block), +// pathLen != 30, +// !CFGImprecisionPersists(srcCtx, srcBlock, prevCtx, prevBlock, targetVar1, targetVar2, _). -.decl CFGImprecisionIntroducedForwardOrd(ctx: number, block: Block, targetVar1: Variable, targetVar2: Variable) -.output CFGImprecisionIntroducedForwardOrd +// .decl CFGImprecisionIntroducedForwardOrd(ctx: number, block: Block, targetVar1: Variable, targetVar2: Variable) +// .output CFGImprecisionIntroducedForwardOrd -.decl CFGImprecisionExists(ctx: global.sens.Context, block: Block, targetVar1: Variable, targetVar2: Variable) +// .decl CFGImprecisionExists(ctx: global.sens.Context, block: Block, targetVar1: Variable, targetVar2: Variable) -CFGImprecisionExists(ctx, block, targetVar1, targetVar2):- - CFGImprecisionInstance(_, _, targetVar1, targetVar2), - global.BlockInputContents(ctx, block, someIndex, targetVar1), - global.BlockInputContents(ctx, block, someIndex, targetVar2). +// CFGImprecisionExists(ctx, block, targetVar1, targetVar2):- +// CFGImprecisionInstance(_, _, targetVar1, targetVar2), +// global.BlockInputContents(ctx, block, someIndex, targetVar1), +// global.BlockInputContents(ctx, block, someIndex, targetVar2). -.decl CFGImprecisionExistsInPrev(ctx: global.sens.Context, block: Block, prevCtx: global.sens.Context, prevBlock: Block, targetVar1: Variable, targetVar2: Variable) +// .decl CFGImprecisionExistsInPrev(ctx: global.sens.Context, block: Block, prevCtx: global.sens.Context, prevBlock: Block, targetVar1: Variable, targetVar2: Variable) -CFGImprecisionExistsInPrev(ctx, block, prevCtx, prevBlock, targetVar1, targetVar2):- - CFGImprecisionExists(prevCtx, prevBlock, targetVar1, targetVar2), - global.BlockEdge(prevCtx, prevBlock, ctx, block). +// CFGImprecisionExistsInPrev(ctx, block, prevCtx, prevBlock, targetVar1, targetVar2):- +// CFGImprecisionExists(prevCtx, prevBlock, targetVar1, targetVar2), +// global.BlockEdge(prevCtx, prevBlock, ctx, block). -CFGImprecisionIntroducedForwardOrd(ord(ctx), block, targetVar1, targetVar2):- - CFGImprecisionExists(ctx, block, targetVar1, targetVar2), - !CFGImprecisionExistsInPrev(ctx, block, _, _, targetVar1, targetVar2). \ No newline at end of file +// CFGImprecisionIntroducedForwardOrd(ord(ctx), block, targetVar1, targetVar2):- +// CFGImprecisionExists(ctx, block, targetVar1, targetVar2), +// !CFGImprecisionExistsInPrev(ctx, block, _, _, targetVar1, targetVar2). \ No newline at end of file From 8e77265737d4f9a49f9974c60f50d15b94781f18 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 14:38:02 +0200 Subject: [PATCH 19/28] Create public function context on PublicFunctionJump instead of PublicFunction --- logic/context-sensitivity/abstract_context.dl | 4 ++-- .../transactional_shrinking_context.dl | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/logic/context-sensitivity/abstract_context.dl b/logic/context-sensitivity/abstract_context.dl index b9abdfbc..3fe0ae60 100644 --- a/logic/context-sensitivity/abstract_context.dl +++ b/logic/context-sensitivity/abstract_context.dl @@ -282,14 +282,14 @@ #ifndef NO_PUBLIC_CONTEXT MergeContext(ctx, caller, ctx) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash, _), + local.PublicFunctionJump(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. .plan 1:(3,1,2) MergeContext(ctx, caller, newContext):- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash, _), + local.PublicFunctionJump(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, pri), prevSigHash = FALLBACK_FUNCTION_SIGHASH, diff --git a/logic/context-sensitivity/transactional_shrinking_context.dl b/logic/context-sensitivity/transactional_shrinking_context.dl index a5ba4521..104abd6e 100644 --- a/logic/context-sensitivity/transactional_shrinking_context.dl +++ b/logic/context-sensitivity/transactional_shrinking_context.dl @@ -5,12 +5,12 @@ // Split into two rules to add plan. MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). .plan 1:(2,3,1) @@ -29,7 +29,7 @@ ReachableContext(ctx, caller), local.PrivateFunctionCall(caller, _, _, _), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), newPrivateContext = [caller, cutDownAtEndPri]. .plan 1:(3,1,2) @@ -78,7 +78,7 @@ MergeContextRequest(ctx, block, cont), PrivateFunctionReturn(block), DecomposeContext(ctx, pub, priCtx), - !local.PublicFunction(block, _, _), + !local.PublicFunctionJump(block, _, _), CutToCaller(priCtx, cont, cutPri). .plan 1:(3,1,2,4), 2:(4,3,1,2) @@ -89,7 +89,7 @@ DecomposeContext(ctx, pub, priCtx), DecomposeAndTruncateIfNeeded(ctx, pub, cutDownAtEndPri), NoCutToCaller(priCtx, cont), - !local.PublicFunction(block, _, _), + !local.PublicFunctionJump(block, _, _), newPrivateContext = [block, cutDownAtEndPri]. .plan 1:(3,1,2,4,5), 2:(4,3,1,2,5), 3:(5,3,1,2,4) From 9af8fb8b7eb439bb5af174b900355c4570feaf10 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Tue, 12 Dec 2023 16:52:43 +0200 Subject: [PATCH 20/28] Skip library_deploy_address in immutable refs. --- src/exporter.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/exporter.py b/src/exporter.py index be009b9a..b40be476 100644 --- a/src/exporter.py +++ b/src/exporter.py @@ -131,6 +131,9 @@ def process_function_debug_data(function_debug_data: Dict[str, Dict[str, Optiona def process_immutable_refs(immutable_refs: Dict[str, List[Dict[str, int]]]) -> List[Tuple[str, int]]: res = [] for id, accesses in immutable_refs.items(): + # TODO: skipping this for now + if id == "library_deploy_address": + continue for access in accesses: res.append((hex(access['start']), int(id))) return res From b7ae3a4e8f59831a9def7b23061bf7b7201bd359 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 14 Dec 2023 16:17:15 +0200 Subject: [PATCH 21/28] Refactor, allow MergeRequests and responses for fallthrough edges as well. --- logic/context-sensitivity/abstract_context.dl | 38 +++++++++++++++---- .../transactional_context.dl | 6 +-- logic/global.dl | 37 +++++++++++------- logic/local.dl | 15 +++++--- 4 files changed, 66 insertions(+), 30 deletions(-) diff --git a/logic/context-sensitivity/abstract_context.dl b/logic/context-sensitivity/abstract_context.dl index 3fe0ae60..bf9f7a08 100644 --- a/logic/context-sensitivity/abstract_context.dl +++ b/logic/context-sensitivity/abstract_context.dl @@ -280,21 +280,43 @@ */ #ifndef NO_PUBLIC_CONTEXT - MergeContext(ctx, caller, ctx) :- - ReachableContext(ctx, caller), + // MergeContext(ctx, caller, ctx) :- + // ReachableContext(ctx, caller), + // local.PublicFunctionJump(caller, sigHash, _), + // !MaxContextDepth(sigHash, -1), + // DecomposeContext(ctx, prevSigHash, _), + // prevSigHash != FALLBACK_FUNCTION_SIGHASH. + // .plan 1:(3,1,2) + // MergeContext(ctx, caller, newContext):- + // ReachableContext(ctx, caller), + // local.PublicFunctionJump(caller, sigHash, _), + // !MaxContextDepth(sigHash, -1), + // DecomposeContext(ctx, prevSigHash, pri), + // prevSigHash = FALLBACK_FUNCTION_SIGHASH, + // newContext = [sigHash, pri]. + // .plan 1:(3,1,2) + + MergeContextResponse(ctx, caller, funcStart, ctx) :- + MergeContextRequest(ctx, caller, funcStart), local.PublicFunctionJump(caller, sigHash, _), + local.PublicFunction(funcStart, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, prevSigHash, _), prevSigHash != FALLBACK_FUNCTION_SIGHASH. - .plan 1:(3,1,2) - MergeContext(ctx, caller, newContext):- - ReachableContext(ctx, caller), + .plan 1:(4,1,2,3) + MergeContextResponse(ctx, caller, funcStart, newContext) :- + MergeContextRequest(ctx, caller, funcStart), local.PublicFunctionJump(caller, sigHash, _), + local.PublicFunction(funcStart, sigHash, _), !MaxContextDepth(sigHash, -1), - DecomposeContext(ctx, prevSigHash, pri), - prevSigHash = FALLBACK_FUNCTION_SIGHASH, + DecomposeContext(ctx, FALLBACK_FUNCTION_SIGHASH, pri), newContext = [sigHash, pri]. - .plan 1:(3,1,2) + MergeContextResponse(ctx, caller, funcStart, ctx) :- + MergeContextRequest(ctx, caller, funcStart), + local.PublicFunctionJump(caller, sigHash, _), + !local.PublicFunction(funcStart, sigHash, _), + !MaxContextDepth(sigHash, -1). + #endif } diff --git a/logic/context-sensitivity/transactional_context.dl b/logic/context-sensitivity/transactional_context.dl index 72a9bcdc..5cbda64b 100644 --- a/logic/context-sensitivity/transactional_context.dl +++ b/logic/context-sensitivity/transactional_context.dl @@ -5,14 +5,14 @@ MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), #endif !local.PrivateFunctionCallOrReturn(caller). MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), #endif DecomposeContext(ctx, pub, _), MaxContextDepth(pub, 0). @@ -26,7 +26,7 @@ DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), #ifndef NO_PUBLIC_CONTEXT - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), #endif newPrivateContext = [caller, cutDownPri]. .plan 1:(3,1,2,4), 2:(4,3,1,2) diff --git a/logic/global.dl b/logic/global.dl index 556e1f4d..9e69fcbc 100644 --- a/logic/global.dl +++ b/logic/global.dl @@ -114,12 +114,17 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- */ .decl BlockJumpValidTarget(ctx: sens.Context, block: Block, var: Variable, target: Block) + /** + Under `ctx`, `next` can follow the execution of `block`. + Includes both fallthrough edges and jumps. + */ + .decl BlockValidNext(ctx: sens.Context, block: Block, next: Block) + /** When `block` is analyzed under `callerCtx`, there will be a CFG edge from `block` to `callee`, causing it to be reachable under `calleeCtx` */ .decl BlockEdge(callerCtx: sens.Context, caller: Block, calleeCtx: sens.Context, callee: Block) - /* @@ -183,31 +188,34 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- ReachableContext(calleeCtx, callee) :- BlockEdge(_, _, calleeCtx, callee). - + ReachableContext(initCtx, FUNCTION_SELECTOR) :- sens.InitialContext(initCtx). - .decl FallthroughEdge(caller: Block, fallthroughBlock: Block) + BlockValidNext(ctx, block, next):- + BlockJumpValidTarget(ctx, block, _, next). - FallthroughEdge(caller, as(fallthrough, Block)), - BlockEdge(callerCtx, caller, calleeCtx, as(fallthrough, Block)) :- - sens.MergeContext(callerCtx, caller, calleeCtx), // implies reachable - Statement_Block(stmt, caller), - FallthroughStmt(stmt, fallthrough), - IsBasicBlockHead(fallthrough). + BlockValidNext(ctx, block, fallthrough):- + ReachableContext(ctx, block), + FallthroughEdge(block, fallthrough). + + // BlockEdge(callerCtx, caller, calleeCtx, fallthrough) :- + // sens.MergeContext(callerCtx, caller, calleeCtx), // implies reachable + // FallthroughEdge(caller, fallthrough). // There may be an unconditional context computed by the algorithm. Use it. BlockEdge(callerCtx, caller, calleeCtx, callee) :- - BlockJumpValidTarget(callerCtx, caller, _, callee), + // BlockJumpValidTarget(callerCtx, caller, _, callee), + BlockValidNext(callerCtx, caller, callee), sens.MergeContext(callerCtx, caller, calleeCtx). .plan 1:(2,1) // Also check if there is a conditional (on-request) context for this case - sens.MergeContextRequest(callerCtx, block, continuation) :- - BlockJumpValidTarget(callerCtx, block, _, continuation). + sens.MergeContextRequest(callerCtx, block, next) :- + BlockValidNext(callerCtx, block, next). BlockEdge(callerCtx, caller, calleeCtx, callee) :- - BlockJumpValidTarget(callerCtx, caller, _, callee), + BlockValidNext(callerCtx, caller, callee), sens.MergeContextResponse(callerCtx, caller, callee, calleeCtx). .plan 1:(2,1) @@ -256,6 +264,9 @@ PreMask_Length(cat(mask, "ff"), bytes+1) :- VariableContainsJumpTarget(var), !VariableUsedInOperation(var). + /** + Used to verify which variables/stack indexes that seem to be used as selectors, are actually selectors + */ .decl ValidSelector(selector: OptionalSelector) ValidSelector($NoSelector()). diff --git a/logic/local.dl b/logic/local.dl index 890acbf0..cbb32885 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -288,7 +288,6 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- // Covers JUMPIs and other fallthrough cases .decl FallthroughStmt(stmt: Statement, next: Statement) - FallthroughStmt(stmt, next) :- BasicBlock_Tail(_, stmt), !JUMP(stmt), @@ -296,9 +295,13 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- !OpcodePossiblyHalts(opcode), Statement_Next(stmt, next). + .decl FallthroughEdge(caller: Block, fallthroughBlock: Block) + FallthroughEdge(caller, as(fallthrough, Block)):- + Statement_Block(stmt, caller), + FallthroughStmt(stmt, fallthrough), + IsBasicBlockHead(fallthrough). - .decl ThrowJump(stmt: Statement) - + .decl ThrowJump(stmt: Statement) ThrowJump(jmp) :- ImmediateBlockJumpTarget(block, variable), Variable_Value(variable, targetValue), @@ -722,7 +725,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- BlockComparesSigVyperBase(block, sigHash, selectorVarOrIndex) :- Statement_Block(pushStmt, block), - (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), + SmallValuePush(pushStmt, sigHash), Statement_Defines(pushStmt, sigHashVar), Statement_Uses_Local(eqStmt, sigHashVar, n), Statement_Uses_Local(eqStmt, selectorVarOrIndex, 1 - n), @@ -737,7 +740,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- // New vyper pattern BlockComparesSigVyperBase(block, sigHash, selectorVarOrIndex):- Statement_Block(pushStmt, block), - (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), + SmallValuePush(pushStmt, sigHash), Statement_Defines(pushStmt, sigHashVar), Statement_Uses_Local(xorStmt, sigHashVar, n), Statement_Uses_Local(xorStmt, selectorVarOrIndex, 1 - n), @@ -759,7 +762,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- BlockComparesSigFallthroughSolidity(block, sigHash, selector) :- Statement_Block(pushStmt, block), ImmediateBlockJumpTarget(block, _), - (PUSH4(pushStmt, sigHash) ; PUSH3(pushStmt, sigHash)), + SmallValuePush(pushStmt, sigHash), Statement_Defines(pushStmt, sigHashVar), SUB(subStmt), Statement_Uses_Local(subStmt, sigHashVar, n), From 257ef8705c06b58147247cff330c1f41419aeaa2 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 14 Dec 2023 16:20:12 +0200 Subject: [PATCH 22/28] refactor remain ctx sens flavors --- logic/context-sensitivity/callsite_context.dl | 2 +- logic/context-sensitivity/selective_context.dl | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/logic/context-sensitivity/callsite_context.dl b/logic/context-sensitivity/callsite_context.dl index abe0c474..db61c297 100644 --- a/logic/context-sensitivity/callsite_context.dl +++ b/logic/context-sensitivity/callsite_context.dl @@ -20,7 +20,7 @@ ReachableContext(ctx, caller), DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), newPrivateContext = [caller, cutDownPri]. .plan 1:(2,1,3), 2:(3,2,1) } \ No newline at end of file diff --git a/logic/context-sensitivity/selective_context.dl b/logic/context-sensitivity/selective_context.dl index 425851fb..add760d1 100644 --- a/logic/context-sensitivity/selective_context.dl +++ b/logic/context-sensitivity/selective_context.dl @@ -23,20 +23,20 @@ MergeContext(ctx, caller, ctx):- ReachableContext(ctx, caller), local.BlockHasTrivialControl(caller), - !local.PublicFunction(caller, _, _). + !local.PublicFunctionJump(caller, _, _). MergeContext(ctx, caller, [pub, newPrivateContext]):- ReachableContext(ctx, caller), DecomposeContext(ctx, pub, pri), TruncateContextIfNeeded(pub, pri, cutDownPri), - !local.PublicFunction(caller, _, _), + !local.PublicFunctionJump(caller, _, _), !local.BlockHasTrivialControl(caller), newPrivateContext = [caller, cutDownPri]. .plan 1:(2,1,3), 2:(3,2,1) MergeContext(ctx, caller, newContext) :- ReachableContext(ctx, caller), - local.PublicFunction(caller, sigHash, _), + local.PublicFunctionJump(caller, sigHash, _), !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, _, callCtx), newContext = [sigHash, callCtx]. From 39dad4810db6596d79da721454481b0fca517915 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 14 Dec 2023 17:25:32 +0200 Subject: [PATCH 23/28] Add missing plan --- logic/context-sensitivity/abstract_context.dl | 1 + 1 file changed, 1 insertion(+) diff --git a/logic/context-sensitivity/abstract_context.dl b/logic/context-sensitivity/abstract_context.dl index bf9f7a08..1d34c886 100644 --- a/logic/context-sensitivity/abstract_context.dl +++ b/logic/context-sensitivity/abstract_context.dl @@ -311,6 +311,7 @@ !MaxContextDepth(sigHash, -1), DecomposeContext(ctx, FALLBACK_FUNCTION_SIGHASH, pri), newContext = [sigHash, pri]. + .plan 1:(4,1,2,3) MergeContextResponse(ctx, caller, funcStart, ctx) :- MergeContextRequest(ctx, caller, funcStart), local.PublicFunctionJump(caller, sigHash, _), From decb1d9f7883fcf96269d70ee3ea9231d1523234 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 14 Dec 2023 18:32:34 +0200 Subject: [PATCH 24/28] Add more PublicFunction and PublicFunctionJump facts in preTrans, for completeness and consistency --- logic/local.dl | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/logic/local.dl b/logic/local.dl index cbb32885..60e78a72 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -773,7 +773,11 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- JUMPI(jumpiStmt), Statement_Uses_Local(jumpiStmt, pred, 1). - PublicFunctionJump(block, sigHash, selectorVarOrIndex) :- BlockComparesSig(block, sigHash, selectorVarOrIndex). + PublicFunctionJump(block, sigHash, selectorVarOrIndex) :- + BlockComparesSig(block, sigHash, selectorVarOrIndex); + BlockComparesSigVyper(block, sigHash, selectorVarOrIndex); + BlockComparesSigFallthroughSolidity(block, sigHash, selectorVarOrIndex). + PublicFunction(as(targetValue, Block), sigHash, selectorVarOrIndex) :- BlockComparesSig(block, sigHash, selectorVarOrIndex), @@ -782,6 +786,11 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- PushValue(push, targetValue), JUMPDEST(as(targetValue, symbol)). + PublicFunction(fallthrough, sigHash, selectorVarOrIndex) :- + (BlockComparesSigVyper(block, sigHash, selectorVarOrIndex); + BlockComparesSigFallthroughSolidity(block, sigHash, selectorVarOrIndex)), + FallthroughEdge(block, fallthrough). + .decl BlockComparesCallDataSizeToFour(block: Block, jumpi: Statement, lessThanFourTarget: Block) .decl BlockJumpsOnCallDataSize(block: Block, jumpi: Statement, noCallDataBranch: Block, callDataBranch: Block) .decl BlockHasReceiveAsFallThrough(block: Block, jumpi: Statement, fallthrough: Block, target: Block) @@ -947,7 +956,7 @@ insertor.insertOps(jumpDestStmt, STMT(JUMP, cat("PublicFunctionJump:", hash)) ) ) :- - preTrans.PublicFunctionJump(block, hash, selector), + preTrans.BlockComparesSig(block, hash, selector), preTrans.PublicFunction(start, hash, selector), ValidSelector(selector), preTrans.Statement_Block(jumpDestStmt, start), @@ -1086,7 +1095,7 @@ postTrans.PublicFunctionJump(block, hash, selector) :- insertor.PublicFunctionJumpMetadata(meta, hash), postTrans.Statement_Block(stmt, block), ValidSelector(selector), - (preTrans.PublicFunctionJump(_, hash, selector); + (preTrans.BlockComparesSig(_, hash, selector); preTrans.BlockComparesSigVyper(_, hash, selector); preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); (preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = RECEIVE_FUNCTION_SIGHASH, selector = $NoSelector()) From 62c1c8a3a29b68cd5b782abc5e9577d659893a27 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Thu, 14 Dec 2023 19:07:19 +0200 Subject: [PATCH 25/28] Fix postTrans.PublicFunction --- logic/local.dl | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/logic/local.dl b/logic/local.dl index 60e78a72..c52c6dd0 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -1130,7 +1130,10 @@ postTrans.PublicFunction(block, hash, $NoSelector()) :- postTrans.JUMPDEST(stmt), postTrans.Statement_Block(stmt, block). -postTrans.PublicFunction(b, h, s) :- preTrans.PublicFunction(b, h, s), ValidSelector(s). +postTrans.PublicFunction(block , hash, selector):- + preTrans.BlockComparesSig(_, hash, selector), + preTrans.PublicFunction(block, hash, selector), + ValidSelector(selector). .output postTrans.PublicFunction, preTrans.PublicFunction, preTrans.BlockComparesSigFallthroughSolidity, preTrans.BlockComparesSigVyper, insertor.MetaData .output postTrans.PublicFunctionJump From 352d78e18040812b8e533e7cae752e5cb3d29b96 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Fri, 15 Dec 2023 12:01:49 +0200 Subject: [PATCH 26/28] fix fallback as well --- logic/local.dl | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/logic/local.dl b/logic/local.dl index c52c6dd0..bf92c626 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -794,6 +794,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- .decl BlockComparesCallDataSizeToFour(block: Block, jumpi: Statement, lessThanFourTarget: Block) .decl BlockJumpsOnCallDataSize(block: Block, jumpi: Statement, noCallDataBranch: Block, callDataBranch: Block) .decl BlockHasReceiveAsFallThrough(block: Block, jumpi: Statement, fallthrough: Block, target: Block) + .decl FallBackFunctionInfo(caller: Block, startBlock: Block, sigHash: Value, selector: OptionalSelector) BlockComparesCallDataSizeToFour(block, stmt5, as(target, Block)):- PushValue(stmt, "0x4"), @@ -846,12 +847,15 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- JUMPDEST(as(noCallDataSizeBranch, Statement)). // Fallback functions - PublicFunctionJump(block, FALLBACK_FUNCTION_SIGHASH, $NoSelector()), - PublicFunction(fallbackStart, FALLBACK_FUNCTION_SIGHASH, $NoSelector()):- + FallBackFunctionInfo(block, fallbackStart, FALLBACK_FUNCTION_SIGHASH, $NoSelector()):- BlockComparesCallDataSizeToFour(block, _, fallbackStart), 1 = count : BlockComparesCallDataSizeToFour(_, _, _), !BlockJumpsOnCallDataSize(fallbackStart, _, _, _). + PublicFunctionJump(block, sigHash, selector), + PublicFunction(fallbackStart, sigHash, selector):- + FallBackFunctionInfo(block, fallbackStart, sigHash, selector). + BlockHasReceiveAsFallThrough(block, jumpi, noCallDataSizeBranch, callDataSizeBranch):- BlockComparesCallDataSizeToFour(_, _, block), BlockJumpsOnCallDataSize(block, jumpi, noCallDataSizeBranch, callDataSizeBranch). @@ -956,7 +960,8 @@ insertor.insertOps(jumpDestStmt, STMT(JUMP, cat("PublicFunctionJump:", hash)) ) ) :- - preTrans.BlockComparesSig(block, hash, selector), + (preTrans.BlockComparesSig(block, hash, selector); + preTrans.FallBackFunctionInfo(block, start, hash, selector)), preTrans.PublicFunction(start, hash, selector), ValidSelector(selector), preTrans.Statement_Block(jumpDestStmt, start), @@ -1096,6 +1101,7 @@ postTrans.PublicFunctionJump(block, hash, selector) :- postTrans.Statement_Block(stmt, block), ValidSelector(selector), (preTrans.BlockComparesSig(_, hash, selector); + preTrans.FallBackFunctionInfo(_, _, hash, selector); preTrans.BlockComparesSigVyper(_, hash, selector); preTrans.BlockComparesSigFallthroughSolidity(_, hash, selector); (preTrans.BlockHasReceiveAsFallThrough(_, _, _, _), hash = RECEIVE_FUNCTION_SIGHASH, selector = $NoSelector()) @@ -1131,7 +1137,8 @@ postTrans.PublicFunction(block, hash, $NoSelector()) :- postTrans.Statement_Block(stmt, block). postTrans.PublicFunction(block , hash, selector):- - preTrans.BlockComparesSig(_, hash, selector), + (preTrans.BlockComparesSig(_, hash, selector); + preTrans.FallBackFunctionInfo(_, _, hash, selector)), preTrans.PublicFunction(block, hash, selector), ValidSelector(selector). From 8d646793874dfa7a70ca6b748af1b110dcff4fb0 Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Fri, 15 Dec 2023 17:03:13 +0200 Subject: [PATCH 27/28] Create PreTransLocalAnalysisAlt to use when we don't filter public functions --- logic/local.dl | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/logic/local.dl b/logic/local.dl index bf92c626..52111ba7 100644 --- a/logic/local.dl +++ b/logic/local.dl @@ -693,7 +693,7 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- BlockComparesSigVyper(_, _, selectorVarOrIndex). // All pushes of values up to 4 bytes, can be used as selectors - .decl SmallValuePush(pushStmt: Statement, value: Value) + .decl SmallValuePush(pushStmt: Statement, value: Value) overridable SmallValuePush(pushStmt, value):- PUSH4(pushStmt, value); PUSH3(pushStmt, value); @@ -862,6 +862,17 @@ ByteCodeHex(substr(bytecode, 2, strlen(bytecode))):- } +/** + Same as PreTransLocalAnalysis but less complete public function identification. + Used when we don't verify/filter public functions based via the `OptionalSelector` mechanism +*/ +.comp PreTransLocalAnalysisAlt: PreTransLocalAnalysis{ + .override SmallValuePush + SmallValuePush(pushStmt, value):- + PUSH4(pushStmt, value); + PUSH3(pushStmt, value). +} + .comp PostTransLocalAnalysis : LocalAnalysis { } @@ -907,7 +918,6 @@ PreTransStatement_OriginalStatement(ogStmt, ogStmt) :- PreTransStatement_OriginalStatement(rvtClStmt, ogStmt) :- revertCloner.StatementToClonedStatement(_, _, ogStmt, rvtClStmt). -.init preTrans = PreTransLocalAnalysis .init revertCloner = RevertBlockCloner COPY_CODE(revertCloner, factReader) @@ -919,6 +929,8 @@ COPY_CODE(revertCloner, factReader) .init blockCloner = BLOCK_CLONING COPY_OUTPUT(blockCloner, revertCloner) blockCloner.Prev_Block_OriginalBlock(block, originalBlock):- revertCloner.Block_OriginalBlock(block, originalBlock). + +.init preTrans = PreTransLocalAnalysis COPY_OUTPUT(preTrans, blockCloner) PreTransStatement_OriginalStatement(heurClStmt, ogStmt) :- @@ -934,6 +946,7 @@ ValidSelector(optionalSelector):- #else +.init preTrans = PreTransLocalAnalysisAlt COPY_OUTPUT(preTrans, revertCloner) ValidSelector(optionalSelector):- From fd4524980474aeb83947a85e316759b4fc3a1dba Mon Sep 17 00:00:00 2001 From: Sifis Lagouvardos Date: Fri, 15 Dec 2023 17:03:33 +0200 Subject: [PATCH 28/28] Fix broken test --- tests/context-sensitivity/finite-precise.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/context-sensitivity/finite-precise.json b/tests/context-sensitivity/finite-precise.json index b342129b..a40303e2 100644 --- a/tests/context-sensitivity/finite-precise.json +++ b/tests/context-sensitivity/finite-precise.json @@ -1,6 +1,6 @@ { "client_path": null, "gigahorse_args": ["-i", "--disable_scalable_fallback", "--disable_precise_fallback", "--disable_inline", "-M", "CONTEXT_SENSITIVITY=FinitePreciseContext"], - "expected_analytics": [["Analytics_JumpToMany", 0, 0], ["Analytics_UnreachableBlock", 5, 0], + "expected_analytics": [["Analytics_JumpToMany", 0, 0], ["Analytics_UnreachableBlock", 4, 0], ["Analytics_BlockHasNoTACBlock", 0, 0]] }