Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 2216:70ec9bb337be

Progress towards invalidation based on equalities of fields.

author	Ziv Scully <ziv@mit.edu>
date	Mon, 10 Nov 2014 22:04:40 -0500
parents	4d64af730e35
children	278e10629ba1

comparison

equal deleted inserted replaced

-:639e62ca2530
+:70ec9bb337be
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 p_list p_exp es,
 string ")"]
 | PCon1 s => box [string (s ^ "("),
 p_list p_exp es,
 string ")"]
-| Eq => p_bop "=" es
+| Cmp Eq => p_bop "=" es
-| Ne => p_bop "<>" es
+| Cmp Ne => p_bop "<>" es
-| Lt => p_bop "<" es
+| Cmp Lt => p_bop "<" es
-| Le => p_bop "<=" es
+| Cmp Le => p_bop "<=" es
-| Gt => p_bop ">" es
+| Cmp Gt => p_bop ">" es
-| Ge => p_bop ">=" es
+| Cmp Ge => p_bop ">=" es
 fun p_prop p =
 case p of
 True => string "True"
 | False => string "False"
 | Unknown => string "??"
-| And (p1, p2) => box [string "(",
+| Lop (And, p1, p2) => box [string "(",
 p_prop p1,
 string ")",
 space,
 string "&&",
 space,
 string "(",
 p_prop p2,
 string ")"]
-| Or (p1, p2) => box [string "(",
+| Lop (Or, p1, p2) => box [string "(",
 p_prop p1,
 string ")",
 space,
 string "||",
 space,
 string "(",
 p_prop p2,
 string ")"]
 | Reln (r, es) => p_reln r es
 | Cond (e, p) => box [string "(",
 p_exp e,
 space,
 string "==",
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
 Known = ref (!(#Known (unNode r))),
 Ge = ref NONE})
 val r'' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = #Cons (unNode r),
 Variety = Recrd (ref (SM.insert (SM.empty, f, r')), false),
 Known = #Known (unNode r),
 Ge = ref NONE})
 in
 #Rep (unNode r) := SOME r'';
 r'
 end
 | _ => raise Contradiction
 end
 in
 rep e
 end
 cons := SM.insert (!cons, f, r');
 #Rep (unNode r) := SOME r'
 end
 | _ => raise Contradiction
 end
-| (Eq, [e1, e2]) =>
+| (Cmp Eq, [e1, e2]) =>
 markEq (representative (db, e1), representative (db, e2))
-| (Ge, [e1, e2]) =>
+| (Cmp Ge, [e1, e2]) =>
 let
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 case !(#Ge (unNode (repOf r2))) of
 | _ => false)
 | (PCon1 f, [e]) =>
 (case #Variety (unNode (representative (db, e))) of
 Dt1 (f', _) => f' = f
 | _ => false)
-| (Eq, [e1, e2]) =>
+| (Cmp Eq, [e1, e2]) =>
 let
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 repOf r1 = repOf r2
 end
-| (Ge, [e1, e2]) =>
+| (Cmp Ge, [e1, e2]) =>
 let
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 case (!(#Ge (unNode (repOf r1))), #Variety (unNode (repOf r2))) of
 ()
 else
 (hyps := (n', hs, ref false);
 Cc.clear db;
 app (fn a => Cc.assert (db, a)) hs)
 end
 fun useKeys () =
 let
 val changed = ref false
 if tab' = tab andalso
 List.exists (List.all (fn f =>
 let
 val r =
 Cc.check (db,
-AReln (Eq, [Proj (r1, f),
+AReln (Cmp Eq, [Proj (r1, f),
 Proj (r2, f)]))
 in
 (*Print.prefaces "Fs"
 [("tab",
 Print.PD.string tab),
 Print.PD.string
 (Bool.toString r))];*)
 r
 end)) ks then
 (changed := true;
-Cc.assert (db, AReln (Eq, [r1, r2]));
+Cc.assert (db, AReln (Cmp Eq, [r1, r2]));
 finder (hyps, acc))
 else
 finder (hyps, a :: acc)
 | a :: hyps => finder (hyps, a :: acc)
 val cname = "cookie/" ^ cname
 val n = !hnames
 val (_, hs, _) = !hyps
 in
 hnames := n + 1;
-hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
+hyps := (n, List.filter (fn AReln (Cmp Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
 end
 fun check a = Cc.check (db, a)
 fun debug () =
 | x :: ls =>
 let
 val ls = removeDups ls
 in
 if List.exists (fn x' => x' = x) ls then
 ls
 else
 x :: ls
 end
 fun deinj env e =
 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
 | Null => inl (Func (DtCon0 "None", []))
 | SqNot e =>
 inr (case expIn e of
-inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
+inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
 | inr _ => Unknown)
 | Field (v, f) => inl (Proj (rvOf v, f))
 | Computed _ => default ()
 | Binop (bo, e1, e2) =>
 let
 val e1 = expIn e1
 val e2 = expIn e2
 in
 inr (case (bo, e1, e2) of
-(Exps f, inl e1, inl e2) => f (e1, e2)
+(RCmp c, inl e1, inl e2) => Reln (Cmp c, [e1, e2])
-| (Props f, v1, v2) =>
+| (RLop l, v1, v2) =>
 let
 fun pin v =
 case v of
-inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
 | inr p => p
 in
-f (pin v1, pin v2)
+Lop (l, pin v1, pin v2)
 end
 | _ => Unknown)
 end
 | SqKnown e =>
 (case expIn e of
 | SOME e => e)
 | SqFunc (f, e) =>
 (case expIn e of
 inl e => inl (Func (Other f, [e]))
 | _ => default ())
 | Unmodeled => inl (Func (Other "allow", [rv ()]))
 end
 in
 expIn
 end
 fun go p k =
 case p of
 True => (k () handle Cc.Contradiction => ())
 | False => ()
 | Unknown => ()
-| And (p1, p2) => go p1 (fn () => go p2 k)
+| Lop (And, p1, p2) => go p1 (fn () => go p2 k)
-| Or (p1, p2) =>
+| Lop (Or, p1, p2) =>
 let
 val saved = save ()
 in
 go p1 k;
 restore saved;
 case #Where r of
 NONE => final ()
 | SOME e =>
 let
 val p = case expIn e of
-inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
+inl e => Reln (Cmp Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
 | inr p => p
 val saved = #Save arg ()
 in
 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
 handle Cc.Contradiction => ()
 fun normal () = doWhere normal'
 in
 (case #Select r of
-[SqExp (Binop (Exps bo, Count, SqConst (Prim.Int 0)), f)] =>
+[SqExp (Binop (RCmp bo, Count, SqConst (Prim.Int 0)), f)] =>
-(case bo (Const (Prim.Int 1), Const (Prim.Int 2)) of
+(case bo of
-Reln (Gt, [Const (Prim.Int 1), Const (Prim.Int 2)]) =>
+Gt =>
 (case #Cont arg of
 SomeCol _ => ()
 | AllCols k =>
 let
 fun answer e = k (Recd [(f, e)])
 [] => k (Func (Other (m ^ "." ^ s), rev acc))
 | (e, _) :: es =>
 evalExp env e (fn e => doArgs (es, e :: acc))
 in
 doArgs (es, [])
 end
 in
 case #1 e of
 EPrim p => k (Const p)
 | ERel n => k (List.nth (env, n))
 | ENamed _ => default ()
 fun doArgs (args, modes, env') =
 case (args, modes) of
 ([], []) => (evalExp env' (#body rf) (fn _ => ());
 St.reinstate saved;
 default ())
 | (arg :: args, mode :: modes) =>
 evalExp env arg (fn arg =>
 let
 val v = case mode of
 Arbitrary => Var (St.nextVar ())
 NextVar = Var o St.nextVar,
 Add = fn a => St.assert [a],
 Save = St.stash,
 Restore = St.reinstate,
 Cont = AllCols (fn x =>
-(St.assert [AReln (Eq, [r, x])];
+(St.assert [AReln (Cmp Eq, [r, x])];
 evalExp (acc :: r :: env) b k))} q
 end)
 | EDml (e, _) =>
 (case parse dml e of
 NONE => (print ("Warning: Information flow checker can't parse DML command at "
 k (Recd [])
 end
 | Delete (tab, e) =>
 let
 val old = St.nextVar ()
 val expIn = expIn (Var o St.nextVar) env
 (fn "T" => Var old
 | _ => raise Fail "Iflow.evalExp: Bad field expression in DELETE")
 val p = case expIn e of
 inl e => raise Fail "Iflow.evalExp: DELETE with non-boolean"
 | inr p => p
 val saved = St.stash ()
 in
 St.assert [AReln (Sql (tab ^ "$Old"), [Var old]),
 AReln (Sql (tab), [Var old])];
 decomp {Save = St.stash,
 fs
 else
 (f, Proj (Var old, f)) :: fs) fs fs'
 val p = case expIn e of
 inl e => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
 | inr p => p
 val saved = St.stash ()
 in
 St.assert [AReln (Sql (tab ^ "$New"), [Recd fs]),
 AReln (Sql (tab ^ "$Old"), [Var old]),
 St.reinstate saved;
 St.havocReln (Sql tab);
 k (Recd []))
 handle Cc.Contradiction => ())
 end)
 | ENextval (EPrim (Prim.String (_, seq)), _) =>
 let
 val nv = St.nextVar ()
 in
 St.assert [AReln (Sql (String.extract (seq, 3, NONE)), [Var nv])];
 | EUnurlify ((EFfiApp ("Basis", "get_cookie", [((EPrim (Prim.String (_, cname)), _), _)]), _), _, _) =>
 let
 val e = Var (St.nextVar ())
 val e' = Func (Other ("cookie/" ^ cname), [])
 in
-St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
+St.assert [AReln (Known, [e]), AReln (Cmp Eq, [e, e'])];
 k e
 end
 | EUnurlify _ => default ()
 | EJavaScript _ => default ()
 in
 St.allowSend ([p], outs)
 end
 | _ => ())
 end
 | _ => ()
 in
 app decl (#1 file)
 end

Mercurial > urweb

comparison src/iflow.sml @ 2216:70ec9bb337be