Add lexer for the Silver language

3 files changed, 256 insertions, 1 deletions

diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py
index a08e806c..3fe81907 100644
--- a/pygments/lexers/_mapping.py
+++ b/pygments/lexers/_mapping.py
@@ -347,6 +347,7 @@ LEXERS = {
     'RubyConsoleLexer': ('pygments.lexers.ruby', 'Ruby irb session', ('rbcon', 'irb'), (), ('text/x-ruby-shellsession',)),
     'RubyLexer': ('pygments.lexers.ruby', 'Ruby', ('rb', 'ruby', 'duby'), ('*.rb', '*.rbw', 'Rakefile', '*.rake', '*.gemspec', '*.rbx', '*.duby', 'Gemfile'), ('text/x-ruby', 'application/x-ruby')),
     'RustLexer': ('pygments.lexers.rust', 'Rust', ('rust',), ('*.rs', '*.rs.in'), ('text/rust',)),
+    'SilverLexer': ('pygments.lexers.esoteric', 'Silver', ('silver',), ('*.sil',), ()),
     'SLexer': ('pygments.lexers.r', 'S', ('splus', 's', 'r'), ('*.S', '*.R', '.Rhistory', '.Rprofile', '.Renviron'), ('text/S-plus', 'text/S', 'text/x-r-source', 'text/x-r', 'text/x-R', 'text/x-r-history', 'text/x-r-profile')),
     'SMLLexer': ('pygments.lexers.ml', 'Standard ML', ('sml',), ('*.sml', '*.sig', '*.fun'), ('text/x-standardml', 'application/x-standardml')),
     'SassLexer': ('pygments.lexers.css', 'Sass', ('sass',), ('*.sass',), ('text/x-sass',)),
diff --git a/pygments/lexers/esoteric.py b/pygments/lexers/esoteric.py
index 73ea4a4a..d7951c35 100644
--- a/pygments/lexers/esoteric.py
+++ b/pygments/lexers/esoteric.py
@@ -13,7 +13,7 @@ from pygments.lexer import RegexLexer, include, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
     Number, Punctuation, Error, Whitespace
 
-__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer', 'CAmkESLexer']
+__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer', 'CAmkESLexer', 'SilverLexer']
 
 
 class BrainfuckLexer(RegexLexer):
@@ -217,3 +217,51 @@ class BoogieLexer(RegexLexer):
             (r'[0-9]+', Number.Integer),
         ],
     }
