open DItv open DomAbs open DomBasic open DomMem open Global open InterNode open SemEval open SemMem open Syn open TStr open UserInputType (** val itv_prune : binop -> Itv.t -> Itv.t -> Itv.t **) let itv_prune op x y = match x with | Itv.V (a, b) -> (match y with | Itv.V (c, d) -> (match op with | Lt -> Itv.gen_itv a (Itv.min' b (Itv.minus'_one d)) | Gt -> Itv.gen_itv (Itv.max' a (Itv.plus'_one c)) b | Le -> Itv.gen_itv a (Itv.min' b d) | Ge -> Itv.gen_itv (Itv.max' a c) b | Eq -> Itv.meet x y | _ -> x) | Itv.Bot -> Itv.bot) | Itv.Bot -> Itv.bot module Make = functor (M:Monad.Monad) -> functor (MB:sig val mem_find : Loc.t -> Mem.t -> Val.t M.m val mem_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m val mem_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m val mem_pre_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m end) -> struct module SemMem = Make(M)(MB) module SemEval = SemEval.Make(M)(MB) (** val prune : G.t -> update_mode -> t -> exp -> Mem.t -> Mem.t M.m **) let prune g mode node cond m0 = match cond with | BinOp (op, e1, e, _) -> (match e1 with | Lval (lv, _) -> let Coq_lval_intro (lh, o, _) = lv in (match lh with | VarLhost (x, is_global) -> (match o with | NoOffset -> let x_lv = SemEval.eval_var node x is_global in M.bind (SemMem.mem_lookup (PowLoc.singleton x_lv) m0) (fun x_v -> M.bind (SemEval.eval mode node e m0) (fun v -> let x_v' = modify_itv x_v (itv_prune op (itv_of_val x_v) (itv_of_val v)) in SemMem.mem_update mode g x_lv x_v' m0)) | _ -> M.ret m0) | MemLhost _ -> M.ret m0) | _ -> M.ret m0) | _ -> M.ret m0 end