Merge pull request #136 from nevillegrech/global_completeness

Increase completeness of global analysis by modeling of constant operations relying on the global analysis

logic/global_components.dl

@@ -4,7 +4,7 @@
 #include "context-sensitivity/context_sensitivity.dl"
 
 #define LIMITSIZE_BLOCK_OUTPUT_CONTENTS 1000000
-#define LIMITSIZE_BIG_BLOCK_OUTPUT_CONTENTS 5000000
+#define LIMITSIZE_BIG_BLOCK_OUTPUT_CONTENTS 2000000
 
 .comp GlobalAnalysis <AbstractContextSensitivity, LocalAnalysis> : LocalAnalysis {
   /*
@@ -55,6 +55,72 @@
   */
   .decl BlockEdge(callerCtx: sens.Context, caller: Block, calleeCtx: sens.Context, callee: Block)
 
+  /**
+    Variable or stack index `variable` has `value` under `ctx`.
+  */
+  .decl GlobalVariable_Value(ctx: sens.Context, variable: VariableOrStackIndex, value: Value)
+  DEBUG_OUTPUT(GlobalVariable_Value)
+
+  /**
+    Global-level value flow and creation of new constant values via an instantiation of the `ConstantFolding` component
+    is limited by the fact that new values are not propagated to following contexts/blocks.
+    This would not model a case where a block reads a value from a previous block and produces a jumpdest,
+    pushing it to the stack for a following block to read/jump to.
+    Haven't seen such patterns in practice so I'm keeping it like that.
+  */
+  .init globalVariableValueConstantOps = ConstantFolding
+
+  GlobalVariable_Value(ctx, variable, value):-
+    ReachableContext(ctx, block),
+    Statement_Block(statement, block),
+    Statement_Defines(statement, variable),
+    Variable_Value(variable, value).
+
+  // global case, highlights limitation
+  GlobalVariable_Value(ctx, stackIndex, value):-
+    BlockInputContents(ctx, block, stackIndex, variable),
+    Statement_Block(statement, block),
+    Statement_Uses_Local(statement, stackIndex, _),
+    CheckIsStackIndex(stackIndex),
+    Variable_Value(variable, value).
+
+
+  /**
+    The set of variables for which we need to recover their values via global-level analysis.
+  */
+  .decl VariableWithoutValueUsedInJumpTargetComputation(variable: Variable)
+
+  VariableWithoutValueUsedInJumpTargetComputation(var):-
+    ImmediateBlockJumpTarget(_, var),
+    !Variable_Value(var, _).
+
+  VariableWithoutValueUsedInJumpTargetComputation(as(use, Variable)):-
+    VariableWithoutValueUsedInJumpTargetComputation(def),
+    Statement_Defines(stmt, def),
+    Statement_Uses_Local(stmt, use, _),
+    CheckIsVariable(use),
+    !Variable_Value(use, _).
+
+  // Helper to produce all constant operation requests
+  .decl GlobalBinopStatementOpAndConstantArgValues(ctx: sens.Context, stmt: Statement, op: Opcode, a_val: Value, b_val: Value)
+  GlobalBinopStatementOpAndConstantArgValues(ctx, stmt, op, aval, bval) :-
+    VariableWithoutValueUsedInJumpTargetComputation(targetVar),
+    Statement_Defines(stmt, targetVar),
+    Statement_Opcode(stmt, op),
+    Statement_Uses_Local(stmt, a, 0),
+    Statement_Uses_Local(stmt, b, 1),
+    GlobalVariable_Value(ctx, a, aval),
+    GlobalVariable_Value(ctx, b, bval).
+   .plan 0:(6,4,5,7,3,2,1),1:(7,5,4,6,3,2,1)
+
+  globalVariableValueConstantOps.RequestConstantFold2(op, a_val, b_val) :-
+    GlobalBinopStatementOpAndConstantArgValues(_, _, op, a_val, b_val).
+
+  GlobalVariable_Value(ctx, to, result) :-
+    globalVariableValueConstantOps.ConstantFoldResult2(op, a_val, b_val, result),
+    GlobalBinopStatementOpAndConstantArgValues(ctx, stmt, op, a_val, b_val),
+    Statement_Defines(stmt, to).
+    .plan 1:(2,1,3)
 
   /*
   ***********
@@ -108,6 +174,12 @@
     Variable_Value(targetVar, targetValue),
     JUMPDEST(as(targetValue, symbol)).
 
+  BlockJumpValidTarget(ctx, block, targetVar, as(targetValue, Block)) :-
+    BlockJumpTarget(ctx, block, targetVar),
+    GlobalVariable_Value(ctx, targetVar, targetValue),
+    JUMPDEST(as(targetValue, symbol)).
+   .plan 1:(2,1,3)
+
 
   /*
   ***********
@@ -148,6 +220,7 @@
     sens.MergeContextResponse(callerCtx, caller, callee, calleeCtx).
     .plan 1:(2,1)
 
+  // Note: It's under __any__ ctx. To be used with caution.
   .decl Statement_Uses(stmt: Statement, var: Variable, n: StackIndex)
 
   // Case: variable originates locally

logic/local_components.dl

@@ -242,10 +242,12 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
 
   .decl BeforeLocalStackContents(stmt: Statement, n: StackIndex, variable: VariableOrStackIndex)
 
-  /**  
+  /**
     The target of a jump at the end of the `block` is a `variable` defined in
     the `block` itself. "Immediate" is misnomer, can't think of better name.
-    This is a context-independent predicate.
+    This is a context-independent predicate.  
+    __Note__: A `variable` in the output of this relation doesn't need to have a value,
+    it can be the result of the constant folding of a variable coming from a previous block.
   */
   .decl ImmediateBlockJumpTarget(block: Block, variable: Variable)
 
@@ -526,14 +528,8 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
     Helper for some ctx sensitivity algorithms
   */
   .decl BlockHasTrivialControl(block: Block)
-
-  BlockHasTrivialControl(block):-
-    BasicBlock_Tail(block, stmt),
-    !JUMP(stmt),
-    !JUMPI(stmt).
-
   BlockHasTrivialControl(block):-
-    ImmediateBlockJumpTarget(block, _).
+    StaticBlockJumpTarget(block, _).
 
   // inverse-escape analysis: helpers for ctx sensitivity
   .decl BlockUsesLocal(block: Block, var: VariableOrStackIndex)
@@ -624,7 +620,8 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
   PrivateFunctionReturn(returnBlock) :-
     Statement_Block(stmt, returnBlock),
     (JUMP(stmt); JUMPI(stmt)), // temp: handle conditional returns
-    !ImmediateBlockJumpTarget(returnBlock, _).
+    !StaticBlockJumpTarget(returnBlock, _).
+    // !ImmediateBlockJumpTarget(returnBlock, _).
 
   .decl PrivateFunctionCallOrReturn(block: Block)
   PrivateFunctionCallOrReturn(block) :-
@@ -766,7 +763,7 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
   // Compares label from stack to a constant: common public function dispatch pattern
   BlockComparesSig(block, sigHash, selector) :-
     Statement_Block(pushStmt, block),
-    ImmediateBlockJumpTarget(block, _),
+    StaticBlockJumpTarget(block, _),
     SmallValuePush(pushStmt, sigHash),
     Statement_Defines(pushStmt, sigHashVar),
     EQ(eqStmt),
@@ -821,7 +818,7 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
   .decl BlockComparesSigFallthroughSolidity(block: Block, sigHash: Value, selectorVarOrIndex: OptionalSelector)
   BlockComparesSigFallthroughSolidity(block, sigHash, selector) :-
     Statement_Block(pushStmt, block),
-    ImmediateBlockJumpTarget(block, _),
+    StaticBlockJumpTarget(block, _),
     SmallValuePush(pushStmt, sigHash),
     Statement_Defines(pushStmt, sigHashVar),
     SUB(subStmt),
@@ -842,9 +839,8 @@ IsStackIndexLessThan(n, maximum) :- n = range(0, maximum, 1).
   PublicFunction(as(targetValue, Block), sigHash, selectorVarOrIndex) :-
     BlockComparesSig(block, sigHash, selectorVarOrIndex),
     ImmediateBlockJumpTarget(block, var),
-    Statement_Defines(push, var),
-    PushValue(push, targetValue),
-    JUMPDEST(as(targetValue, symbol)).
+    Variable_Value(var, targetValue),
+    JUMPDEST(as(targetValue, Statement)).
 
   PublicFunction(fallthrough, sigHash, selectorVarOrIndex) :-
     (BlockComparesSigVyper(block, sigHash, selectorVarOrIndex);

logic/types_defs.dl

@@ -5,6 +5,11 @@
 #include "../clientlib/util.dl"
 
 #ifndef MAX_STACK_HEIGHT
+/**
+  This parameter is tuned, increasing it (for example to 80) will give a minor completeness increase in extreme cases.
+  However it can negatively affect scalability so I'm keeping it at 70 for now.
+  To review.
+*/
 #define MAX_STACK_HEIGHT 70
 #endif
 

tests/core-decompiler/49ceac2769b83ac04f76bb527e62ed01.json

@@ -0,0 +1,6 @@
+{
+    "client_path": null,
+    "gigahorse_args": ["-i", "--disable_inline"],
+    "expected_analytics": [["Analytics_JumpToMany", 0, 0], ["Analytics_UnreachableBlock", 0, 0], ["Analytics_BlockHasNoTACBlock", 0, 0],
+                           ["Analytics_MissingJumpTargetSomeCtx", 0, 0], ["Analytics_MissingJumpTargetAnyCtx", 0, 0]]
+}

tooling/compare-runs.py

@@ -39,7 +39,7 @@
   'Analytics_PrivateFunctionMatchesMetadata': 'completeness',
   'Analytics_PrivateFunctionMatchesMetadataIncorrectArgs': 'imprecision',
   'Analytics_PrivateFunctionMatchesMetadataIncorrectReturnArgs': 'imprecision',
-#  'Analytics_MissingJumpTargetAnyCtx',
+  'Analytics_MissingJumpTargetAnyCtx' : 'incompleteness',
 #  'Analytics_JumpToManyWithoutGlobalImprecision',
 #  'Analytics_Blocks',
   'Analytics_Contexts' : 'scalability',
@@ -64,7 +64,8 @@
 }
 
 clients_analytics = {
-  'client_time' : 'scalability'
+  'client_time' : 'scalability',
+  'inline_time': 'scalability'
 }
 
 list_of_verbatim_rels = {