fix improper stacktrace handling in the context of optimising pre mod…

…ules
NethermindEth · Mar 1, 2023 · 156a312 · 156a312
1 parent 4982f80
commit 156a312
Show file tree

Hide file tree

Showing 16 changed files with 49 additions and 44 deletions.
diff --git a/src/Horus/CairoSemantics.hs b/src/Horus/CairoSemantics.hs
@@ -23,7 +23,7 @@ import Data.Maybe (fromMaybe, isJust)
 import Data.Set qualified as Set (Set, member)
 import Data.Text (Text)
 import Data.Traversable (for)
-import Lens.Micro ((^.), _3)
+import Lens.Micro ((^.), _1)
 
 import Horus.CallStack as CS (CallEntry, CallStack)
 import Horus.Expr (Cast (..), Expr (ExistsFelt, (:+)), Ty (..), (.&&), (./=), (.<), (.<=), (.==), (.=>), (.||))
@@ -382,7 +382,7 @@ withExecutionCtx ctx action = do
 mkInstructionConstraints ::
   LabeledInst ->
   Label ->
-  Maybe (CallStack, Label, ScopedFunction) ->
+  Maybe (CallStack, ScopedFunction) ->
   Map (NonEmpty Label, Label) Bool ->
   CairoSemanticsL (Maybe (Expr TFelt))
 mkInstructionConstraints lInst@(pc, Instruction{..}) nextPc optimisingF jnzOracle = do
@@ -403,7 +403,7 @@ mkCallConstraints ::
   Label ->
   Label ->
   Expr TFelt ->
-  Maybe (CallStack, Label, ScopedFunction) ->
+  Maybe (CallStack, ScopedFunction) ->
   ScopedFunction ->
   CairoSemanticsL (Maybe (Expr TFelt))
 mkCallConstraints pc nextPc fp optimisingF f = do
@@ -417,7 +417,12 @@ mkCallConstraints pc nextPc fp optimisingF f = do
   -- Considering we have already pushed the stackFrame by now, we need to make sure that either
   -- the function is inlinable and we'll encounter a 'ret', or we need to pop right away
   -- once we encode semantics of the function.
-  if Just f == ((^. _3) <$> optimisingF)
+
+  -- Determine whether the current function matches the function being optimised exactly -
+  -- this necessitates comparing execution traces.
+  executionContext <- getStackTraceDescr
+  optimisedFExecutionContext <- getStackTraceDescr' ((^. _1) <$> optimisingF)
+  if isJust optimisingF && executionContext == optimisedFExecutionContext
     then Just <$> getFp <* pop
     else do
       -- This is reachable unless the module is optimizing, in which case the precondition
@@ -475,7 +480,7 @@ mkApConstraints apEnd insts = do
  where
   lastLInst@(lastPc, lastInst) = NonEmpty.last insts
 
-mkBuiltinConstraints :: Expr TFelt -> NonEmpty LabeledInst -> Maybe (CallStack, Label, ScopedFunction) -> CairoSemanticsL ()
+mkBuiltinConstraints :: Expr TFelt -> NonEmpty LabeledInst -> Maybe (CallStack, ScopedFunction) -> CairoSemanticsL ()
 mkBuiltinConstraints apEnd insts optimisesF =
   unless (isJust optimisesF) $ do
     fp <- getFp

diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs
@@ -25,7 +25,7 @@ import Data.Text qualified as Text (isPrefixOf)
 import Data.Traversable (for)
 import System.FilePath.Posix ((</>))
 
-import Horus.CFGBuild (CFGBuildL, Label, LabeledInst, buildCFG)
+import Horus.CFGBuild (CFGBuildL, LabeledInst, buildCFG)
 import Horus.CFGBuild.Runner (CFG (..))
 import Horus.CairoSemantics (CairoSemanticsL, encodeModule)
 import Horus.CairoSemantics.Runner
@@ -166,7 +166,7 @@ data SolvingInfo = SolvingInfo
   , si_funcName :: Text
   , si_result :: HorusResult
   , si_inlinable :: Bool
-  , si_optimisesF :: Maybe (CallStack, Label, ScopedFunction)
+  , si_optimisesF :: Maybe (CallStack, ScopedFunction)
   }
   deriving (Eq, Show)
 

diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs
@@ -27,7 +27,7 @@ import Data.Text qualified as Text (concat, intercalate)
 import Lens.Micro (ix, (^.))
 import Text.Printf (printf)
 
