Skip to content

Commit

Permalink
started figuring out what is wrong
Browse files Browse the repository at this point in the history
  • Loading branch information
jeanqasaur committed Jun 13, 2016
1 parent c33e013 commit 93fa0f5
Show file tree
Hide file tree
Showing 5 changed files with 152 additions and 21 deletions.
16 changes: 16 additions & 0 deletions JeevesLib.py
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,22 @@ def clear_cache():
def get_cache():
return jeevesState.concretecache.cache

def get_solverstate():
return jeevesState.solverstate


'''
Early concretization optimization.
'''
def set_viewer(viewer):
jeevesState.set_viewer(viewer)
jeevesState.reset_solverstate(viewer)
def clear_viewer():
jeevesState.reset_viewer()
jeevesState.clear_solverstate()
def get_viewer():
return jeevesState.viewer

class PositiveVariable:
def __init__(self, var):
self.var = var
Expand Down
3 changes: 3 additions & 0 deletions demo/conf/conf/views.py
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@
import logging

def register_account(request):
JeevesLib.clear_viewer()

if request.user.is_authenticated():
return HttpResponseRedirect("index")

Expand Down Expand Up @@ -123,6 +125,7 @@ def about_view(request):
@jeeves
def papers_view(request):
user = UserProfile.objects.get(username=request.user.username)
JeevesLib.set_viewer(user)

# TODO: Figure out why we can't loop over this if we don't concretize it...
papers = Paper.objects.all()
Expand Down
72 changes: 71 additions & 1 deletion env/PolicyEnv.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

import fast.AST
from collections import defaultdict
from fast.AST import FExpr
from fast.AST import Constant, FExpr

from smt.Z3 import Z3
from weakref import WeakKeyDictionary
Expand All @@ -24,6 +24,65 @@ def __init__(self, policies, ctxt):
self.policies = policies
# self.policies_index = 0

def getLabelClosure(self, varsNeeded):
for label in varsNeeded:
if self.policies.has_key(label):
policy = self.policies[label]

varsNeeded = varsNeeded.union(policy(self.ctxt).vars())
return varsNeeded

def solvePolicies(self, varsNeeded, pathenv):
assignedVars = True
constraints = []

# Get relevant policies.
for label in varsNeeded:
assignedVar = False
# If there are policies associated with the label.
if self.policies.has_key(label):
policy = self.policies[label]

#predicate should be True if label can be HIGH
print "EVALUATING PREDICATE FOR ", label
predicate = policy(self.ctxt).partialEval(pathenv)
constraint = fast.AST.Implies(
label, predicate).partialEval(pathenv)

# If the predicate is a constant, this means there are no
# dependencies on other labels so we can simply evaluate the
# policy.
if predicate.type != bool:
raise ValueError("constraints must be bools")
if isinstance(predicate, Constant):
if not predicate.v:
self.result[label] = False
else:
self.result[label] = True
assignedVar = True

constraints.append(constraint)
else:
print "NO POLICY FOR ", label
assignedVars = assignedVars and assignedVar

if not assignedVars:
for constraint in constraints:
self.solver.boolExprAssert(constraint)

for var in varsNeeded:
if var not in self.result:
self.solver.push()
self.solver.boolExprAssert(var)
if self.solver.isSatisfiable():
self.result[var] = True
else:
self.solver.pop()
self.solver.boolExprAssert(fast.AST.Not(var))
self.result[var] = False

assert self.solver.check()

