From 7916b1f9aa93fca368afda8b18396230ac7f338c Mon Sep 17 00:00:00 2001
From: Araq <rumpf_a@web.de>
Date: Sun, 21 Sep 2014 18:39:00 +0200
Subject: implemented 'guard' annotation

---
 compiler/guards.nim | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'compiler/guards.nim')

diff --git a/compiler/guards.nim b/compiler/guards.nim
index 05128f409..cd0aaf296 100644
--- a/compiler/guards.nim
+++ b/compiler/guards.nim
@@ -838,6 +838,22 @@ proc addAsgnFact*(m: var TModel, key, value: PNode) =
   fact.sons[2] = value
   m.add fact
 
+proc sameSubexprs*(m: TModel; a, b: PNode): bool =
+  # This should be used to check whether two *path expressions* refer to the
+  # same memory location according to 'm'. This is tricky:
+  # lock a[i].guard:
+  #   ...
+  #   access a[i].guarded
+  #
+  # Here a[i] is the same as a[i] iff 'i' and 'a' are not changed via '...'.
+  # However, nil checking requires exactly the same mechanism! But for now
+  # we simply use sameTree and live with the unsoundness of the analysis.
+  var check = newNodeI(nkCall, a.info, 3)
+  check.sons[0] = newSymNode(opEq)
+  check.sons[1] = a
+  check.sons[2] = b
+  result = m.doesImply(check) == impYes
+
 proc addCaseBranchFacts*(m: var TModel, n: PNode, i: int) =
   let branch = n.sons[i]
   if branch.kind == nkOfBranch:
-- 
cgit 1.4.1-2-gfad0

199a2fd37568a5f5a6c7c394b160b229e90c'>refs</a> <a href='/ahoang/Nim/log/tests/manyloc/packages/os.nim?h=devel'>log</a> <a class='active' href='/ahoang/Nim/blame/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>blame</a> <a href='/ahoang/Nim/commit/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>commit</a> <a href='/ahoang/Nim/diff/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>diff</a> <a href='/ahoang/Nim/stats/tests/manyloc/packages/os.nim?h=devel'>stats</a></td><td class='form'><form class='right' method='get' action='/ahoang/Nim/log/tests/manyloc/packages/os.nim'>
<input type='hidden' name='h' value='devel'/><input type='hidden' name='id' value='bd90199a2fd37568a5f5a6c7c394b160b229e90c'/><select name='qt'>
<option value='grep'>log msg</option>
<option value='author'>author</option>
<option value='committer'>committer</option>
<option value='range'>range</option>
</select>
<input class='txt' type='search' size='10' name='q' value=''/>
<input type='submit' value='search'/>
</form>
</td></tr></table>
<div class='path'>path: <a href='/ahoang/Nim/blame/?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>root</a>/<a href='/ahoang/Nim/blame/tests?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>tests</a>/<a href='/ahoang/Nim/blame/tests/manyloc?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>manyloc</a>/<a href='/ahoang/Nim/blame/tests/manyloc/packages?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>packages</a>/<a href='/ahoang/Nim/blame/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>os.nim</a></div><div class='content'>blob: 8a59612f99efbf5d82d3c5b89ad84ffbd350a91d (<a href='/ahoang/Nim/plain/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>plain</a>) (<a href='/ahoang/Nim/tree/tests/manyloc/packages/os.nim?h=devel&amp;id=bd90199a2fd37568a5f5a6c7c394b160b229e90c'>tree</a>)
<table class='blame blob'>
<tr>
<td class='hashes'><div class='alt'><pre><span class='oid'><a title='author  Araq &lt;rumpf_a@web.de&gt;  2013-09-26 17:34:46 +0200
committer  Araq &lt;rumpf_a@web.de&gt;  2013-09-26 17:34:46 +0200

the compiler can now deal with multiple modules of the same name' href='/ahoang/Nim/commit/tests/manyloc/packages/os.nim?h=devel&amp;id=a0b82db40229620a29726fa33a4358db2f5fcd44'>a0b82db40</a></span> <a title='Blame the previous revision' href='/ahoang/Nim/blame/tests/manyloc/packages/os.nim?h=devel&amp;id=c085a1b4f058008b8320ad3a24e6598472f0daf9'>^</a>




</pre></div></td>
<td class='linenumbers'><div class='alt'><pre><a id='n1' href='#n1'>1</a>
<a id='n2' href='#n2'>2</a>
<a id='n3' href='#n3'>3</a>
<a id='n4' href='#n4'>4</a>
<a id='n5' href='#n5'>5</a>
</pre></div></td>
<td class='lines'><div><div><div class='alt'><pre>




                             </pre></div></div><pre><code>