(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) (** * Abstract semantics (context-insen + localized) *) Set Implicit Arguments. Require Import hpattern vgtac. Require Import Global UserProofType DStr Syn Global. Require DomCon SemCon DomInsen. Require Import SemCommon. Module Make (Import PInput : PINPUT). Local Open Scope type. Include DomInsen.Make PInput. Section Sem. Variable g : G.t. Let pgm : InterCfg.t := G.icfg g. Let mode : UserInputType.update_mode := UserInputType.Strong. Variable amap : access_map. Definition postfix_cmd (cn : InterNode.t) (s : state_t) : Prop := forall cmd (Hcmd : Some cmd = InterCfg.get_cmd pgm cn), let m := s (cn, Inputof) in let m' := run_only mode g cn cmd m in let m'' := s (cn, Outputof) in Mem.le m' m''. Definition postfix_intra_edge (cn : InterNode.t) (s : state_t) : Prop := let p := InterNode.get_pid cn in let n := InterNode.get_node cn in forall n' cfg (Hcfg : InterCfg.PidMap.MapsTo p cfg (InterCfg.cfgs pgm)) (Hedge : IntraCfg.is_succ cfg n n') (Hcn_cond: not (InterCfg.is_call_node pgm cn)), Mem.le (s (cn, Outputof)) (s ((p, n'), Inputof)). Definition postfix_intra_call (cn : InterNode.t) (s : state_t) : Prop := forall callee (Hedge : InterCfg.is_succ pgm cn (callee, IntraNode.Entry)) retn (Hretn : Some retn = InterCfg.returnof pgm cn), let access := get_all_access callee amap in let m := s (cn, Outputof) in let m' := Mem.subtract access m in Mem.le m' (s (retn, Inputof)). Definition postfix_inter_call (cn : InterNode.t) (s : state_t) : Prop := forall callee (Hedge : InterCfg.is_succ pgm cn (callee, IntraNode.Entry)), let access := get_all_access callee amap in let m := s (cn, Outputof) in let m' := Mem.restrict access m in Mem.le m' (s ((callee, IntraNode.Entry), Inputof)). Definition postfix_inter_ret (cn : InterNode.t) (s : state_t) : Prop := forall p (Hp : cn = (p, IntraNode.Exit)) cn' (Hedge : InterCfg.is_succ pgm cn cn') calln (Hret: Some cn' = InterCfg.returnof pgm calln), Mem.le (s (cn, Outputof)) (s (cn', Inputof)). Definition postfix (s : state_t) : Prop := forall (cn : InterNode.t) , postfix_cmd cn s /\ postfix_intra_edge cn s /\ postfix_intra_call cn s /\ postfix_inter_call cn s /\ postfix_inter_ret cn s. Definition sound_amap_run (s : state_t) := forall cn cmd (Hcmd : Some cmd = InterCfg.get_cmd pgm cn), Acc.le (Acc.get_acc (run_access mode g cn cmd (s (cn, SemCommon.Inputof)))) (get_access (InterNode.get_pid cn) amap). Definition sound_amap_reachable := forall f1 f2 (Hr : InterCfg.reachable pgm f1 f2), Acc.le (get_access f2 amap) (get_access f1 amap). Definition sound_amap (s : state_t) : Prop := sound_amap_run s /\ sound_amap_reachable. End Sem. Local Close Scope type. End Make.