Cleanup and improvements regarding sparse bit

felixwiemuth · felixwiemuth · commit dbd687d06f55 · 2024-08-14T18:39:30.000+02:00
- Remove remainders from an earlier refactoring (local variable `_isDataBoundByPC` is not used)
  - The check for this variable in UserRuntimeZero was thus always false
  - However, calls to join (label groups) are already put under a conditional checking the sparse bit in the Stack2JS phase
  - Also `wrap_block_rhs` seems to already only occour under such a conditional generated by Stack2JS, so that the blocking label is only updated when the sparse bit is not set. The function wrap_block_rhs thus becomes redundant, as it only returns its argument.
- Make code less redundant
- Use consistent naming: use "sparse bit" in all places, instead of "bound slot" etc.
diff --git a/compiler/src/Stack2JS.hs b/compiler/src/Stack2JS.hs
@@ -92,9 +92,9 @@ addLibs xs = vcat (map addOneLib xs)
 
 data TheState = TheState { freshCounter :: Integer
                          , frameSize    :: Int
-                         , boundSlot    :: Int
-                         , consts       :: Raw.Consts 
-                         , stHFN        :: IR.HFN } 
+                         , sparseSlot    :: Int
+                         , consts       :: Raw.Consts
+                         , stHFN        :: IR.HFN }
 
 type RetKontText = PP.Doc
 
@@ -103,7 +103,7 @@ type W = RWS Bool  ([LibAccess], [Basics.AtomName], [RetKontText]) TheState
 
 initState = TheState { freshCounter = 0
                      , frameSize = error "frameSize should not be accessed yet"
-                     , boundSlot = error "boundSlot should not be accessed yet"
+                     , sparseSlot = error "sparseSlot should not be accessed yet"
                      , consts = error "consts should not be accessed yet"
                      , stHFN = error "stHFN should not be accessed yet"
                      }
@@ -207,22 +207,21 @@ constsToJS consts =
 instance ToJS FunDef where 
     toJS fdef@(FunDef hfn stacksize consts bb irfdef) = do
        {--
-          |  |  | ... | <bound_slot> | 
+          |  |  | ... | <sparse slot> | 
           ^           ^
           |           |
           SP          stacksize 
        
        --}       
        let _frameSize = stacksize + 1 
 
-       modify (\s -> s { frameSize = _frameSize, boundSlot = stacksize, stHFN = hfn, consts = consts } ) -- + 1 for the _data_bound_by_pc flag; 2021-03-17; AA
-       let lits = constsToJS consts 
+       modify (\s -> s { frameSize = _frameSize, sparseSlot = stacksize, stHFN = hfn, consts = consts } ) -- + 1 for the sparse flag; 2021-03-17; AA
+       let lits = constsToJS consts
        jj <- toJS bb
        debug <- ask
-       let (irdeps, libdeps, atomdeps ) = IR.ppDeps irfdef           
-           b_slot_index = text "_SP + " PP.<> (PP.int stacksize)
-           data_bound_by_pc_slot = text "_STACK[ " PP.<> b_slot_index PP.<> "]"
-            
+       let (irdeps, libdeps, atomdeps ) = IR.ppDeps irfdef
+       sparseSlotIdxPP <- ppSparseSlotIdx
+
        return $
           vcat [text "this." PP.<>  ppId hfn <+> text "=" <+> ppArgs ["$env"] <+> text "=> {"
                , if debug then nest 2 $ text "rt.debug" <+> (PP.parens . PP.quotes.  ppId) hfn
@@ -232,8 +231,11 @@ instance ToJS FunDef where
                   "let _STACK = _T.callStack",
                   "let _SP = _T._sp",
                   "let _SP_OLD",
-                  data_bound_by_pc_slot <+> " = _T.checkDataBoundsEntry($env.__dataLevel)",
-                  "_T.boundSlot = " <+> b_slot_index,
+                  -- Update sparse bit at function entry:
+                  -- Check whether environment's data level, and the label and data level of R0 are bound by PC.
+                  -- Requires sparseSlot to be updated first.
+                  "_T.sparseSlot = " <+> sparseSlotIdxPP,
+                  "_T.updateSparseBitOnEntry($env.__dataLevel)",
                   lits,
                   jj]
                , text "}"
@@ -285,7 +287,7 @@ binOpToJS = \case
     Neq -> "rt.neq"
     Concat -> "+"
     HasField -> "rt.hasField"
-    LatticeJoin -> "rt.join"
+    LatticeJoin -> "rt.raw_join"
     -- No RT operations (should be moved to a different datatype)
     RaisedTo -> error "Not a runtime operation"
     -- Not yet implemented in IR2Raw
@@ -350,25 +352,22 @@ ir2js (MkFunClosures envBindings funBindings) = do
        where ppEnvIds env ls =
                 vcat (
                       (map (\(a,b) -> semi $ (ppId env) PP.<> text "." PP.<> (ppId a) <+> text "=" <+> ppId b ) ls)
-                      ++ 
-                      [ppId env PP.<> text ".__dataLevel = " <+> (jsFunCall "rt.join" (map (\(_, b) -> ppId b <> text ".dataLevel") ls )) ]
+                      ++
+                      [ppId env PP.<> text ".__dataLevel = " <+> jsFunCall (text $ binOpToJS Basics.LatticeJoin) (map (\(_, b) -> ppId b <> text ".dataLevel") ls ) ]
                 )
              hsepc ls = semi $ PP.hsep (PP.punctuate (text ",") ls)
 
 
-ir2js (SetState c x) = 
-  let rhs = case c of MonBlock -> ppFunCall "rt.wrap_block_rhs" [ppId x]
-                      _     -> ppId x 
-
-  in return $ semi $ monStateToJs c <+> "=" <+> rhs 
+ir2js (SetState c x) = return $ semi $ monStateToJs c <+> "=" <+> ppId x
 
 ir2js (RTAssertion a) = return $ ppRTAssertionCode jsFunCall a
 
-ir2js (LabelGroup ii) = do 
-  ii' <- mapM ppLevelOp ii 
-  b_slot <- data_bounded_by_pc_slot
+ir2js (LabelGroup ii) = do
+  ii' <- mapM ppLevelOp ii
+  sparseSlot <- ppSparseSlot
   return $ vcat $
-           [ "if (!" <+> b_slot <+> ") {"
+           [ -- "if (! _T.getSparseBit()) {" -- Alternative, but involves extra call to RT
+             "if (!" <+> sparseSlot <+> ") {"
            , nest 2 (vcat ii')
            , text "}"
            ]
@@ -391,30 +390,33 @@ ir2js InvalidateSparseBit = return $
 {-- TERMINATORS --}
 
 
-tr2js (Call bb bb2) = do 
-    _frameSize <- frameSize <$> get 
-    _boundSlot <- boundSlot <$> get 
-    _consts    <- consts <$> get 
-    modify (\s -> s {frameSize = 0, boundSlot = _boundSlot - _frameSize - 5})
+tr2js (Call bb bb2) = do
+    _frameSize <- gets frameSize
+    _sparseSlot <- gets sparseSlot
+    _consts <- gets consts
+    modify (\s -> s {frameSize = 0, sparseSlot = _sparseSlot - _frameSize - 5})
         -- AA; 2021-04-24; Because 
     js <- toJS bb
-    modify (\s -> s { frameSize = _frameSize, boundSlot = _boundSlot }) 
+    modify (\s -> s { frameSize = _frameSize, sparseSlot = _sparseSlot })
         -- TODO: AA; 2021-04-24; we should really be using a reader monad here for frame size
         -- #codedebt
     js2 <- toJS bb2
-    kname <- freshKontName 
-    b_slot <- data_bounded_by_pc_slot
-    b_slot_index <- b_slot_absolute_index
-    let jsKont = 
-           vcat ["this." PP.<> ppId kname <+> text "= () => {",                 
-                  nest 2 $ 
-                        vcat [                          
+    kname <- freshKontName
+    sparseSlotIdxPP <- ppSparseSlotIdx
+    let jsKont =
+           vcat ["this." PP.<> ppId kname <+> text "= () => {",
+                  nest 2 $
+                        vcat [
                           "let _T = rt.runtime.$t",
                           "let _STACK = _T.callStack",
                           "let _SP = _T._sp",
+                          -- TODO Do we need this? It seems to be only used zero or one time in the generated places.
+                          -- So we could instead just use the let where it is actually set.
                           "let _SP_OLD",
-                          b_slot <+> "= _T.checkDataBounds(" <+> b_slot <+> ")" , 
-                          "_T.boundSlot =" <+> b_slot_index ,
+                          -- Check data bound at return point (could have received labelled information or raised).
+                          -- Requires sparseSlot to be updated first.
+                          "_T.sparseSlot =" <+> sparseSlotIdxPP,
+                          "_T.updateSparseBitOnReturn()",
                           constsToJS _consts , -- 2021-05-18; TODO: optimize by including only the _used_ constants
                           js2
                         ],
@@ -479,15 +481,16 @@ monStateToJs c =
         R0_TLev -> text "r0_tlev"
 
 
-data_bounded_by_pc_slot  :: W PP.Doc 
-data_bounded_by_pc_slot = do    
-   _b <- boundSlot <$> get 
-   return $ text "_STACK[ _SP + "  PP.<> (text (show (_b)))  PP.<> text "]"
+ppSparseSlotIdx :: W PP.Doc
+ppSparseSlotIdx = do
+  s <- gets sparseSlot
+  return $ text "_SP + " PP.<+> PP.int s
+
+ppSparseSlot :: W PP.Doc 
+ppSparseSlot = do    
+   idx <- ppSparseSlotIdx
+   return $ text "_STACK[ "  PP.<> idx PP.<> text "]"
 
-b_slot_absolute_index :: W PP.Doc 
-b_slot_absolute_index = do 
-  _b <- boundSlot<$> get  
-  return $ text "_SP +" PP.<+> (PP.int _b)
 -----------------------------------------------------------
 
 
@@ -563,16 +566,16 @@ jsFunCall a b = semi $ ppFunCall a b
 
 
 freshEnvVar :: W VarName
-freshEnvVar = do 
-    k <- freshCounter <$>  get 
-    modify (\s -> s { freshCounter = k + 1  } )  
+freshEnvVar = do
+    k <- gets freshCounter
+    modify (\s -> s { freshCounter = k + 1  } )
     return $ VN  $ "$$$env" ++ (show k)
 
- 
+
 freshKontName :: W VarName
-freshKontName = do 
-    j <- freshCounter <$> get 
-    HFN s <- stHFN <$> get 
+freshKontName = do
+    j <- gets freshCounter
+    HFN s <- gets stHFN
     modify (\s -> s { freshCounter = j + 1})
     return $ VN $  "$$$" ++ s ++ "$$$kont" ++ (show j)
 
diff --git a/rt/src/Thread.mts b/rt/src/Thread.mts
@@ -212,9 +212,7 @@ export class Thread {
     next :  () => any;
     callStack : any []
     _sp : number;
-    boundSlot : number;
-    
-    _isDataBoundByPC: boolean = false;
+    sparseSlot : number; // slot on the stack holding the sparse bit (whether data is bounded by PC)
     
     processDebuggingName: string;
 
@@ -250,7 +248,7 @@ export class Thread {
         ---> stack growth direction --->
 
         |---------+-------------------+--------------+-----------------------------+---------------+-------------------------+--------------------|
-        | sp_prev | pc at return site | ret callback | mclear at the time of entry | branching bit | [escaping locals]       | bound_slot         |
+        | sp_prev | pc at return site | ret callback | mclear at the time of entry | branching bit | [escaping locals]       | sparse slot        |
         |---------+-------------------+--------------+-----------------------------+---------------+-------------------------+--------------------|
         | sp - 5  | sp - 4            | sp - 3       | sp - 2                      | sp - 1        | sp ... (sp + framesize) | sp + framesize + 1 |
 
@@ -329,7 +327,7 @@ export class Thread {
 
     showStack ()  {
         console.log ("======== SHOW STACK ========= ")
-        console.log (`sp = ${this._sp} boundslot = ${this.boundSlot}`)
+        console.log (`sp = ${this._sp} sparseSlot = ${this.sparseSlot}`)
         let j = this._sp - 1 
         let stack = this.callStack
         while ( j > 0) {
@@ -365,46 +363,51 @@ export class Thread {
         return f;
     }
 
+    getSparseBit() {
+        return this.callStack[this.sparseSlot]
+    }
 
-    invalidateSparseBit () {
-        this.callStack[this.boundSlot] = false;
-    }
-
-    // Check whether the label of R0 (argument), the data level of R0 and the given one are bound by PC.
-    checkDataBoundsEntry (x: Level) {
-        const _pc = this.pc 
-        let y = 
-             flowsTo(this.r0_lev, _pc) 
-              && 
-                flowsTo (x, _pc)
-                    && (this.r0_val._troupeType == undefined 
-                                ? true
-                                : flowsTo (this.r0_val.dataLevel, _pc)
-                        )
-             
-                                    
-        // this._isDataBoundByPC = y;    
-        return y;
-    }
-
-    // Check whether the label of R0 (return value) and the data level of R0 are bound by PC.
-    // Return false if x is false.
-    // TODO Better check x directly and do not call this function if false (now that _isDataBoundByPC is not updated).
-    checkDataBounds (x: boolean) {
-        const _pc = this.pc 
-        let y = 
-             x? flowsTo(this.r0_lev, _pc) 
-                    && (this.r0_val._troupeType == undefined 
-                                ? true
-                                : flowsTo (this.r0_val.dataLevel, _pc)
-                        )
-             : false 
-                                    
-        // this._isDataBoundByPC = y;    
-        return y;
+    invalidateSparseBit() {
+        this.callStack[this.sparseSlot] = false;
     }
 
-    
+    private setSparseBit(b: boolean) {
+        this.callStack[this.sparseSlot] = b;
+    }
+
+    /**
+     * Check whether the label of R0 (argument), the data level of R0 and the given label are bound by PC
+     * and update sparse bit accordingly.
+     */
+    updateSparseBitOnEntry(x: Level) {
+        const _pc = this.pc
+        // Only non-basic types (_troupeType is defined) have a data level. For those, it
+        // is sufficient to check r0_val.dataLevel ⊑ _pc, as r0_lev ⊑ r0_val.dataLev. For
+        // base types, we instead have to check r0_lev ⊑ _pc.
+        if (this.r0_val._troupeType != undefined) {
+            this.setSparseBit(flowsTo(x, _pc) && flowsTo(this.r0_val.dataLevel, _pc))
+        } else {
+            this.setSparseBit(flowsTo(x, _pc) && flowsTo(this.r0_lev, _pc))
+        }
+    }
+
+    /**
+     * If the sparse bit is set, check whether it is still valid for the returned value (and reset it if not):
+     * Check whether the label of R0 (return value) and the data level of R0 are bound by PC.
+     */
+    updateSparseBitOnReturn() {
+        const _pc = this.pc
+        if (this.getSparseBit()) {
+            // Only non-basic types (_troupeType is defined) have a data level. For those, it
+            // is sufficient to check r0_val.dataLevel ⊑ _pc, as r0_lev ⊑ r0_val.dataLev. For
+            // base types, we instead have to check r0_lev ⊑ _pc.
+            if (this.r0_val._troupeType != undefined) {
+                this.setSparseBit(flowsTo(this.r0_val.dataLevel, _pc))
+            } else {
+                this.setSparseBit(flowsTo(this.r0_lev, _pc))
+            }
+        }
+    }
 
 
     runNext (theFun, args, nm)  {
@@ -619,8 +622,7 @@ export class Thread {
 
 
     blockdeclto (auth, bl_to = this.pc) {        
-        let is_bounded_by_pc = flowsTo (this.pc, bl_to);
-        if (!is_bounded_by_pc) {
+        if (! flowsTo (this.pc, bl_to)) {
             this.threadError ("The provided target blocking level is lower than the current pc\n" + 
                               ` | the current pc: ${this.pc.stringRep()}\n` +
                               ` | target blocking level: ${bl_to.stringRep()}`)
diff --git a/rt/src/builtins/UserRuntimeZero.mts b/rt/src/builtins/UserRuntimeZero.mts
@@ -92,22 +92,11 @@ export class UserRuntimeZero {
         this.runtime.ret (x)
     }
 
-    join (...xs) {
-        if (this.runtime.$t._isDataBoundByPC) {
-            return this.runtime.$t.pc 
-        } 
+    // SimpleRT
+    raw_join(...xs) : Level {
         return lub.apply (null, xs)
     }
 
-    wrap_block_rhs (x) {
-        if (this.runtime.$t._isDataBoundByPC) {
-            return this.runtime.$t.bl 
-        } else {
-            return x;
-        }
-        
-    }
-
     // SpecialRT
     raw_invalidateSparseBit() {
         this.runtime.$t.invalidateSparseBit()
