Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1229:a2cd6664f57f

sendOwnIds policies

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 11 Apr 2010 17:55:37 -0400
parents	7dfa67560916
children	8768145eed1e

comparison

equal deleted inserted replaced

-:7dfa67560916
+:a2cd6664f57f
 type database = {Vars : representative IM.map ref,
 Consts : representative CM.map ref,
 Con0s : representative SM.map ref,
 Records : (representative SM.map * representative) list ref,
-Funcs : ((string * representative list) * representative) list ref }
+Funcs : ((string * representative list) * representative) list ref}
 fun database () = {Vars = ref IM.empty,
 Consts = ref CM.empty,
 Con0s = ref SM.empty,
 Records = ref [],
 if !(#Known (unNode r2)) then
 markKnown r1
 else
 ();
 #Cons (unNode r2) := SM.unionWith #1 (!(#Cons (unNode r2)), !(#Cons (unNode r1)));
 compactFuncs ())
 and compactFuncs () =
 let
 fun loop funcs =
 let
 fun expIn (e, rvN) =
 let
 fun default () =
 let
-val (rvN, e) = rv rvN
+val (rvN, e') = rv rvN
 in
-(inl e, rvN)
+(inl e', rvN)
 end
 in
 case e of
 SqConst p => (inl (Const p), rvN)
 | Field (v, f) => (inl (Proj (rvOf v, f)), rvN)
 val p =
 foldl (fn ((t, v), p) =>
 let
 val t =
 case v of
-"New" => "$New"
+"New" => t ^ "$New"
 | _ => t
 in
 And (p, Reln (Sql t, [rvOf v]))
 end) True (#From r)
 val p =
 foldl (fn ((t, v), p) =>
 let
 val t =
 case v of
-"New" => "$New"
+"New" => t ^ "$New"
 | _ => t
 in
 And (p, Reln (Sql t, [rvOf v]))
 end) True (#From r)
 let
 fun default () =
 let
 val (st, nv) = St.nextVar st
 in
+(*Print.prefaces "default" [("e", MonoPrint.p_exp MonoEnv.empty e),
+("nv", p_exp (Var nv))];*)
 (Var nv, st)
 end
 fun addSent (p, e, st) =
 let
 ((x, e), st)
 end)
 st es
 in
 (Recd [], St.addInsert (st, (loc, And (St.ambient st,
-Reln (Sql "$New", [Recd es])))))
+Reln (Sql (tab ^ "$New"), [Recd es])))))
 end
 | Delete (tab, e) =>
 let
 val (st, old) = St.nextVar st
 val (p, st) = case expIn (e, st) of
 (inl e, _) => raise Fail "Iflow.evalExp: UPDATE with non-boolean"
 | (inr p, st) => (p, st)
 val p = And (p,
-And (Reln (Sql "$New", [Recd fs]),
+And (Reln (Sql (tab ^ "$New"), [Recd fs]),
 And (Reln (Sql "$Old", [Var old]),
 Reln (Sql tab, [Var old]))))
 in
 (Recd [], St.addUpdate (st, (loc, And (St.ambient st, p))))
 end)
+| ENextval (EPrim (Prim.String seq), _) =>
+let
+val (st, nv) = St.nextVar st
+in
+(Var nv, St.setAmbient (st, And (St.ambient st, Reln (Sql (String.extract (seq, 3, NONE)), [Var nv]))))
+end
 | ENextval _ => default ()
 | ESetval _ => default ()
 | EUnurlify ((EFfiApp ("Basis", "get_cookie", _), _), _, _) =>
 let
 let
 val p = updateProp 0 rv e
 in
 (vals, inserts, deletes, updates, client, insert, delete, p :: update)
 end
+| PolSequence e =>
+(case #1 e of
+EPrim (Prim.String seq) =>
+let
+val p = Reln (Sql (String.extract (seq, 3, NONE)), [Lvar 0])
+val outs = [Lvar 0]
+in
+(vals, inserts, deletes, updates, (p, outs) :: client, insert, delete, update)
+end
+| _ => (vals, inserts, deletes, updates, client, insert, delete, update))
 end
 | _ => (vals, inserts, deletes, updates, client, insert, delete, update)
 val () = reset ()
 fun doDml (cmds, pols) =
 app (fn (loc, p) =>
 if decompH p
 (fn hyps =>
 List.exists (fn p' =>
-decompG p'
+if decompG p'
-(fn goals => imply (hyps, goals, NONE)))
+(fn goals => imply (hyps, goals, NONE)) then
+((*reset ();
+Print.prefaces "Match" [("hyp", p_prop p),
+("goal", p_prop p')];*)
+true)
+else
+false)
 pols) then
 ()
 else
 (ErrorMsg.errorAt loc "The information flow policy may be violated here.";
 Print.preface ("The state satisifies this predicate:", p_prop p))) cmds
 decompG p'
 (fn goals => imply (hyps, goals, SOME outs)))
 client
 orelse tryCombos (0, client, True, [])
 orelse (reset ();
-Print.preface ("Untenable hypotheses",
+Print.preface ("Untenable hypotheses"
+^ (case fl of
+Control Where => " (WHERE clause)"
+| Control Case => " (case discriminee)"
+| Data => " (returned data value)"),
 Print.p_list p_atom hyps);
 false)
 end) then
 ()
 else

Mercurial > urweb

comparison src/iflow.sml @ 1229:a2cd6664f57f