+
+class SilverLexer(RegexLexer):
+    """
+    For `Silver <https://bitbucket.org/viperproject/silver>`_ source code.
+
+    .. versionadded:: 2.1
+    """
+    name = 'Silver'
+    aliases = ['silver']
+    filenames = ['*.sil']
+
+    tokens = {
+        'root': [
+            # Whitespace and Comments
+            (r'\n', Whitespace),
+            (r'\s+', Whitespace),
+            (r'//[/!](.*?)\n', Comment.Doc),
+            (r'//(.*?)\n', Comment.Single),
+            (r'/\*', Comment.Multiline, 'comment'),
+
+            (words((
+                'result', 'true', 'false', 'null', 'method', 'function',
+                'predicate', 'program', 'domain', 'axiom', 'var', 'returns',
+                'field', 'define', 'requires', 'ensures', 'invariant',
+                'fold', 'unfold', 'inhale', 'exhale', 'new', 'assert',
+                'assume', 'goto', 'while', 'if', 'elseif', 'else', 'fresh',
+                'constraining', 'Seq', 'Set', 'Multiset', 'union', 'intersection',
+                'setminus', 'subset', 'unfolding', 'in', 'old', 'forall', 'exists',
+                'acc', 'wildcard', 'write', 'none', 'epsilon', 'perm', 'unique'),
+             suffix=r'\b'), Keyword),
+            (words(('Int', 'Perm', 'Bool', 'Ref'), suffix=r'\b'), Keyword.Type),
+            include('numbers'),
+
+            (r'[!%&*+=|?:<>/-]', Operator),
+            (r"([{}():;,.])", Punctuation),
+            # Identifier
+            (r'[a-zA-Z_$0-9]\w*', Name),
+        ],
+        'comment': [
+            (r'[^*/]+', Comment.Multiline),
+            (r'/\*', Comment.Multiline, '#push'),
+            (r'\*/', Comment.Multiline, '#pop'),
+            (r'[*/]', Comment.Multiline),
+        ],
+        'numbers': [
+            (r'[0-9]+', Number.Integer),
+        ],
+    }
diff --git a/tests/examplefiles/test.sil b/tests/examplefiles/test.sil
new file mode 100644
index 00000000..3bcee835
--- /dev/null
+++ b/tests/examplefiles/test.sil
@@ -0,0 +1,206 @@
+domain Option__Node {
+    unique function Option__Node__Some(): Option__Node
+    unique function Option__Node__None(): Option__Node
+
+    function variantOfOptionNode(self: Ref): Option__Node
+
+    function isOptionNode(self: Ref): Bool
+
+    axiom ax_variantOfOptionNodeChoices {
+        forall x: Ref :: { variantOfOptionNode(x) }
+            (variantOfOptionNode(x) == Option__Node__Some() || variantOfOptionNode(x) == Option__Node__None())
+    }
+
+    axiom ax_isCounterState {
+        forall x: Ref ::  { variantOfOptionNode(x) }
+            isOptionNode(x) == (variantOfOptionNode(x) == Option__Node__Some() ||
+                variantOfOptionNode(x) == Option__Node__None())
+    }
+}
+
+predicate validOption(this: Ref) {
+    isOptionNode(this) &&
+    variantOfOptionNode(this) == Option__Node__Some() ==> (
+        acc(this.Option__Node__Some__1, write) &&
+        acc(validNode(this.Option__Node__Some__1))
+    )
+}
+
+field Option__Node__Some__1: Ref
+
+field Node__v: Int
+field Node__next: Ref
+
+predicate validNode(this: Ref) {
+    acc(this.Node__v) &&
+    acc(this.Node__next) &&
+    acc(validOption(this.Node__next))
+}
+
+
+function length(this: Ref): Int
+    requires acc(validNode(this), write)
+    ensures result >= 1
+{
+    (unfolding acc(validNode(this), write) in
+        unfolding acc(validOption(this.Node__next)) in
+        (variantOfOptionNode(this.Node__next) == Option__Node__None()) ? 
+            1 : 1 + length(this.Node__next.Option__Node__Some__1)
+    )
+}
+
+function itemAt(this: Ref, i: Int): Int
+    requires acc(validNode(this), write)
+    requires 0 <= i && i < length(this)
+{
+    unfolding acc(validNode(this), write) in unfolding acc(validOption(this.Node__next)) in (
+        (i == 0) ?
+            this.Node__v:
+            (variantOfOptionNode(this.Node__next) == Option__Node__Some()) ? 
+                itemAt(this.Node__next.Option__Node__Some__1, i-1) : this.Node__v
+    )
+}
+
+function sum(this$1: Ref): Int
+    requires acc(validNode(this$1), write)
+{
+    (unfolding acc(validNode(this$1), write) in unfolding acc(validOption(this$1.Node__next)) in 
+        (variantOfOptionNode(this$1.Node__next) == Option__Node__None()) ? this$1.Node__v : this$1.Node__v + sum(this$1.Node__next.Option__Node__Some__1))
+}
+
+method append(this: Ref, val: Int)
+    requires acc(validNode(this), write)
+    ensures acc(validNode(this), write) /* POST1 */
+    ensures length(this) == (old(length(this)) + 1) /* POST2 */
+    ensures (forall i: Int :: (0 <= i && i < old(length(this))) ==> (itemAt(this, i) == old(itemAt(this, i)))) /* POST3 */
+    ensures itemAt(this, length(this) - 1) == val /* POST4 */
+    ensures true ==> true
+{
+    var tmp_node: Ref
+    var tmp_option: Ref
+
+    unfold acc(validNode(this), write)
+    unfold acc(validOption(this.Node__next), write)
+
+    if (variantOfOptionNode(this.Node__next) == Option__Node__None()) {
+        tmp_node := new(Node__next, Node__v)
+        tmp_node.Node__next := null
+        tmp_node.Node__v := val
+
+        assume variantOfOptionNode(tmp_node.Node__next) == Option__Node__None()
+        fold acc(validOption(tmp_node.Node__next))
+        fold acc(validNode(tmp_node), write)
+
+        tmp_option := new(Option__Node__Some__1)
+        tmp_option.Option__Node__Some__1 := tmp_node
+        assume variantOfOptionNode(tmp_option) == Option__Node__Some()
+        fold acc(validOption(tmp_option))
+
+        this.Node__next := tmp_option
+
+ 
+        unfold validOption(tmp_option)
+        assert length(tmp_node) == 1 /* TODO: Required by Silicon, POST2 fails otherwise */
+        assert itemAt(tmp_node, 0) == val /* TODO: Required by Silicon, POST4 fails otherwise */
+        fold validOption(tmp_option)
+    } else {
+        append(this.Node__next.Option__Node__Some__1, val)
+        fold acc(validOption(this.Node__next), write)
+    }
+
+    fold acc(validNode(this), write)
+}
+
+method prepend(tail: Ref, val: Int) returns (res: Ref)
+    requires acc(validNode(tail))
+    ensures acc(validNode(res))
+    //ensures acc(validNode(tail))
+    ensures length(res) == old(length(tail)) + 1
+
+    ensures (forall i: Int :: (1 <= i && i < length(res)) ==> (itemAt(res, i) == old(itemAt(tail, i-1)))) /* POST3 */
+    ensures itemAt(res, 0) == val
+{
+    var tmp_option: Ref
+
+    res := new(Node__v, Node__next)
+    res.Node__v := val
+
+    tmp_option := new(Option__Node__Some__1)
+    tmp_option.Option__Node__Some__1 := tail
+    assume variantOfOptionNode(tmp_option) == Option__Node__Some()
+
+    res.Node__next := tmp_option
+
+    assert acc(validNode(tail))
+    fold acc(validOption(res.Node__next))
+    fold acc(validNode(res))
+}
+
+method length_iter(list: Ref) returns (len: Int)
+    requires acc(validNode(list), write)
+    ensures old(length(list)) == len
+    // TODO we have to preserve this property
+    // ensures acc(validNode(list))
+{
+    var curr: Ref := list
+    var tmp: Ref := list
+
+    len := 1
+
+    unfold acc(validNode(curr))
+    unfold acc(validOption(curr.Node__next))
+    while(variantOfOptionNode(curr.Node__next) == Option__Node__Some())
+        invariant acc(curr.Node__v)
+        invariant acc(curr.Node__next)
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> (
+            acc(curr.Node__next.Option__Node__Some__1, write) &&
+            acc(validNode(curr.Node__next.Option__Node__Some__1))
+        ))
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> len + length(curr.Node__next.Option__Node__Some__1) == old(length(list)))
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__None() ==> len == old(length(list)))
+    {
+        assert acc(validNode(curr.Node__next.Option__Node__Some__1))
+        len := len + 1
+        tmp := curr
+        curr := curr.Node__next.Option__Node__Some__1
+        unfold acc(validNode(curr))
+        unfold acc(validOption(curr.Node__next))
+    }
+}
+
+method t1()
+{
+    var l: Ref
+
+    l := new(Node__v, Node__next)
+    l.Node__next := null
+    l.Node__v := 1
+    assume variantOfOptionNode(l.Node__next) == Option__Node__None()
+
+    fold validOption(l.Node__next)
+    fold validNode(l)
+
+    assert length(l) == 1
+    assert itemAt(l, 0) == 1
+
+    append(l, 7)
+    assert itemAt(l, 1) == 7
+    assert itemAt(l, 0) == 1
+    assert length(l) == 2
+
+    l := prepend(l, 10)
+    assert itemAt(l, 2) == 7
+    assert itemAt(l, 1) == 1
+    assert itemAt(l, 0) == 10
+    assert length(l) == 3
+
+    //assert sum(l) == 18
+}
+
+method t2(l: Ref) returns (res: Ref)
+    requires acc(validNode(l), write)
+    ensures acc(validNode(res), write)
+    ensures length(res) > old(length(l))
+{
+    res := prepend(l, 10)
+}