def concretizeExp(self, f, pathenv):
"""
Expression concretization.
Expand Down Expand Up @@ -77,6 +136,17 @@ def concretizeExp(self, f, pathenv):

return f.eval(self.result)

def assignLabel(self, label, pathenv):
if label in self.result:
return self.result[label]
else:
varsNeeded = self.getLabelClosure({label})
self.solvePolicies(varsNeeded, pathenv)

JeevesLib.log_counts(len(varsNeeded))

return self.result[label]

class PolicyEnv:
def __init__(self):
self.policies = WeakKeyDictionary()
Expand Down
55 changes: 42 additions & 13 deletions fast/AST.py
Original file line number Diff line number Diff line change
Expand Up @@ -50,23 +50,27 @@ def __init__(self):
pass

def init(self):
# Cache of concretized values.
self._concretecache = defaultdict(env.ConcreteCache.ConcreteCache)
# Cache of concretized values.
self._concretecache = defaultdict(env.ConcreteCache.ConcreteCache)

# Regular environments.
self._varenv = defaultdict(env.VarEnv.VarEnv)
self._pathenv = defaultdict(env.PathVars.PathVars)
self._policyenv = defaultdict(env.PolicyEnv.PolicyEnv)
self._writeenv = defaultdict(env.WritePolicyEnv.WritePolicyEnv)
self._all_labels = defaultdict(dict)
# Regular environments.
self._varenv = defaultdict(env.VarEnv.VarEnv)
self._pathenv = defaultdict(env.PathVars.PathVars)
self._policyenv = defaultdict(env.PolicyEnv.PolicyEnv)
self._writeenv = defaultdict(env.WritePolicyEnv.WritePolicyEnv)
self._all_labels = defaultdict(dict)

self._solverstate = defaultdict()

# Logging.
self._log_policies = False
self._policy_log_filehandle = None
self._log_policies = False
self._policy_log_filehandle = None

self._num_concretize = 0
self._num_labels = 0
# self._num_policies = 0
self._num_concretize = 0
self._num_labels = 0

# Early concretization optimization.
self._viewer = defaultdict(FNull)

@property
def concretecache(self):
Expand Down Expand Up @@ -134,6 +138,26 @@ def writeenv(self):
def all_labels(self):
return self._all_labels[threading.current_thread()]

@property
def solverstate(self):
if self._solverstate.has_key(threading.current_thread()):
return self._solverstate[threading.current_thread()]
else:
return None
def reset_solverstate(self, ctxt):
self._solverstate[threading.current_thread()] = \
env.PolicyEnv.SolverState(self.policyenv.policies, ctxt)
def clear_solverstate(self):
self._solverstate[threading.current_thread()] = None

@property
def viewer(self):
return self._viewer[threading.current_thread()]
def set_viewer(self, viewer):
self._viewer[threading.current_thread()] = viewer
def reset_viewer(self):
self._viewer[threading.current_thread()] = FNull()

jeevesState = JeevesState()

'''
Expand Down Expand Up @@ -962,6 +986,11 @@ def prettyPrint(self, indent=""):
def __getstate__(self):
return "(FObject(%s):%s)" % (id(self.v), self.v.__getstate__())

class FNull(FExpr):
def __init__(self):
pass


"""
def __and__(l, r):
def __rand__(r, l):
Expand Down
27 changes: 20 additions & 7 deletions jeevesdb/JeevesModel.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

import JeevesLib
from JeevesLib import fexpr_cast
from fast.AST import Facet, FObject, Unassigned, FExpr
from fast.AST import Facet, FObject, Unassigned, FExpr, FNull
import JeevesModelUtils

class JeevesQuerySet(QuerySet):
Expand Down Expand Up @@ -62,17 +62,30 @@ def get(self, use_base_env=False, **kwargs):
raise Exception("wow such error: \
get() found rows for more than one jeeves_id")

viewer = JeevesLib.get_viewer()
has_viewer = not isinstance(viewer, FNull)

pathenv = JeevesLib.jeevesState.pathenv.getEnv()
solverstate = JeevesLib.get_solverstate()

cur = None
for (row, conditions) in matches:
old = cur
cur = FObject(row)
for var_name, val in conditions.iteritems():
if val:
cur = Facet(acquire_label_by_name(
self.model._meta.app_label, var_name), cur, old)
else:
cur = Facet(acquire_label_by_name(
self.model._meta.app_label, var_name), old, cur)
label = acquire_label_by_name(self.model._meta.app_label, var_name)
if has_viewer:
if solverstate.assignLabel(label, pathenv):
if not val:
cur = old
else:
if val:
cur = old
else:
if val:
cur = Facet(label, cur, old)
else:
cur = Facet(label, old, cur)
try:
return cur.partialEval({} if use_base_env \
else JeevesLib.jeevesState.pathenv.getEnv())
Expand Down

0 comments on commit 93fa0f5

Please sign in to comment.