Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1245:5c2555dfce8f

Take advantage of equalities between get_cookie calls

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 18 Apr 2010 13:56:47 -0400
parents	1eedc9086e6c
children	fd4028a594a9

comparison

equal deleted inserted replaced

-:1eedc9086e6c
+:5c2555dfce8f
 datatype node = Node of {Id : int,
 Rep : node ref option ref,
 Cons : node ref SM.map ref,
 Variety : variety,
-Known : bool ref}
+Known : bool ref,
+Ge : Int64.int option ref}
 and variety =
 Dt0 of string
 | Dt1 of string * node ref
 | Prim of Prim.t
 string "}",
 if b then
 box [space,
 string "(complete)"]
 else
-box []]]
+box []],
+if !(#Known (unNode n)) then
+string " (known)"
+else
+box [],
+case !(#Ge (unNode n)) of
+NONE => box []
+| SOME n => string (" (>= " ^ Int64.toString n ^ ")")]
 fun p_database (db : database) =
 box [string "Vars:",
 newline,
 p_list_sep newline (fn (i, n) => box [string ("x" ^ Int.toString i),
 space,
 string "=",
 space,
-p_rep n,
+p_rep n]) (IM.listItemsi (!(#Vars db)))]
-if !(#Known (unNode n)) then
-box [space,
-string "(known)"]
-else
-box []]) (IM.listItemsi (!(#Vars db)))]
 fun repOf (n : representative) : representative =
 case !(#Rep (unNode n)) of
 NONE => n
 | SOME r =>
 let
 val r = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Prim p,
-Known = ref true})
+Known = ref true,
+Ge = ref (case p of
+Prim.Int n => SOME n
+| _ => NONE)})
 in
 #Consts db := CM.insert (!(#Consts db), p, r);
 r
 end)
 | Var n => (case IM.find (!(#Vars db), n) of
 let
 val r = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref false})
+Known = ref false,
+Ge = ref NONE})
 in
 #Vars db := IM.insert (!(#Vars db), n, r);
 r
 end)
 | Lvar _ => raise Undetermined
 let
 val r = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Dt0 f,
-Known = ref true})
+Known = ref true,
+Ge = ref NONE})
 in
 #Con0s db := SM.insert (!(#Con0s db), f, r);
 r
 end)
 | Func (DtCon0 _, _) => raise Fail "Iflow.rep: DtCon0"
 let
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Dt1 (f, r),
-Known = ref (!(#Known (unNode r)))})
+Known = ref (!(#Known (unNode r))),
+Ge = ref NONE})
 in
 #Cons (unNode r) := SM.insert (!(#Cons (unNode r)), f, r');
 r'
 end
 end
 val cons = ref SM.empty
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = cons,
 Variety = Nothing,
-Known = ref (!(#Known (unNode r)))})
+Known = ref (!(#Known (unNode r))),
+Ge = ref NONE})
 val r'' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = #Cons (unNode r),
 Variety = Dt1 (f, r'),
-Known = #Known (unNode r)})
+Known = #Known (unNode r),
+Ge = ref NONE})
 in
 cons := SM.insert (!cons, f, r'');
 #Rep (unNode r) := SOME r'';
 r'
 end
 let
 val r = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref false})
+Known = ref false,
+Ge = ref NONE})
 in
 #Funcs db := ((f, rs), r) :: (!(#Funcs db));
 r
 end
 | SOME (_, r) => repOf r
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Recrd (ref xes, true),
-Known = ref false})
+Known = ref false,
+Ge = ref NONE})
 in
 #Records db := (xes, r') :: (!(#Records db));
 r'
 end
 end
 | NONE => let
 val r = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref (!(#Known (unNode r)))})
+Known = ref (!(#Known (unNode r))),
+Ge = ref NONE})
 in
 xes := SM.insert (!xes, f, r);
 r
 end)
 | Nothing =>
 let
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref (!(#Known (unNode r)))})
+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)})
+Known = #Known (unNode r),
+Ge = ref NONE})
 in
 #Rep (unNode r) := SOME r'';
 r'
 end
 | _ => raise Contradiction
 if !(#Known (unNode r2)) then
 markKnown r1
 else
 ();
 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
+case !(#Ge (unNode r1)) of
+NONE => ()
+| SOME n1 =>
+case !(#Ge (unNode r2)) of
+NONE => #Ge (unNode r2) := SOME n1
+| SOME n2 => #Ge (unNode r2) := SOME (Int64.max (n1, n2));
 compactFuncs ())
 and compactFuncs () =
 let
 let
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Dt0 f,
-Known = ref false})
+Known = ref false,
+Ge = ref NONE})
 in
 #Rep (unNode r) := SOME r';
 #Con0s db := SM.insert (!(#Con0s db), f, r')
 end)
 | _ => raise Contradiction
 let
 val r'' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Nothing,
-Known = ref (!(#Known (unNode r)))})
+Known = ref (!(#Known (unNode r))),
+Ge = ref NONE})
 val r' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
 Cons = ref SM.empty,
 Variety = Dt1 (f, r''),
-Known = #Known (unNode r)})
+Known = #Known (unNode r),
+Ge = ref NONE})
 in
 #Rep (unNode r) := SOME r'
 end
 | _ => raise Contradiction
 end
 | (Eq, [e1, e2]) =>
 markEq (representative (db, e1), representative (db, e2))
