LogicSemantics.ml

  let pred polarity env p =
    Context.with_current_loc p.pred_loc (pred_trigger polarity env) p

  let logic env t =
    Context.with_current_loc t.term_loc (term_trigger env) t

  let region env t =
    Context.with_current_loc t.term_loc (assignable env) t

  let () = C.bootstrap_pred pred
  let () = C.bootstrap_term term
  let () = C.bootstrap_logic logic
  let () = C.bootstrap_region region

  let lemma = C.lemma

  (* -------------------------------------------------------------------------- *)
  (* --- Regions                                                            --- *)
  (* -------------------------------------------------------------------------- *)

  let assigned_of_lval env (lv : Cil_types.lval) =
    assignable_lval env (Logic_utils.lval_to_term_lval lv)

  let assigned_of_froms env froms =
    List.concat
      (List.map
         (fun ({it_content=wr},_deps) -> region env wr) froms)

  let assigned_of_assigns env = function
    | WritesAny -> None
    | Writes froms -> Some (assigned_of_froms env froms)

  let occurs_opt x = function None -> false | Some t -> F.occurs x t

  let occurs_sloc x = function
    | Sloc l -> M.occurs x l
    | Sarray(l,_,_) -> M.occurs x l
    | Srange(l,_,a,b) -> M.occurs x l || occurs_opt x a || occurs_opt x b
    | Sdescr(xs,l,p) ->
      if List.exists (Var.equal x) xs then false
      else (M.occurs x l || F.occursp x p)

  let occurs x region = List.exists (fun (_,s) -> occurs_sloc x s) region

  let vars_opt = function None -> Vars.empty | Some t -> F.vars t

  let vars_sloc = function
    | Sloc l
    | Sarray(l,_,_) ->
      M.vars l
    | Srange(l,_,a,b) ->
      Vars.union (M.vars l) (Vars.union (vars_opt a) (vars_opt b))
    | Sdescr(xs,l,p) ->
      List.fold_left
        (fun xs x -> Vars.remove x xs)
        (Vars.union (M.vars l) (F.varsp p)) xs

  let vars region =
    List.fold_left
      (fun xs (_,s) -> Vars.union xs (vars_sloc s)) Vars.empty region

  (* -------------------------------------------------------------------------- *)
  (* --- CheckAssigns                                                       --- *)
  (* -------------------------------------------------------------------------- *)

  let rec assignable_region unfold reg assignable =
    let inclusion = p_any (L.included reg) assignable in
    if unfold = 0 then inclusion
    else p_or inclusion (assignable_unfolded_region unfold reg assignable)

  (* Note that when a region cannot be unfolded anymore (that is, when it is a
     [Sloc] with atomic type, including unknown size arrays and opaque structs),
     the function return [p_false]. *)
  and assignable_unfolded_region unfold (obj, sloc) assignable =
    let range size = Some e_zero, Some (e_sub (e_int size) e_one) in
    match sloc with
    | Sloc loc ->
      begin match obj with
        | C_pointer _ | C_int _ | C_float _
        | C_comp { cfields = None } | C_array { arr_flat = None } ->
          (* Nothing to unfold *)
          p_false

        | C_comp { cfields = Some fields } ->
          let assignable_field f =
            let reg = Ctypes.object_of f.ftype, Sloc (M.field loc f) in
            assignable_region (unfold-1) reg assignable
          in
          p_conj (List.map assignable_field fields)

        | C_array { arr_flat = Some { arr_size=len ; arr_cell=typ } } ->
          let obj = Ctypes.object_of typ in
          assignable_unfolded_range unfold loc obj (range len) assignable
      end

    | Sarray (loc, obj, len) ->
      assignable_unfolded_range unfold loc obj (range len) assignable

    | Srange (loc, obj, b, e) ->
      assignable_unfolded_range unfold loc obj (b, e) assignable

    | Sdescr (xs, loc, guard) ->
      assignable_unfolded_descr unfold obj xs loc guard assignable

  and assignable_unfolded_range unfold loc obj (low, up) =
    let x = Lang.freshvar ~basename:"k" Lang.t_int in
    let k = e_var x in
    let guard = Vset.in_range k low up in
    let loc = M.shift loc obj k in
    assignable_unfolded_descr unfold obj [x] loc guard

  and assignable_unfolded_descr unfold obj xs loc guard assignable =
    p_forall xs
      (p_imply guard
         (assignable_region (unfold-1) (obj, Sloc loc) assignable))

  let check_assigns ~unfold sigma ~written ~assignable =
    p_all
      (fun reg ->
         p_imply
           (p_not (L.invalid sigma reg))
           (assignable_region unfold reg assignable)
      ) (written : region)

end