Limit 'extern' to trusted code
[hcoop/domtool2.git] / src / tycheck.sml
index ac69a6d..007a0fe 100644 (file)
@@ -24,6 +24,10 @@ open Ast Print Env
 
 structure SM = StringMap
 
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
 local
     val unifCount = ref 0
 in
@@ -170,6 +174,8 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
       | (_, CPrefix p2) => predImplies (p1All, p2)
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
+      | (CRoot, CNot (CConst _, _)) => true
+      | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
 
       | _ => false
 
@@ -296,6 +302,22 @@ fun hasTyp (e, t1, t2) =
     else
        subTyp (t1, t2)
 
+fun checkPred G (p, loc) =
+    let
+       val err = ErrorMsg.error (SOME loc)
+    in
+       case p of
+           CRoot => ()
+         | CConst s =>
+           if lookupContext G s then
+               ()
+           else
+               err ("Unbound context " ^ s)
+         | CPrefix p => checkPred G p
+         | CNot p => checkPred G p
+         | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
+    end
+
 fun checkTyp G (tAll as (t, loc)) =
     let
        val err = ErrorMsg.error (SOME loc)
@@ -309,13 +331,32 @@ fun checkTyp G (tAll as (t, loc)) =
                 (TError, loc))
          | TList t => (TList (checkTyp G t), loc)
          | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
-         | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
-                                          SM.map (checkTyp G) r), loc)
-         | TNested (p, t) => (TNested (p, checkTyp G t), loc)
+         | TAction (p, d, r) => (checkPred G p;
+                                 (TAction (p, SM.map (checkTyp G) d,
+                                           SM.map (checkTyp G) r), loc))
+         | TNested (p, t) => (checkPred G p;
+                              (TNested (p, checkTyp G t), loc))
          | TError => raise Fail "TError in parser-generated type"
          | TUnif _ => raise Fail "TUnif in parser-generated type"
     end
 
+fun envVarSetFrom v (e, _) =
+    case e of
+       ESet (v', e) =>
+       if v = v' then
+           SOME e
+       else
+           NONE
+      | EGet (_, _, e) => envVarSetFrom v e
+      | ESeq es => foldr (fn (e, found) =>
+                            case found of
+                                SOME _ => found
+                              | NONE => envVarSetFrom v e)
+                        NONE es
+      | ELocal (_, e) => envVarSetFrom v e
+
+      | _ => NONE
+
 fun checkExp G (eAll as (e, loc)) =
     let
        val dte = describe_type_error loc
@@ -389,6 +430,23 @@ fun checkExp G (eAll as (e, loc)) =
                        (TError, loc))
            end
 
+         | EALam (x, p, e) =>
+           let
+               val p' = checkPred G p
+
+               val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+               val t' = whnorm (checkExp G' e)
+           in
+               case t' of
+                   (TAction _, _) => (TNested (p, t'), loc)
+                 | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
+                                         "action",
+                                         e,
+                                         t',
+                                         NONE));
+                         (TError, loc))
+           end
+
          | ESet (evar, e) =>
            let
                val t = checkExp G e
@@ -449,21 +507,25 @@ fun checkExp G (eAll as (e, loc)) =
                                                        (case SM.find (d', name) of
                                                             NONE => SM.insert (d', name, t)
                                                           | SOME t' =>
-                                                            (subTyp (t, t')
+                                                            ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t, t')
+                                                                | SOME e => hasTyp (e, t, t'))
                                                              handle Unify ue =>
                                                                     dte (WrongType ("Shared environment variable",
                                                                                     (EVar name, loc),
-                                                                                    t,
                                                                                     t',
+                                                                                    t,
                                                                                     SOME ue));
                                                              d'))
                                                      | SOME t' =>
-                                                       (subTyp (t, t')
+                                                       ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t, t')
+                                                                | SOME e => hasTyp (e, t, t'))
                                                         handle Unify ue =>
                                                                dte (WrongType ("Shared environment variable",
                                                                                (EVar name, loc),
-                                                                               t,
                                                                                t',
+                                                                               t,
                                                                                SOME ue));
                                                         d'))
                                                d1 d2
@@ -507,21 +569,25 @@ fun checkExp G (eAll as (e, loc)) =
                                                        (case SM.find (d', name) of
                                                             NONE => SM.insert (d', name, t)
                                                           | SOME t' =>
-                                                            (subTyp (t, t')
+                                                            ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t', t)
+                                                                | SOME e => hasTyp (e, t', t))
                                                              handle Unify ue =>
                                                                     dte (WrongType ("Shared environment variable",
                                                                                     (EVar name, loc),
-                                                                                    t,
                                                                                     t',
+                                                                                    t,
                                                                                     SOME ue));
                                                              d'))
                                                      | SOME t' =>
-                                                       (subTyp (t, t')
+                                                       ((case envVarSetFrom name e1 of
+                                                                  NONE => subTyp (t', t)
+                                                                | SOME e => hasTyp (e, t', t))
                                                         handle Unify ue =>
                                                                dte (WrongType ("Shared environment variable",
                                                                                (EVar name, loc),
-                                                                               t,
                                                                                t',
+                                                                               t,
                                                                                SOME ue));
                                                         d'))
                                                d1 d2
@@ -641,8 +707,18 @@ fun checkUnit G (eAll as (_, loc)) =
 
 fun checkDecl G (d, _, loc) =
     case d of
-       DExternType name => bindType G name
-      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+       DExternType name =>
+       if !externFlag then
+           bindType G name
+       else
+           (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
+            G)
+      | DExternVal (name, t) =>
+       if !externFlag then
+           bindVal G (name, checkTyp G t, NONE)
+       else
+           (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
+            G)
       | DVal (name, to, e) =>
        let
            val to =
@@ -662,8 +738,9 @@ fun checkDecl G (d, _, loc) =
                                                   SOME ue));
            bindVal G (name, to, SOME e)
        end
+      | DContext name => bindContext G name
 
-fun checkFile G tInit (ds, eo) =
+fun checkFile G tInit (_, ds, eo) =
     let
        val G' = foldl (fn (d, G) => checkDecl G d) G ds
     in