Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1216:09caa8c780e5

Some serious debugging of the new Cc

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 08 Apr 2010 14:20:46 -0400
parents	360f1ed0a969
children	4d206e603300

comparison

equal deleted inserted replaced

-:360f1ed0a969
+:09caa8c780e5
 | NONE =>
 let
 val r' = ref (Node {Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Dt1 (f, r),
-Known = ref false})
+Known = #Known (unNode r)})
 in
 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
 r'
 end
 end
 let
 val cons = ref SM.empty
 val r' = ref (Node {Rep = ref NONE,
 Cons = cons,
 Variety = Nothing,
-Known = ref false})
+Known = #Known (unNode r)})
 val r'' = ref (Node {Rep = ref NONE,
 Cons = #Cons (unNode r),
 Variety = Dt1 (f, r'),
 Known = #Known (unNode r)})
 in
 case #Variety (unNode r) of
 Recrd xes =>
 (case SM.find (!xes, f) of
 SOME r => repOf r
-| NONE =>let
+| NONE => let
 val r = ref (Node {Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref false})
+Known = #Known (unNode r)})
 in
 xes := SM.insert (!xes, f, r);
 r
 end)
 | Nothing =>
 let
 val r' = ref (Node {Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref false})
+Known = #Known (unNode r)})
 val r'' = ref (Node {Rep = ref NONE,
 Cons = #Cons (unNode r),
 Variety = Recrd (ref (SM.insert (SM.empty, f, r'))),
 Known = #Known (unNode r)})
 decomp
 end
 fun imply (p1, p2) =
 (reset ();
+(*Print.prefaces "Bigger go" [("p1", p_prop p1),
+("p2", p_prop p2)];*)
 decomp true (fn (e1, e2) => e1 andalso e2 ()) p1
 (fn hyps =>
 decomp false (fn (e1, e2) => e1 orelse e2 ()) p2
 (fn goals =>
 let
 ("hyps", Print.p_list p_atom hyps),
 ("db", Cc.p_database cc)];*)
 false)) acc
 orelse onFail ())
 handle Cc.Contradiction => onFail ()
-end handle Cc.Undetermined => onFail ())
+end handle Cc.Undetermined => ((*print "Undetermined\n";*) onFail ()))
-| AReln (Sql gf, [ge]) :: goals =>
+| (g as AReln (Sql gf, [ge])) :: goals =>
 let
 fun hps hyps =
 case hyps of
-[] => onFail ()
+[] => gls goals onFail (g :: acc)
 | AReln (Sql hf, [he]) :: hyps =>
 if gf = hf then
 let
 val saved = save ()
 in
 in
 hps hyps
 end
 | g :: goals => gls goals onFail (g :: acc)
 in
+(*Print.prefaces "Big go" [("hyps", Print.p_list p_atom hyps),
+("goals", Print.p_list p_atom goals)];*)
 gls goals (fn () => false) []
 end handle Cc.Contradiction => true)))
 fun patCon pc =
 case pc of
 datatype queryMode =
 SomeCol of exp
 | AllCols of exp
+exception Default
 fun queryProp env rvN rv oe e =
-case parse query e of
+let
-NONE => (print ("Warning: Information flow checker can't parse SQL query at "
+fun default () = (print ("Warning: Information flow checker can't parse SQL query at "
 ^ ErrorMsg.spanToString (#2 e) ^ "\n");
-(rvN, Var 0, Unknown, []))
+(rvN, Unknown, []))
-| SOME r =>
+in
-let
+case parse query e of
-val (rvN, count) = rv rvN
+NONE => default ()
+| SOME r =>
-val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
+let
-let
+val (rvs, rvN) = ListUtil.foldlMap (fn ((_, v), rvN) =>
-val (rvN, e) = rv rvN
+let
-in
+val (rvN, e) = rv rvN
-((v, e), rvN)
+in
-end) rvN (#From r)
+((v, e), rvN)
+end) rvN (#From r)
-fun rvOf v =
-case List.find (fn (v', _) => v' = v) rvs of
+fun rvOf v =
-NONE => raise Fail "Iflow.queryProp: Bad table variable"
+case List.find (fn (v', _) => v' = v) rvs of
-| SOME (_, e) => e
+NONE => raise Fail "Iflow.queryProp: Bad table variable"
+| SOME (_, e) => e
-fun usedFields e =
-case e of
+fun usedFields e =
-SqConst _ => []
+case e of
-| Field (v, f) => [(v, f)]
+SqConst _ => []
-| Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
+| Field (v, f) => [(v, f)]
-| SqKnown _ => []
+| Binop (_, e1, e2) => removeDups (usedFields e1 @ usedFields e2)
-| Inj _ => []
+| SqKnown _ => []
-| SqFunc (_, e) => usedFields e
+| Inj _ => []
-| Count => []
+| SqFunc (_, e) => usedFields e
+| Count => []
-val p =
-foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
+val p =
+foldl (fn ((t, v), p) => And (p, Reln (Sql t, [rvOf v]))) True (#From r)
-fun expIn e =
-case e of
+fun expIn e =
-SqConst p => inl (Const p)
+case e of
-| Field (v, f) => inl (Proj (rvOf v, f))
+SqConst p => inl (Const p)
-| Binop (bo, e1, e2) =>
+| Field (v, f) => inl (Proj (rvOf v, f))
-inr (case (bo, expIn e1, expIn e2) of
+| Binop (bo, e1, e2) =>
-(Exps f, inl e1, inl e2) => f (e1, e2)
+inr (case (bo, expIn e1, expIn e2) of
-| (Props f, inr p1, inr p2) => f (p1, p2)
+(Exps f, inl e1, inl e2) => f (e1, e2)
-| _ => Unknown)
+| (Props f, inr p1, inr p2) => f (p1, p2)
-| SqKnown e =>
+| _ => Unknown)
-inr (case expIn e of
+| SqKnown e =>
-inl e => Reln (Known, [e])
+inr (case expIn e of
-| _ => Unknown)
+inl e => Reln (Known, [e])
-| Inj e =>
+| _ => Unknown)
-let
+| Inj e =>
-fun deinj (e, _) =
+let
-case e of
+fun deinj (e, _) =
-ERel n => List.nth (env, n)
+case e of
-| EField (e, f) => Proj (deinj e, f)
+ERel n => List.nth (env, n)
-| _ => raise Fail "Iflow: non-variable injected into query"
+| EField (e, f) => Proj (deinj e, f)
-in
+| _ => raise Fail "Iflow: non-variable injected into query"
-inl (deinj e)
+in
-end
+inl (deinj e)
-| SqFunc (f, e) =>
+end
-inl (case expIn e of
+| SqFunc (f, e) =>
-inl e => Func (Other f, [e])
+inl (case expIn e of
-| _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
+inl e => Func (Other f, [e])
-| Count => inl count
+| _ => raise Fail ("Iflow: non-expresion passed to function " ^ f))
+| Count => raise Default
-val p = case #Where r of
-NONE => p
+val p = case #Where r of
-| SOME e =>
+NONE => p
-case expIn e of
+| SOME e =>
-inr p' => And (p, p')
+case expIn e of
-| _ => p
+inr p' => And (p, p')
-in
+| _ => p
-(rvN,
-count,
+fun normal () =
-And (p, case oe of
+(rvN,
-SomeCol oe =>
+And (p, case oe of
-foldl (fn (si, p) =>
+SomeCol oe =>
-let
+foldl (fn (si, p) =>
-val p' = case si of
+let
-SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
+val p' = case si of
-| SqExp (e, f) =>
+SqField (v, f) => Reln (Eq, [oe, Proj (rvOf v, f)])
-case expIn e of
+| SqExp (e, f) =>
-inr _ => Unknown
+case expIn e of
-| inl e => Reln (Eq, [oe, e])
+inr _ => Unknown
-in
+| inl e => Reln (Eq, [oe, e])
-Or (p, p')
+in
-end)
+Or (p, p')
-False (#Select r)
+end)
-| AllCols oe =>
+False (#Select r)
-foldl (fn (si, p) =>
+| AllCols oe =>
-let
+foldl (fn (si, p) =>
-val p' = case si of
+let
-SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
+val p' = case si of
-Proj (rvOf v, f)])
+SqField (v, f) => Reln (Eq, [Proj (Proj (oe, v), f),
-| SqExp (e, f) =>
+Proj (rvOf v, f)])
-case expIn e of
+| SqExp (e, f) =>
-inr p => Cond (Proj (oe, f), p)
+case expIn e of
-| inl e => Reln (Eq, [Proj (oe, f), e])
+inr p => Cond (Proj (oe, f), p)
-in
+| inl e => Reln (Eq, [Proj (oe, f), e])
-And (p, p')
+in
-end)
+And (p, p')
-True (#Select r)),
+end)
+True (#Select r)),
 case #Where r of
 NONE => []
 | SOME e => map (fn (v, f) => Proj (rvOf v, f)) (usedFields e))
-end
+in
+case #Select r of
+[SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
+(case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
+Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
+let
+val oe = case oe of
+SomeCol oe => oe
+| AllCols oe => Proj (oe, f)
+in
+(rvN,
+Or (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.False", [])]),
+And (Reln (Eq, [oe, Func (DtCon0 "Basis.bool.True", [])]),
+p)),
+[])
+end
+| _ => normal ())
+| _ => normal ()
+end
+handle Default => default ()
+end
 fun evalPat env e (pt, _) =
 case pt of
 PWild => (env, True)
 | PVar _ => (e :: env, True)
 val st = foldl (fn ((pt, pe), st) =>
 let
 val (env, pp) = evalPat env e pt
 val (pe, st') = evalExp env (pe, (#1 st, And (orig, pp), #3 st))
+(*val () = Print.prefaces "Case" [("loc", Print.PD.string
+(ErrorMsg.spanToString (#2 pt))),
+("env", Print.p_list p_exp env),
+("sent", Print.p_list_sep Print.PD.newline
+(fn (loc, e, p) =>
+Print.box [Print.PD.string
+(ErrorMsg.spanToString loc),
+Print.PD.string ":",
+Print.space,
+p_exp e,
+Print.space,
+Print.PD.string "in",
+Print.space,
+p_prop p])
+(List.take (#3 st', length (#3 st')
+- length (#3 st))))]*)
 val this = And (removeRedundant orig (#2 st'), Reln (Eq, [Var r, pe]))
 in
 (#1 st', Or (#2 st, this), #3 st')
 end) (#1 st, False, #3 st) pes
 val acc = #1 st + 1
 val st' = (#1 st + 2, #2 st, #3 st)
 val (b, st') = evalExp (Var acc :: Var r :: env) (b, st')
-val (rvN, count, qp, used) =
+val (rvN, qp, used) =
 queryProp env
 (#1 st') (fn rvN => (rvN + 1, Var rvN))
 (AllCols (Var r)) q
 val p' = And (qp, #2 st')
 let
 val out = rvN
 val p = Or (Reln (Eq, [Var out, i]),
 And (Reln (Eq, [Var out, b]),
-And (Reln (Gt, [count,
+p'))
-Const (Prim.Int 0)]),
-p')))
 in
 (out + 1, p, Var out)
 end
 val sent = map (fn (loc, e, p) => (loc, e, And (qp, p))) (#3 st')
 let
 val file = MonoReduce.reduce file
 val file = MonoOpt.optimize file
 val file = Fuse.fuse file
 val file = MonoOpt.optimize file
+val file = MonoShake.shake file
 (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*)
 val exptd = foldl (fn ((d, _), exptd) =>
 case d of
 DExport (_, _, n, _, _, _) => IS.add (exptd, n)
 val (e, (_, p, sent)) = evalExp env (e, (nv, p, []))
 in
 (sent @ vals, pols)
 end
-| DPolicy (PolClient e) => (vals, #3 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
+| DPolicy (PolClient e) => (vals, #2 (queryProp [] 0 (fn rvN => (rvN + 1, Lvar rvN))
 (SomeCol (Var 0)) e) :: pols)
 | _ => (vals, pols)
 val () = reset ()
 else
 false) pols then
 ()
 else
 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
-Print.preface ("The state satisifes this predicate:", p_prop p))
+Print.preface ("The state satisifies this predicate:", p_prop p))
 end
 fun doAll e =
 case e of
 Const _ => ()
 | Var _ => doOne e
 | Lvar _ => raise Fail "Iflow.doAll: Lvar"
-| Func (UnCon _, [e]) => doOne e
+| Func (UnCon _, [_]) => doOne e
 | Func (_, es) => app doAll es
 | Recd xes => app (doAll o #2) xes
 | Proj _ => doOne e
 | Finish => ()
 in

Mercurial > urweb

comparison src/iflow.sml @ 1216:09caa8c780e5