Support for policies in first-order logic
diff --git a/demo.py b/demo.py
index ad07c4c..d4c03af 100644
--- a/demo.py
+++ b/demo.py
@@ -1,4 +1,4 @@
-import plyproto.parser as plyproto
+import plyxproto.parser as plyproto
test1 = """package tutorial;"""
@@ -16,7 +16,9 @@
option java_outer_classname = "PushNotifications";
option optimize_for = SPEED;
- message Person(types.Actor) {
+ policy slice_user <foobar>
+
+ message Person(core.Actor) {
required string name = 1;
required int32 id = 2;
optional string email = 3;
@@ -45,5 +47,6 @@
extensions 500 to max;
}"""
+p5 = '''policy foo <exists foo: foo.x=foo.y>'''
parser = plyproto.ProtobufAnalyzer()
-print(parser.parse_string(test3))
+print(parser.parse_string(p5))
diff --git a/foldemo.py b/foldemo.py
new file mode 100644
index 0000000..e924e54
--- /dev/null
+++ b/foldemo.py
@@ -0,0 +1,18 @@
+from plyxproto.logicparser import *
+import ply.lex as lex
+import ply.yacc as yacc
+
+test_1 = "true"
+test_2 = "a | b"
+test_3 = "exists a: x=y"
+test_4 = "forall a: exists b: x.b=y.b"
+test_5 = "forall a: {{ a.endswith('good') }} "
+
+DEBUG = 0
+
+lexer = lex.lex(module=FOLLexer(), debug=DEBUG)#, optimize=1)
+parser = yacc.yacc(module=FOLParser(), start='goal', debug=DEBUG)
+
+for x,v in globals().items():
+ if x.startswith('test_'):
+ print parser.parse(v, lexer = lexer, debug=DEBUG)
diff --git a/plyxproto/helpers.py b/plyxproto/helpers.py
new file mode 100644
index 0000000..b059c17
--- /dev/null
+++ b/plyxproto/helpers.py
@@ -0,0 +1,178 @@
+class LexHelper:
+ offset = 0
+ def get_max_linespan(self, p):
+ defSpan=[1e60, -1]
+ mSpan=[1e60, -1]
+ for sp in range(0, len(p)):
+ csp = p.linespan(sp)
+ if csp[0] == 0 and csp[1] == 0:
+ if hasattr(p[sp], "linespan"):
+ csp = p[sp].linespan
+ else:
+ continue
+ if csp == None or len(csp) != 2: continue
+ if csp[0] == 0 and csp[1] == 0: continue
+ if csp[0] < mSpan[0]: mSpan[0] = csp[0]
+ if csp[1] > mSpan[1]: mSpan[1] = csp[1]
+ if defSpan == mSpan: return (0,0)
+ return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
+
+ def get_max_lexspan(self, p):
+ defSpan=[1e60, -1]
+ mSpan=[1e60, -1]
+ for sp in range(0, len(p)):
+ csp = p.lexspan(sp)
+ if csp[0] == 0 and csp[1] == 0:
+ if hasattr(p[sp], "lexspan"):
+ csp = p[sp].lexspan
+ else:
+ continue
+ if csp == None or len(csp) != 2: continue
+ if csp[0] == 0 and csp[1] == 0: continue
+ if csp[0] < mSpan[0]: mSpan[0] = csp[0]
+ if csp[1] > mSpan[1]: mSpan[1] = csp[1]
+ if defSpan == mSpan: return (0,0)
+ return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
+
+ def set_parse_object(self, dst, p):
+ dst.setLexData(linespan=self.get_max_linespan(p), lexspan=self.get_max_lexspan(p))
+ dst.setLexObj(p)
+
+class Base(object):
+ parent = None
+ lexspan = None
+ linespan = None
+
+ def v(self, obj, visitor):
+ if obj == None:
+ return
+ elif hasattr(obj, "accept"):
+ obj.accept(visitor)
+ elif isinstance(obj, list):
+ for s in obj:
+ self.v(s, visitor)
+ pass
+ pass
+
+ @staticmethod
+ def p(obj, parent):
+ if isinstance(obj, list):
+ for s in obj:
+ Base.p(s, parent)
+
+ if hasattr(obj, "parent"):
+ obj.parent = parent
+
+# Lexical unit - contains lexspan and linespan for later analysis.
+class LU(Base):
+ def __init__(self, p, idx):
+ self.p = p
+ self.idx = idx
+ self.pval = p[idx]
+ self.lexspan = p.lexspan(idx)
+ self.linespan = p.linespan(idx)
+
+ # If string is in the value (raw value) and start and stop lexspan is the same, add real span
+ # obtained by string length.
+ if isinstance(self.pval, str) \
+ and self.lexspan != None \
+ and self.lexspan[0] == self.lexspan[1] \
+ and self.lexspan[0] != 0:
+ self.lexspan = tuple([self.lexspan[0], self.lexspan[0] + len(self.pval)])
+ super(LU, self).__init__()
+
+ @staticmethod
+ def i(p, idx):
+ if isinstance(p[idx], LU): return p[idx]
+ if isinstance(p[idx], str): return LU(p, idx)
+ return p[idx]
+
+ def describe(self):
+ return "LU(%s,%s)" % (self.pval, self.lexspan)
+
+ def __str__(self):
+ return self.pval
+
+ def __repr__(self):
+ return self.describe()
+
+ def accept(self, visitor):
+ self.v(self.pval, visitor)
+
+ def __iter__(self):
+ for x in self.pval:
+ yield x
+
+# Base node
+class SourceElement(Base):
+ '''
+ A SourceElement is the base class for all elements that occur in a Protocol Buffers
+ file parsed by plyproto.
+ '''
+ def __init__(self, linespan=[], lexspan=[], p=None):
+ super(SourceElement, self).__init__()
+ self._fields = [] # ['linespan', 'lexspan']
+ self.linespan = linespan
+ self.lexspan = lexspan
+ self.p = p
+
+ def __repr__(self):
+ equals = ("{0}={1!r}".format(k, getattr(self, k))
+ for k in self._fields)
+ args = ", ".join(equals)
+ return "{0}({1})".format(self.__class__.__name__, args)
+
+ def __eq__(self, other):
+ try:
+ return self.__dict__ == other.__dict__
+ except AttributeError:
+ return False
+
+ def __ne__(self, other):
+ return not self == other
+
+ def setLexData(self, linespan, lexspan):
+ self.linespan = linespan
+ self.lexspan = lexspan
+
+ def setLexObj(self, p):
+ self.p = p
+
+ def accept(self, visitor):
+ pass
+
+class Visitor(object):
+
+ def __init__(self, verbose=False):
+ self.verbose = verbose
+
+ def __getattr__(self, name):
+ if not name.startswith('visit_'):
+ raise AttributeError('name must start with visit_ but was {}'.format(name))
+
+ def f(element):
+ if self.verbose:
+ msg = 'unimplemented call to {}; ignoring ({})'
+ print(msg.format(name, element))
+ return True
+ return f
+
+ # visitor.visit_PackageStatement(self)
+ # visitor.visit_ImportStatement(self)
+ # visitor.visit_OptionStatement(self)
+ # visitor.visit_FieldDirective(self)
+ # visitor.visit_FieldType(self)
+ # visitor.visit_FieldDefinition(self)
+ # visitor.visit_EnumFieldDefinition(self)
+ # visitor.visit_EnumDefinition(self)
+ # visitor.visit_MessageDefinition(self)
+ # visitor.visit_MessageExtension(self)
+ # visitor.visit_MethodDefinition(self)
+ # visitor.visit_ServiceDefinition(self)
+ # visitor.visit_ExtensionsDirective(self)
+ # visitor.visit_Literal(self)
+ # visitor.visit_Name(self)
+ # visitor.visit_Proto(self)
+ # visitor.visit_LU(self)
+
+
diff --git a/plyxproto/logicparser.py b/plyxproto/logicparser.py
new file mode 100644
index 0000000..8bdfb1c
--- /dev/null
+++ b/plyxproto/logicparser.py
@@ -0,0 +1,119 @@
+__author__ = "Sapan Bhatia"
+
+__copyright__ = "Copyright (C) 2017 Open Networking Lab"
+__version__ = "1.0"
+
+import ply.lex as lex
+import ply.yacc as yacc
+
+from helpers import LexHelper, LU
+
+class FOLLexer(object):
+ keywords = ('forall', 'exists', 'true', 'false', 'not')
+
+ tokens = ['ESCAPE', 'COLON', 'IMPLIES', 'OR', 'AND', 'LPAREN', 'RPAREN', 'EQUALS', 'SYMBOL', 'LT', 'RT'] + [k.upper() for k in keywords]
+ # literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+ t_ignore_LINE_COMMENT = '//.*'
+ t_COLON = '\\:'
+ t_IMPLIES = '\\-\\>'
+ t_OR = '\\|'
+ t_LT = '\\<'
+ t_RT = '\\>'
+ t_AND = '\\&'
+ t_LPAREN = '\\('
+ t_RPAREN = '\\)'
+
+ t_EQUALS = '\\='
+
+ literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
+
+ t_ignore = ' \t\f'
+
+ def t_newline(self, t):
+ r'\n+'
+ t.lexer.lineno += len(t.value)
+
+ def t_newline2(self, t):
+ r'(\r\n)+'
+ t.lexer.lineno += len(t.value) / 2
+
+ t_ESCAPE = r'{{ (.|\n)*? }}'
+
+ def t_BLOCK_COMMENT(self, t):
+ r'/\*(.|\n)*?\*/'
+ t.lexer.lineno += t.value.count('\n')
+
+ def t_SYMBOL(self, t):
+ '[A-Za-z_$][\.A-Za-z0-9_+$]*'
+ if t.value in FOLLexer.keywords:
+ t.type = t.value.upper()
+ return t
+
+ def t_error(self, t):
+ print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno))
+ t.lexer.skip(1)
+
+
+
+class FOLParser(object):
+ tokens = FOLLexer.tokens
+ offset = 0
+ lh = LexHelper()
+
+ def setOffset(self, of):
+ self.offset = of
+ self.lh.offset = of
+
+ def p_empty(self, p):
+ '''empty :'''
+ pass
+
+ def p_term_constant(self, p):
+ '''term : FALSE
+ | TRUE'''
+ p[0] = p[1]
+
+ def p_fole_not(self, p):
+ '''fole : NOT fole'''
+ p[0] = {p[1]: p[2]}
+
+ def p_fole_term(self, p):
+ '''fole : term'''
+ p[0] = p[1]
+
+ def p_term_symbol(self, p):
+ '''term : SYMBOL'''
+ p[0] = p[1]
+
+ def p_term_python(self, p):
+ '''fole : ESCAPE '''
+ p[0] = {'python': p[1]}
+
+ def p_fole_group(self, p):
+ "fole : LPAREN fole RPAREN"
+ p[0] = p[2]
+
+ def p_fole_equals(self, p):
+ "fole : term EQUALS term"
+ p[0] = {'=': (p[1], p[3])}
+
+ def p_fole_binary(self, p):
+ '''fole : fole AND fole
+ | fole OR fole
+ | fole IMPLIES fole'''
+ p[0] = {p[2]: [p[1], p[3]]}
+
+ def p_fole_quant(self, p):
+ '''fole : FORALL SYMBOL COLON fole
+ | EXISTS SYMBOL COLON fole'''
+ p[0] = {p[1]: [p[2], p[4]]}
+
+
+ def p_goal(self, p):
+ '''goal : LT fole RT'''
+ p[0] = p[2]
+
+ def p_error(self, p):
+ print('error: {}'.format(p))
+
diff --git a/plyxproto/model.py b/plyxproto/model.py
index 7acf7a3..3f33704 100644
--- a/plyxproto/model.py
+++ b/plyxproto/model.py
@@ -1,144 +1,4 @@
-__author__ = "Dusan (Ph4r05) Klinec"
-__copyright__ = "Copyright (C) 2014 Dusan (ph4r05) Klinec"
-__license__ = "Apache License, Version 2.0"
-__version__ = "1.0"
-
-class Visitor(object):
-
- def __init__(self, verbose=False):
- self.verbose = verbose
-
- def __getattr__(self, name):
- if not name.startswith('visit_'):
- raise AttributeError('name must start with visit_ but was {}'.format(name))
-
- def f(element):
- if self.verbose:
- msg = 'unimplemented call to {}; ignoring ({})'
- print(msg.format(name, element))
- return True
- return f
-
- # visitor.visit_PackageStatement(self)
- # visitor.visit_ImportStatement(self)
- # visitor.visit_OptionStatement(self)
- # visitor.visit_FieldDirective(self)
- # visitor.visit_FieldType(self)
- # visitor.visit_FieldDefinition(self)
- # visitor.visit_EnumFieldDefinition(self)
- # visitor.visit_EnumDefinition(self)
- # visitor.visit_MessageDefinition(self)
- # visitor.visit_MessageExtension(self)
- # visitor.visit_MethodDefinition(self)
- # visitor.visit_ServiceDefinition(self)
- # visitor.visit_ExtensionsDirective(self)
- # visitor.visit_Literal(self)
- # visitor.visit_Name(self)
- # visitor.visit_Proto(self)
- # visitor.visit_LU(self)
-
-class Base(object):
- parent = None
- lexspan = None
- linespan = None
-
- def v(self, obj, visitor):
- if obj == None:
- return
- elif hasattr(obj, "accept"):
- obj.accept(visitor)
- elif isinstance(obj, list):
- for s in obj:
- self.v(s, visitor)
- pass
- pass
-
- @staticmethod
- def p(obj, parent):
- if isinstance(obj, list):
- for s in obj:
- Base.p(s, parent)
-
- if hasattr(obj, "parent"):
- obj.parent = parent
-
-# Lexical unit - contains lexspan and linespan for later analysis.
-class LU(Base):
- def __init__(self, p, idx):
- self.p = p
- self.idx = idx
- self.pval = p[idx]
- self.lexspan = p.lexspan(idx)
- self.linespan = p.linespan(idx)
-
- # If string is in the value (raw value) and start and stop lexspan is the same, add real span
- # obtained by string length.
- if isinstance(self.pval, str) \
- and self.lexspan != None \
- and self.lexspan[0] == self.lexspan[1] \
- and self.lexspan[0] != 0:
- self.lexspan = tuple([self.lexspan[0], self.lexspan[0] + len(self.pval)])
- super(LU, self).__init__()
-
- @staticmethod
- def i(p, idx):
- if isinstance(p[idx], LU): return p[idx]
- if isinstance(p[idx], str): return LU(p, idx)
- return p[idx]
-
- def describe(self):
- return "LU(%s,%s)" % (self.pval, self.lexspan)
-
- def __str__(self):
- return self.pval
-
- def __repr__(self):
- return self.describe()
-
- def accept(self, visitor):
- self.v(self.pval, visitor)
-
- def __iter__(self):
- for x in self.pval:
- yield x
-
-# Base node
-class SourceElement(Base):
- '''
- A SourceElement is the base class for all elements that occur in a Protocol Buffers
- file parsed by plyproto.
- '''
- def __init__(self, linespan=[], lexspan=[], p=None):
- super(SourceElement, self).__init__()
- self._fields = [] # ['linespan', 'lexspan']
- self.linespan = linespan
- self.lexspan = lexspan
- self.p = p
-
- def __repr__(self):
- equals = ("{0}={1!r}".format(k, getattr(self, k))
- for k in self._fields)
- args = ", ".join(equals)
- return "{0}({1})".format(self.__class__.__name__, args)
-
- def __eq__(self, other):
- try:
- return self.__dict__ == other.__dict__
- except AttributeError:
- return False
-
- def __ne__(self, other):
- return not self == other
-
- def setLexData(self, linespan, lexspan):
- self.linespan = linespan
- self.lexspan = lexspan
-
- def setLexObj(self, p):
- self.p = p
-
- def accept(self, visitor):
- pass
+from helpers import Base, SourceElement
class PackageStatement(SourceElement):
def __init__(self, name, linespan=None, lexspan=None, p=None):
@@ -258,6 +118,20 @@
self.v(self.name, visitor)
self.v(self.fieldId, visitor)
+class PolicyDefinition(SourceElement):
+ def __init__(self, name, body, linespan=None, lexspan=None, p=None):
+ super(PolicyDefinition, self).__init__(linespan=linespan, lexspan=lexspan, p=p)
+ self._fields += ['name', 'body']
+ self.name = name
+ Base.p(self.name, self)
+ self.body = body
+ Base.p(self.body, self)
+
+ def accept(self, visitor):
+ if visitor.visit_EnumDefinition(self):
+ self.v(self.name, visitor)
+ self.v(self.body, visitor)
+
class EnumDefinition(SourceElement):
def __init__(self, name, body, linespan=None, lexspan=None, p=None):
super(EnumDefinition, self).__init__(linespan=linespan, lexspan=lexspan, p=p)
diff --git a/plyxproto/parser.py b/plyxproto/parser.py
index 72899e1..443ebb1 100755
--- a/plyxproto/parser.py
+++ b/plyxproto/parser.py
@@ -9,25 +9,31 @@
from .model import *
import pdb
+from helpers import LexHelper, LU
+from logicparser import FOLParser, FOLLexer
class ProtobufLexer(object):
keywords = ('double', 'float', 'int32', 'int64', 'uint32', 'uint64', 'sint32', 'sint64',
'fixed32', 'fixed64', 'sfixed32', 'sfixed64', 'bool', 'string', 'bytes',
'message', 'required', 'optional', 'repeated', 'enum', 'extensions', 'max', 'extend',
- 'to', 'package', '_service', 'rpc', 'returns', 'true', 'false', 'option', 'import', 'manytoone', 'manytomany', 'onetoone')
+ 'to', 'package', '_service', 'rpc', 'returns', 'true', 'false', 'option', 'import', 'manytoone', 'manytomany', 'onetoone', 'policy')
tokens = [
+ 'POLICYBODY',
'NAME',
'NUM',
'STRING_LITERAL',
#'LINE_COMMENT', 'BLOCK_COMMENT',
-
'LBRACE', 'RBRACE', 'LBRACK', 'RBRACK',
'LPAR', 'RPAR', 'EQ', 'SEMI', 'DOT',
'ARROW', 'COLON', 'COMMA', 'SLASH',
+ 'DOUBLECOLON',
'STARTTOKEN'
-
] + [k.upper() for k in keywords]
+
+
+ t_POLICYBODY = r'< (.|\n)*? >'
+
literals = '()+-*/=?:,.^|&~!=[]{};<>@%'
t_NUM = r'[+-]?\d+(\.\d+)?'
@@ -42,6 +48,8 @@
t_RBRACE = '}'
t_LBRACK = '\\['
t_RBRACK = '\\]'
+
+
t_LPAR = '\\('
t_RPAR = '\\)'
t_EQ = '='
@@ -53,6 +61,7 @@
t_DOT = '\\.'
t_ignore = ' \t\f'
t_STARTTOKEN = '\\+'
+ t_DOUBLECOLON = '\\:\\:'
def t_NAME(self, t):
'[A-Za-z_$][A-Za-z0-9_+$]*'
@@ -73,45 +82,6 @@
print("Illegal character '{}' ({}) in line {}".format(t.value[0], hex(ord(t.value[0])), t.lexer.lineno))
t.lexer.skip(1)
-class LexHelper:
- offset = 0
- def get_max_linespan(self, p):
- defSpan=[1e60, -1]
- mSpan=[1e60, -1]
- for sp in range(0, len(p)):
- csp = p.linespan(sp)
- if csp[0] == 0 and csp[1] == 0:
- if hasattr(p[sp], "linespan"):
- csp = p[sp].linespan
- else:
- continue
- if csp == None or len(csp) != 2: continue
- if csp[0] == 0 and csp[1] == 0: continue
- if csp[0] < mSpan[0]: mSpan[0] = csp[0]
- if csp[1] > mSpan[1]: mSpan[1] = csp[1]
- if defSpan == mSpan: return (0,0)
- return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
-
- def get_max_lexspan(self, p):
- defSpan=[1e60, -1]
- mSpan=[1e60, -1]
- for sp in range(0, len(p)):
- csp = p.lexspan(sp)
- if csp[0] == 0 and csp[1] == 0:
- if hasattr(p[sp], "lexspan"):
- csp = p[sp].lexspan
- else:
- continue
- if csp == None or len(csp) != 2: continue
- if csp[0] == 0 and csp[1] == 0: continue
- if csp[0] < mSpan[0]: mSpan[0] = csp[0]
- if csp[1] > mSpan[1]: mSpan[1] = csp[1]
- if defSpan == mSpan: return (0,0)
- return tuple([mSpan[0]-self.offset, mSpan[1]-self.offset])
-
- def set_parse_object(self, dst, p):
- dst.setLexData(linespan=self.get_max_linespan(p), lexspan=self.get_max_lexspan(p))
- dst.setLexObj(p)
def srcPort(x):
if (x):
@@ -124,6 +94,8 @@
tokens = ProtobufLexer.tokens
offset = 0
lh = LexHelper()
+ fol_lexer = lex.lex(module=FOLLexer())#, optimize=1)
+ fol_parser = yacc.yacc(module=FOLParser(), start='goal')
def setOffset(self, of):
self.offset = of
@@ -325,6 +297,12 @@
'''enum_body_opt : enum_body'''
p[0] = p[1]
+ def p_policy_definition(self, p):
+ '''policy_definition : POLICY NAME POLICYBODY'''
+ fol = self.fol_parser.parse(p[3], lexer = self.fol_lexer)
+ p[0] = PolicyDefinition(Name(LU.i(p, 2)), fol)
+ self.lh.set_parse_object(p[0], p)
+
# Root of the enum declaration.
# enum_definition ::= 'enum' ident '{' { ident '=' integer ';' }* '}'
def p_enum_definition(self, p):
@@ -446,6 +424,7 @@
'''topLevel : message_definition
| message_extension
| enum_definition
+ | policy_definition
| service_definition
| import_directive
| package_directive