Commit e84f5bdb authored by Axel Simon's avatar Axel Simon
Browse files

try to improve error messages for fields

parent ed41f6ad
......@@ -40,6 +40,8 @@ structure BooleanDomain : sig
val addToSet : bvar * bvarset -> bvarset
val isRelated : bvar * bfun -> bvar -> bool
val setToString : bvarset -> string
val projectOnto : bvarset * bfun -> bfun
......@@ -48,6 +50,7 @@ structure BooleanDomain : sig
val meet : bfun * bfun -> bfun
(*val b1 : bvar
val b2 : bvar
val b3 : bvar
......@@ -204,16 +207,27 @@ end = struct
val emptySet = IS.empty
val union = IS.union
fun addToSet (BVAR v, set) =
if IS.member (set,v) then set else IS.add' (v,set)
fun addToSet (BVAR v, set) = IS.add' (v,set)
fun setToString set =
let
fun show (v, (str, sep)) = (str ^ sep ^ i v, ", ")
in
#1 (List.foldl show ("", "{") (IS.listItems set)) ^ "}"
#1 (List.foldl show ("{", "") (IS.listItems set)) ^ "}"
end
fun isRelated (BVAR v, (us, cs)) =
let
val set = CS.foldl (fn ((v1,v2),vs) =>
if IS.member(vs,Int.abs v1) then IS.add' (Int.abs v2, vs) else
if IS.member(vs,Int.abs v2) then IS.add' (Int.abs v1, vs) else vs)
(IS.singleton v) cs
(*val _ = TextIO.print ("bVar " ^ i v ^ " is related to " ^ setToString set ^
" in " ^ showBFun (us, cs) ^ "\n")*)
in
fn (BVAR var) => IS.member(set,var)
end
fun projectOnto (keep, (us, cs)) =
let
fun addBad (v,set) = if IS.member (keep,Int.abs v) then set
......
......@@ -754,22 +754,24 @@ end = struct
aF (SymbolSet.empty, substs, env)
end
fun affectedField (bVar, env) =
fun affectedField (bVar, env as (scs,state)) =
let
val pred = BD.isRelated(bVar,Scope.getFlow state)
fun aF (_, SOME f) = SOME f
| aF (([],_), NONE) = NONE
| aF (env, NONE) = case Scope.unwrap env of
(KAPPA {ty = t}, env) => aF (env, fieldOfBVar (bVar, t))
| (SINGLE {name, ty = t}, env) => aF (env, fieldOfBVar (bVar, t))
(KAPPA {ty = t}, env) =>
aF (env, fieldOfBVar (pred, t))
| (SINGLE {name, ty = t}, env) => aF (env, fieldOfBVar (pred, t))
| (GROUP l, env) =>
let
fun findField ((_,t), SOME f) = SOME f
| findField ((_,t), NONE) = fieldOfBVar (bVar, t)
| findField ((_,t), NONE) = fieldOfBVar (pred, t)
fun aFL {name, ty = tOpt, width, uses} =
List.foldl findField
(case tOpt of
NONE => NONE
| SOME (t,_) => fieldOfBVar (bVar, t))
| SOME (t,_) => fieldOfBVar (pred, t))
(SpanMap.listItems uses)
in
aF (env, case List.mapPartial aFL l of
......@@ -1274,7 +1276,8 @@ end = struct
val bVars = texpBVarset onlyInputs (t,[])
fun checkField bVar =
(case BD.meetVarZero bVar bFun of _ => NONE)
handle (BD.Unsatisfiable _) => fieldOfBVar (bVar,t)
handle (BD.Unsatisfiable _) =>
fieldOfBVar (BD.isRelated (bVar,bFun),t)
in
List.foldl (fn (bVar,fs) => case checkField bVar of
SOME f => f :: fs
......
......@@ -121,7 +121,7 @@ structure Types = struct
in (tCF co (e, BD.empty))
end
fun fieldOfBVar (v, e) = let
fun fieldOfBVar (pred, e) = let
fun takeIfSome (t,fo) = case ff t of SOME f => SOME f | NONE => fo
and ff (FUN (f1, f2)) = takeIfSome (f2,
case List.mapPartial ff f1 of
......@@ -141,7 +141,7 @@ structure Types = struct
| ff (MONAD (r,f,t)) = takeIfSome (r, (takeIfSome (f,ff t)))
| ff (VAR (b,_)) = NONE
and ffF (RField {name = n, fty = t, exists = b}) =
if BD.eq(v,b) then SOME n else ff t
if pred b then SOME n else ff t
in ff e
end
......
......@@ -29,9 +29,6 @@ val decode = do
addrsz='0',
lock='0',
segment=DS,
mod='00',
reg/opcode='000',
rm='000',
ptrty=32}; #TODO: check
p64
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment