<> <> <> <> <> <> <> <> DIRECTORY Basics USING [CARD, LowHalf], Rope USING [ROPE, Size], TextLooks USING [Looks, Runs, Size], TextLooksSupport USING [TbaseSize], Tioga USING [maxLen, Node], TiogaPrivate USING []; CheckNodeImpl: CEDAR PROGRAM IMPORTS TextLooks, TextLooksSupport, Rope, Basics EXPORTS TiogaPrivate SHARES Rope, TextLooks = BEGIN <> Node: TYPE ~ Tioga.Node; maxLen: INT ~ Tioga.maxLen; CheckFailed: PUBLIC ERROR = CODE; Check: PUBLIC PROC [node: Node] = { CheckRope[node.rope]; CheckRuns[node.runs]; }; CheckRope: PUBLIC PROC [rope: Rope.ROPE] = { size: INT _ Rope.Size[rope]; CheckRopeOffset[rope, size, size, 0]; ClearRopeCache[]; }; ropeCacheSize: NAT = 128; -- should be a power of 2 ropeCacheMax: NAT = (ropeCacheSize*2)/3; -- don't fill too full ropeCacheCount: NAT; -- number of entries currently in use RopeCache: TYPE = ARRAY [0..ropeCacheSize) OF Rope.ROPE; ropeCache: REF RopeCache _ NEW[RopeCache _ ALL[NIL]]; ClearRopeCache: PROC = { ropeCacheCount _ 0; FOR i: NAT IN [0..ropeCacheSize) DO ropeCache[i] _ NIL; ENDLOOP; }; CheckRopeOffset: PROC [rope: Rope.ROPE, sizeMin, sizeMax: INT, depth: NAT] = TRUSTED { <<-- use explicit recursion instead of looping so if there is an error,>> <<-- will be able to track it up the stack>> initloc, loc: NAT; found: BOOLEAN _ FALSE; IF rope=NIL THEN IF sizeMax=0 THEN RETURN ELSE ERROR CheckFailed; IF depth > 1000 THEN ERROR CheckFailed; loc _ initloc _ (LOOPHOLE[Basics.LowHalf[LOOPHOLE[rope]],CARDINAL]/16) MOD ropeCacheSize; DO -- search cache SELECT ropeCache[loc] FROM rope => { found _ TRUE; EXIT }; NIL => EXIT; -- this is an unused entry ENDCASE; SELECT (loc _ loc+1) FROM ropeCacheSize => IF (loc _ 0)=initloc THEN EXIT; initloc => EXIT; ENDCASE; ENDLOOP; IF ~found THEN { IF ropeCacheCount = ropeCacheMax THEN { loc _ initloc; ClearRopeCache[] }; ropeCache[loc] _ rope }; WITH x:rope SELECT FROM text => { SELECT LONG[x.length] FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; ENDCASE }; node => WITH x:x SELECT FROM substr => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; ENDCASE; IF ~found THEN CheckRopeOffset[x.base, x.size+x.start, maxLen, depth+1] }; concat => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; < x.pos => ERROR CheckFailed; ENDCASE; IF ~found THEN { CheckRopeOffset[x.base,x.pos,x.pos,depth+1]; CheckRopeOffset[x.rest,x.size-x.pos,x.size-x.pos,depth+1] }}; replace => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; < x.newPos => ERROR CheckFailed; ENDCASE; SELECT x.start FROM > x.newPos => ERROR CheckFailed; > x.oldPos => ERROR CheckFailed; ENDCASE; IF ~found THEN { CheckRopeOffset[x.replace,x.newPos-x.start,x.newPos-x.start,depth+1]; CheckRopeOffset[x.base,x.size+x.oldPos-x.newPos, x.size+x.oldPos-x.newPos,depth+1] }}; object => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; ENDCASE }; ENDCASE => ERROR CheckFailed; ENDCASE => ERROR CheckFailed; }; CheckRuns: PUBLIC PROC [runs: TextLooks.Runs] = { size: INT; IF runs=NIL THEN RETURN; size _ TextLooks.Size[runs]; CheckNodeRuns[runs,size,size,0]; ClearRunsCache[]; }; runsCacheSize: NAT = 128; -- should be a power of 2 runsCacheMax: NAT = (runsCacheSize*2)/3; -- don't fill too full runsCacheCount: NAT; -- number of entries currently in use RunsCache: TYPE = ARRAY [0..runsCacheSize) OF TextLooks.Runs; runsCache: REF RunsCache _ NEW[RunsCache _ ALL[NIL]]; ClearRunsCache: PROC = { runsCacheCount _ 0; FOR i: NAT IN [0..runsCacheSize) DO runsCache[i] _ NIL; ENDLOOP; }; CheckNodeRuns: PROC [ runs: TextLooks.Runs, sizeMin, sizeMax: INT, depth: NAT] = TRUSTED { <<-- use explicit recursion instead of looping so if there is an error,>> <<-- will be able to track it up the stack>> initloc, loc: NAT; found: BOOLEAN _ FALSE; IF runs=NIL THEN IF sizeMax=0 THEN RETURN ELSE ERROR CheckFailed; IF depth > 1000 THEN ERROR CheckFailed; loc _ initloc _ (LOOPHOLE[Basics.LowHalf[LOOPHOLE[runs]],CARDINAL]/16) MOD runsCacheSize; DO -- search cache SELECT runsCache[loc] FROM runs => { found _ TRUE; EXIT }; NIL => EXIT; -- this is an unused entry ENDCASE; SELECT (loc _ loc+1) FROM runsCacheSize => IF (loc _ 0)=initloc THEN EXIT; initloc => EXIT; ENDCASE; ENDLOOP; IF ~found THEN { IF runsCacheCount = runsCacheMax THEN { loc _ initloc; ClearRunsCache[] }; runsCache[loc] _ runs }; WITH x:runs SELECT FROM base => { SELECT TextLooksSupport.TbaseSize[@x] FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; ENDCASE; IF ~found THEN { loc: INT; looks: TextLooks.Looks; IF x.length=0 THEN ERROR CheckFailed; loc _ x[0].after; looks _ x[0].looks; FOR i:NAT IN (0..x.length) DO IF x[i].after <= loc THEN ERROR CheckFailed; IF x[i].looks = looks THEN ERROR CheckFailed; loc _ x[i].after; looks _ x[i].looks; ENDLOOP }}; node => WITH x:x SELECT FROM substr => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; ENDCASE; IF ~found THEN CheckNodeRuns[x.base,x.size+x.start,maxLen,depth+1] }; concat => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; < x.pos => ERROR CheckFailed; ENDCASE; IF ~found THEN { CheckNodeRuns[x.base,x.pos,x.pos,depth+1]; CheckNodeRuns[x.rest,x.size-x.pos,x.size-x.pos,depth+1] }}; replace => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; < x.newPos => ERROR CheckFailed; ENDCASE; SELECT x.start FROM > x.newPos => ERROR CheckFailed; > x.oldPos => ERROR CheckFailed; ENDCASE; IF ~found THEN { CheckNodeRuns[x.replace,x.newPos-x.start,x.newPos-x.start,depth+1]; CheckNodeRuns[x.base,x.size+x.oldPos-x.newPos, x.size+x.oldPos-x.newPos,depth+1] }}; change => { SELECT x.size FROM < sizeMin => ERROR CheckFailed; > sizeMax => ERROR CheckFailed; < x.start+x.len => ERROR CheckFailed; ENDCASE; IF ~found THEN CheckNodeRuns[x.base,x.size,x.size,depth+1] }; ENDCASE => ERROR CheckFailed; ENDCASE => ERROR CheckFailed; }; <> <<--limits>> maxDepth: CARDINAL = 2000; Depth: TYPE = [0..maxDepth); <<--globals>> Verify: PUBLIC PROC [node: Node] = { VerifyNode[node,0] }; VerifyNode: PROC [parent: Node, vdepth: Depth] = { hDepth: Depth _ 0; Check[parent]; -- checks rope & runs for text node IF vdepth >= maxDepth THEN ERROR; -- tree is too deep to believe IF parent.child = NIL THEN RETURN; FOR tn: Node _ parent.child, tn.next DO IF tn = NIL THEN ERROR; VerifyNode[tn, vdepth+1]; IF tn.last THEN { IF tn.next = parent THEN RETURN; IF tn.next # NIL THEN FindSmashedLink[parent, tn.next]; ERROR }; IF (hDepth _ hDepth + 1) >= maxDepth THEN ERROR; -- too many siblings to believe ENDLOOP; }; --VerifyNode <<--FindSmashedLink is called when the node pointed to at the end of>> <<--a sibling chain is not the parent who started the chain. We assume>> <<--some pointer in that chain is smashed and is pointing to some>> <<--other random but wellformed section of the tree. We then traverse>> <<--the startparent sibling chain, looking for the first node whose immediate>> <<--sibling is a son of the endparent. That is the smashed node, called badguy.>> FindSmashedLink: PROC[startparent: Node, endparent: Node] = { badguy: Node _ startparent; -- this will finally be the node with a smashed pointer FOR tnode: Node _ startparent.child, tnode.next UNTIL tnode.last DO FOR bnode: Node _ endparent.child, bnode.next UNTIL bnode.last DO IF tnode = bnode THEN ERROR; -- tnode is a child of endparent <<-- but is pointed to by badguy, a child of startparent>> <<-- or tnode=startparent.child and startparent=badguy>> badguy _ tnode; ENDLOOP; ENDLOOP; }; --FindSmashedLink <> ClearRopeCache[]; ClearRunsCache[]; END.