Merge pull request #120 from nevillegrech/unsoundness_global_experiment

Introduce `incompleteGlobal` analysis round, other changes
nevillegrech · Dec 18, 2023 · 5338247 · 5338247
2 parents 02c8f5b + fd45249
commit 5338247
Show file tree

Hide file tree

Showing 16 changed files with 491 additions and 211 deletions.
diff --git 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(_).
 }
@@ -280,21 +280,44 @@
   */
 
   #ifndef NO_PUBLIC_CONTEXT
-  MergeContext(ctx, caller, ctx) :-
-    ReachableContext(ctx, caller),
-    local.PublicFunction(caller, sigHash),
+  // 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),
-    local.PublicFunction(caller, sigHash),
+  .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)
+  .plan 1:(4,1,2,3)
+  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/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)
 }
diff --git 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
@@ -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
@@ -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
@@ -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].

diff --git 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/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)