-import Horus.CFGBuild (ArcCondition (..), Label (Label, unLabel), Vertex (v_label, v_optimisesF))
+import Horus.CFGBuild (ArcCondition (..), Label (unLabel), Vertex (v_label, v_optimisesF))
 import Horus.CFGBuild.Runner (CFG (..), verticesLabelledBy)
 import Horus.CallStack (CallStack, callerPcOfCallEntry, digestOfCallStack, initialWithFunc, pop, push, stackTrace, top)
 import Horus.ContractInfo (pcToFun)
@@ -36,21 +36,20 @@ import Horus.Expr qualified as Expr (and)
 import Horus.Expr.SMT (pprExpr)
 import Horus.Expr.Vars (ap, fp)
 import Horus.FunctionAnalysis (FInfo, FuncOp (ArcCall, ArcRet), ScopedFunction (sf_scopedName), isRetArc, sizeOfCall)
-import Horus.Instruction (LabeledInst)
+import Horus.Instruction (LabeledInst, uncheckedCallDestination)
 import Horus.Label (moveLabel)
 import Horus.Program (Identifiers)
 import Horus.SW.FuncSpec (FuncSpec (..))
 import Horus.SW.Identifier (Function (..), getFunctionPc, getLabelPc)
 import Horus.SW.ScopedName (ScopedName (..), toText)
-import Horus.Util (tShow)
 
 data Module = Module
   { m_spec :: ModuleSpec
   , m_prog :: [LabeledInst]
   , m_jnzOracle :: Map (NonEmpty Label, Label) Bool
   , m_calledF :: Label
   , m_lastPc :: (CallStack, Label)
-  , m_optimisesF :: Maybe (CallStack, Label, ScopedFunction)
+  , m_optimisesF :: Maybe (CallStack, ScopedFunction)
   }
   deriving stock (Show)
 
@@ -206,10 +205,10 @@ getModuleNameParts idents (Module spec prog oracle calledF _ optimisesF) =
   post = case spec of MSRich fs -> fs_post fs; MSPlain ps -> ps_post ps
   optimisingSuffix = case optimisesF of
     Nothing -> ""
-    Just (callstack, Label l, f) ->
+    Just (callstack, f) ->
       let fName = toText . ScopedName . dropMain . sn_path . sf_scopedName $ f
           stack = digestOfCallStack (Map.map sf_scopedName (pcToFun idents)) callstack
-       in " Pre<" <> fName <> "|" <> stack <> "@" <> tShow l <> ">"
+       in " Pre<" <> fName <> "|" <> stack <> ">"
 
 data Error
   = ELoopNoInvariant Label
@@ -311,18 +310,19 @@ gatherFromSource cfg function fSpec = do
     assertions = map snd (cfg_assertions cfg ^. ix v)
     onFinalNode = null (cfg_arcs cfg ^. ix v)
     emitPlain pre post = emit . MSPlain $ PlainSpec pre post
-    emitRich pre post = emit . MSRich $ FuncSpec pre post $ fs_storage fSpec
+    emitRich pre post = emit . MSRich . FuncSpec pre post $ fs_storage fSpec
 
     emit spec =
       emitModule