+| (Ge, [e1, e2]) =>
+let
+val r1 = representative (db, e1)
+val r2 = representative (db, e2)
+in
+case !(#Ge (unNode (repOf r2))) of
+NONE => ()
+| SOME n2 =>
+case !(#Ge (unNode (repOf r1))) of
+NONE => #Ge (unNode (repOf r1)) := SOME n2
+| SOME n1 => #Ge (unNode (repOf r1)) := SOME (Int64.max (n1, n2))
+end
 | _ => ()
 end
 fun check (db, a) =
 case a of
 val r1 = representative (db, e1)
 val r2 = representative (db, e2)
 in
 repOf r1 = repOf r2
 end
+| (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
+(SOME n1, Prim (Prim.Int n2)) => Int64.>= (n1, n2)
+| _ => false
+end
 | _ => false
 fun builtFrom (db, {UseKnown = uk, Base = bs, Derived = d}) =
 let
 val bs = map (fn b => representative (db, b)) bs
 | Computed of string
 | Binop of Rel * sqexp * sqexp
 | SqKnown of sqexp
 | Inj of Mono.exp
 | SqFunc of string * sqexp
-| Count
+| Unmodeled
 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
 val sqbrel = altL [cmp "=" Eq,
 cmp "<>" Ne,
 constK "MIN",
 constK "MAX",
 constK "SUM",
 constK "AVG"]
+val unmodeled = altL [const "COUNT(*)",
+const "CURRENT_TIMESTAMP"]
 fun sqexp chs =
 log "sqexp"
 (altL [wrap prim SqConst,
 wrap (const "TRUE") (fn () => SqTrue),
 wrap (const "FALSE") (fn () => SqFalse),
 wrap field Field,
 wrap uw_ident Computed,
 wrap known SqKnown,
 wrap func SqFunc,
-wrap (const "COUNT(*)") (fn () => Count),
+wrap unmodeled (fn () => Unmodeled),
 wrap sqlify Inj,
 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
 (follow (keep (fn ch => ch <> #")")) (const ")")))))
 (fn ((), (e, _)) => e),
 wrap (follow (ws (const "("))
 val allowUpdate : atom list -> unit
 val update : ErrorMsg.span -> unit
 val havocReln : reln -> unit
+val havocCookie : string -> unit
 val debug : unit -> unit
 end = struct
 val hnames = ref 1
 in
 tryAll unifs hyps
 end
 | (g as AReln (r, es)) :: goals =>
 (complete ();
-Cc.check (db, AReln (r, map (simplify unifs) es))
+(if Cc.check (db, AReln (r, map (simplify unifs) es)) then
+true
+else
+((*Print.preface ("Fail", p_atom (AReln (r, map (simplify unifs) es)));*)
+false))
 andalso checkGoals goals unifs)
 | ACond _ :: _ => false
 in
 checkGoals goals IM.empty
 end
 else
 let
 val (_, hs, _) = !hyps
 in
 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
-Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs),
+Print.prefaces "Situation" [("User learns", p_exp e),
-("User learns", p_exp e)(*,
+("Hypotheses", Print.p_list p_atom hs)(*,
 ("E-graph", Cc.p_database db)*)]
 end
 end
 fun checkPaths () =
 else
 let
 val (_, hs, _) = !hyps
 in
 ErrorMsg.errorAt loc "The database update policy may be violated here.";
-Print.preface ("Hypotheses", Print.p_list p_atom hs)
+Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
+("E-graph", Cc.p_database db)*)]
 end
 end
 val insertable = ref ([] : atom list list)
 fun allowInsert v = insertable := v :: !insertable
 val n = !hnames
 val (_, hs, _) = !hyps
 in
 hnames := n + 1;
 hyps := (n, List.filter (fn AReln (r', _) => r' <> r | _ => true) hs, ref false)
+end
+fun havocCookie cname =
+let
+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)
 end
 fun debug () =
 let
 val (_, hs, _) = !hyps
 | SqFunc (f, e) =>
 (case expIn e of
 inl e => inl (Func (Other f, [e]))
 | _ => default ())
-| Count => default ()
+| Unmodeled => default ()
 end
 in
 expIn
 end
 (case deinj (#Env arg) e of
 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
 [])
 | SOME e => [(true, e)])
 | SqFunc (_, e) => usedFields e
-| Count => []
+| Unmodeled => []
 fun doUsed () = case #Where r of
 NONE => ()
 | SOME e =>
 app (#UsedExp arg) (usedFields e)
 fun doFfi (m, s, es) =
 if m = "Basis" andalso SS.member (writers, s) then
 let
 fun doArgs es =
 case es of
-[] => k (Recd [])
+[] =>
+(if s = "set_cookie" then
+case es of
+[_, cname, _, _, _] =>
+(case #1 cname of
+EPrim (Prim.String cname) =>
+St.havocCookie cname
+| _ => ())
+| _ => ()
+else
+();
+k (Recd []))
 | e :: es =>
 evalExp env e (fn e => (St.send true (e, loc); doArgs es))
 in
 doArgs es
 end
 | ESetval _ => default ()
 | 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])];
+St.assert [AReln (Known, [e]), AReln (Eq, [e, e'])];
 k e
 end
 | EUnurlify _ => default ()
 | EJavaScript _ => default ()

Mercurial > urweb

comparison src/iflow.sml @ 1245:5c2555dfce8f