-        ( Module
-            spec
-            acc
-            oracle'
-            (fu_pc function)
-            (callstack', l)
-            ((callstack',l,) <$> v_optimisesF v)
+        ( Module spec acc oracle' (fu_pc function) (callstack', l) executionContextOfOptimisedF
         )
+     where
+      optimisingStackFrame = (fCallerPc, fCalledF)
+       where
+        laballedCall@(fCallerPc, _) = last acc
+        fCalledF = uncheckedCallDestination laballedCall
+      executionContextOfOptimisedF =
+        (push optimisingStackFrame callstack',) <$> v_optimisesF v
 
     visitArcs newOracle acc' pre v' = do
       let outArcs = cfg_arcs cfg ^. ix v'

diff --git a/tests/resources/golden/get_block_timestamp.gold b/tests/resources/golden/get_block_timestamp.gold
@@ -1,5 +1,5 @@
 
-test_invalid_1 Pre<starkware.starknet.common.syscalls.get_block_timestamp|<root>@14>
+test_invalid_1 Pre<starkware.starknet.common.syscalls.get_block_timestamp|<12=get_block_timestamp/root>>
 Verified
 
 test_invalid_1:::default

diff --git a/tests/resources/golden/get_caller_address.gold b/tests/resources/golden/get_caller_address.gold
@@ -1,5 +1,5 @@
 
-test_invalid_1 Pre<starkware.starknet.common.syscalls.get_caller_address|<root>@14>
+test_invalid_1 Pre<starkware.starknet.common.syscalls.get_caller_address|<12=get_caller_address/root>>
 Verified
 
 test_invalid_1:::default

diff --git a/tests/resources/golden/get_contract_address.gold b/tests/resources/golden/get_contract_address.gold
@@ -1,5 +1,5 @@
 
-test_invalid_1 Pre<starkware.starknet.common.syscalls.get_contract_address|<root>@14>
+test_invalid_1 Pre<starkware.starknet.common.syscalls.get_contract_address|<12=get_contract_address/root>>
 Verified
 
 test_invalid_1:::default

diff --git a/tests/resources/golden/inline_small.gold b/tests/resources/golden/inline_small.gold
@@ -1,5 +1,5 @@
 
-main Pre<pred|<14=id/root>@11>
+main Pre<pred|<9=pred/14=id/root>>
 Verified
 
 main:::default

diff --git a/tests/resources/golden/inline_stack_minimal_sat.gold b/tests/resources/golden/inline_stack_minimal_sat.gold
@@ -1,11 +1,11 @@
 
-main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<33=lit/root>@24>
+main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<22=get_ap/33=lit/root>>
 Verified
 
-main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<37=lit/root>@24>
+main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<22=get_ap/37=lit/root>>
 Verified
 
-main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<39=add/root>@17>
+main_ Pre<starkware.cairo.lang.compiler.lib.registers.get_ap|<15=get_ap/39=add/root>>
 Verified
 
 main_:::default

diff --git a/tests/resources/golden/invalidate_sat.gold b/tests/resources/golden/invalidate_sat.gold
@@ -2,7 +2,7 @@
 id
 Verified
 
-test1 Pre<id|<root>@5>
+test1 Pre<id|<3=id/root>>
 Verified
 
 test1:::default

diff --git a/tests/resources/golden/lvar_capture.gold b/tests/resources/golden/lvar_capture.gold
@@ -2,7 +2,7 @@
 f0
 Verified
 
-f1 Pre<inc|<root>@11>
+f1 Pre<inc|<9=inc/root>>
 Verified
 
 f1:::default

diff --git a/tests/resources/golden/range_check_fake.gold b/tests/resources/golden/range_check_fake.gold
@@ -1,5 +1,5 @@
 
-max Pre<starkware.cairo.common.math_cmp.is_le|<root>@89>
+max Pre<starkware.cairo.common.math_cmp.is_le|<87=is_le/root>>
 Verified
 
 max:::1

diff --git a/tests/resources/golden/range_check_simple_fake.gold b/tests/resources/golden/range_check_simple_fake.gold
@@ -2,7 +2,7 @@
 apply_range_check
 Verified
 
-main Pre<apply_range_check|<root>@10>
+main Pre<apply_range_check|<8=apply_range_check/root>>
 Verified
 
 main:::default

diff --git a/tests/resources/golden/range_check_simple_fake_no_builtin.gold b/tests/resources/golden/range_check_simple_fake_no_builtin.gold
@@ -2,7 +2,7 @@
 apply_range_check
 Verified
 
-main Pre<apply_range_check|<root>@9>
+main Pre<apply_range_check|<7=apply_range_check/root>>
 Verified
 
 main:::default

diff --git a/tests/resources/golden/sat_cause_42.gold b/tests/resources/golden/sat_cause_42.gold
@@ -8,7 +8,7 @@ Verified
 main.loop:::1
 Verified
 
-main.loop:::2 Pre<f|<root>@23>
+main.loop:::2 Pre<f|<21=f/root>>
 Verified
 
 main.loop:::2

diff --git a/tests/resources/golden/storage_pre.gold b/tests/resources/golden/storage_pre.gold
@@ -2,26 +2,26 @@
 inc
 Verified
 
-main Pre<inc|<root>@75>
+main Pre<inc|<73=inc/root>>
 Verified
 
-main Pre<tt|<root>@77>
+main Pre<tt|<75=tt/root>>
 False
 
-main Pre<inc|<root>@84>
+main Pre<inc|<82=inc/root>>
 Verified
 
-main Pre<tt|<root>@86>
-False
+main Pre<tt|<84=tt/root>>
+Verified
 
-main Pre<inc|<root>@93>
+main Pre<inc|<91=inc/root>>
 Verified
 
-main Pre<tt|<root>@95>
+main Pre<tt|<93=tt/root>>
 Verified
 
-main Pre<tt|<root>@104>
-False
+main Pre<tt|<102=tt/root>>
+Verified
 
 main:::default
 Verified

diff --git a/tests/resources/golden/violated_call_pre.gold b/tests/resources/golden/violated_call_pre.gold
@@ -2,7 +2,7 @@
 transfer
 Verified
 
-main Pre<transfer|<root>@8> [inlined]
+main Pre<transfer|<6=transfer/root>> [inlined]
 False
 
 main:::default [inlined]