Commit 6cb5d379 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Detect illegal accesses to allocated memory.

\valid(p+i) now additionally checks whether p and p+i point to the same
block
parent 2118ef54
......@@ -279,6 +279,34 @@ let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
let arith_op = function
| MinusPI -> MinusA
| PlusPI -> PlusA
| IndexPI -> PlusA
| _ -> assert false
let rec ptr_index ?(index=(Cil.zero Location.unknown)) exp =
(* ****************************************************************** *)
match exp.enode with
| BinOp(op, lhs, rhs, _) ->
(match op with
(* Pointer arithmetic: split pointer and integer parts *)
| MinusPI | PlusPI | IndexPI ->
let index = Cil.mkBinOp Location.unknown (arith_op op) index rhs
in ptr_index ~index lhs
(* Other arithmetic: treat the whole expression as pointer address *)
| MinusPP | PlusA | MinusA | Mult | Div | Mod ->
(exp, index)
| _ -> assert false)
(* ****************************************************************** *)
| CastE(_) -> ptr_index ~index (Cil.stripCasts exp)
(* ****************************************************************** *)
| Const(_)
| StartOf(_)
| AddrOf(_)
| Lval(_) -> (exp, index)
| _ -> assert false
(*
Local Variables:
compile-command: "make"
......
......@@ -91,6 +91,11 @@ val reorder_ast: unit -> unit
val cty: logic_type -> typ
(* Assume that the logic type is indeed a C type. Just return it. *)
val ptr_index: ?index:Cil_types.exp -> Cil_types.exp
-> Cil_types.exp * Cil_types.exp
(** Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts. *)
(* ************************************************************************** *)
(** {2 Handling prefixes of generated library functions and variables} *)
(* ************************************************************************** *)
......
......@@ -213,21 +213,23 @@ static size_t block_length(void* ptr) {
}
/* return whether the size bytes of ptr are readable/writable */
static int valid(void* ptr, size_t size) {
if(ptr == NULL)
static int valid(void* ptr, size_t size, void *ptr_base) {
bt_block * blk = bt_find(ptr);
bt_block * blk_base = bt_find(ptr_base);
if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
bt_block * tmp = bt_find(ptr);
return (tmp == NULL) ? false :
(tmp->size - ((size_t)ptr - tmp->ptr ) >= size && !tmp->is_readonly);
return (blk->size - ((size_t)ptr - blk->ptr) >= size && !blk->is_readonly);
}
/* return whether the size bytes of ptr are readable */
static int valid_read(void* ptr, size_t size) {
if(ptr == NULL)
static int valid_read(void* ptr, size_t size, void *ptr_base) {
bt_block * blk = bt_find(ptr);
bt_block * blk_base = bt_find(ptr_base);
if (blk == NULL || blk_base == NULL || blk->ptr != blk_base->ptr)
return false;
bt_block * tmp = bt_find(ptr);
return (tmp == NULL) ?
false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
return (blk->size - ((size_t)ptr - blk->ptr) >= size);
}
/* return the base address of the block containing ptr */
......@@ -394,7 +396,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
vassert(valid(memptr, sizeof(void*)),
vassert(valid(memptr, sizeof(void*), memptr),
"\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
......
......@@ -134,7 +134,7 @@ int __e_acsl_freeable(void * ptr)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __e_acsl_valid(void * ptr, size_t size)
int __e_acsl_valid(void * ptr, size_t size, void *ptr_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
......@@ -144,7 +144,7 @@ int __e_acsl_valid(void * ptr, size_t size)
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __e_acsl_valid_read(void * ptr, size_t size)
int __e_acsl_valid_read(void * ptr, size_t size, void *ptr_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
......
......@@ -30,8 +30,8 @@
#include <errno.h>
#include <sys/resource.h>
static int valid(void * ptr, size_t size);
static int valid_read(void * ptr, size_t size);
static int valid(void * ptr, size_t size, void *ptr_base);
static int valid_read(void * ptr, size_t size, void *ptr_base);
#include "e_acsl_string.h"
#include "e_acsl_bits.h"
......@@ -77,24 +77,26 @@ static void readonly(void * ptr) {
/* E-ACSL annotations */
/* ****************** */
static int valid(void * ptr, size_t size) {
static int valid(void * ptr, size_t size, void *ptr_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
if (IS_ON_HEAP(addr))
return heap_allocated(addr, size);
return heap_allocated(addr, size, base);
else if (IS_ON_STACK(addr) || IS_ON_TLS(addr))
return static_allocated(addr, size);
return static_allocated(addr, size, base);
else if (IS_ON_GLOBAL(addr))
return static_allocated(addr, size) && !global_readonly(addr);
return static_allocated(addr, size, base) && !global_readonly(addr);
else if (!IS_ON_VALID(addr))
return 0;
return 0;
}
static int valid_read(void * ptr, size_t size) {
static int valid_read(void * ptr, size_t size, void *ptr_base) {
uintptr_t addr = (uintptr_t)ptr;
uintptr_t base = (uintptr_t)ptr_base;
TRY_SEGMENT(addr,
return heap_allocated(addr, size),
return static_allocated(addr, size));
return heap_allocated(addr, size, base),
return static_allocated(addr, size, base));
if (!IS_ON_VALID(addr))
return 0;
return 0;
......
......@@ -119,6 +119,11 @@ const size_t max_allocated = SIZE_MAX - HEAP_SEGMENT;
#define ALLOC_SIZE(_s) \
(_s > 0 && _s < max_allocated ? ALIGNED_SIZE(_s) : 0)
/** \brief Evaluate to `true` if address _addr belongs to a memory block
* with base address _base and length _length */
#define BELONGS(_addr, _base, _length) \
(_addr >= _base && _addr < _base + _length)
/*! \brief For short blocks numbers 1 to 36 represent lengths and offsets,
* such that:
* - 0 -> length 0, offset 0
......@@ -296,14 +301,14 @@ static void validate_memory_layout() {
* program's heap */
# define DVALIDATE_HEAP_ACCESS(_addr, _size) \
DVASSERT(IS_ON_HEAP(_addr), "Expected heap location: %a\n ", _addr); \
DVASSERT(heap_allocated((uintptr_t)_addr, _size), \
DVASSERT(heap_allocated((uintptr_t)_addr, _size, (uintptr_t)_addr), \
"Operation on unallocated heap block [%a + %lu]\n ", _addr, _size)
/* Assert that memory block [_addr, _addr + _size] is allocated on stack, TLS
* or globally */
# define DVALIDATE_STATIC_ACCESS(_addr, _size) \
DVASSERT(IS_ON_STATIC(_addr), "Expected location: %a\n ", _addr); \
DVASSERT(static_allocated((uintptr_t)_addr, _size), \
DVASSERT(static_allocated((uintptr_t)_addr, _size,(uintptr_t)_addr), \
"Operation on unallocated block [%a + %lu]\n ", _addr, _size)
/* Same as ::DVALIDATE_STATIC_LOCATION but for a single memory location */
......@@ -339,8 +344,8 @@ static void validate_memory_layout() {
/* See definitions for documentation */
static uintptr_t heap_info(uintptr_t addr, char type);
static uintptr_t static_info(uintptr_t addr, char type);
static int heap_allocated(uintptr_t addr, size_t size);
static int static_allocated(uintptr_t addr, long size);
static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr);
static int freeable(void *ptr);
/*! \brief Quick test to check if a static location belongs to allocation.
......@@ -507,8 +512,10 @@ static void shadow_freea(void *ptr) {
/*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to a tracked stack, tls or
* global memory block and 0 otherwise.
* This function is only safe if applied to a tls, stack or global address. */
static int static_allocated(uintptr_t addr, long size) {
* This function is only safe if applied to a tls, stack or global address.
* Explanations regarding the third argument - `base_ptr` - are given
* via inline documentation of function ::heap_allocated */
static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) {
unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
/* Unless the address belongs to tracked allocation 0 is returned */
if (prim_shadow[0]) {
......@@ -525,7 +532,14 @@ static int static_allocated(uintptr_t addr, long size) {
offset = short_offsets[code];
length = short_lengths[code];
}
return offset + size <= length;
if (addr != base_ptr) {
uintptr_t base_addr = addr - offset;
return BELONGS(base_ptr, base_addr, length)
&& offset + size <= length;
} else {
return offset + size <= length;
}
}
return 0;
}
......@@ -536,7 +550,7 @@ static int static_allocated(uintptr_t addr, long size) {
static int static_initialized(uintptr_t addr, long size) {
/* Return 0 right away if the address does not belong to
* static allocation */
if (!static_allocated(addr, size))
if (!static_allocated(addr, size, addr))
return 0;
DVALIDATE_STATIC_ACCESS(addr, size);
......@@ -669,7 +683,7 @@ static void mark_readonly (uintptr_t addr, long size) {
/* Since read-only blocks can only be stored in the globals segments (e.g.,
* TEXT), this function required ptr carry a global address. */
DASSERT(IS_ON_GLOBAL(addr));
DASSERT(static_allocated(addr, 1));
DASSERT(static_allocated_one(addr));
DVASSERT(!(addr - base_addr(addr) + size > block_length(addr)),
"Attempt to mark read-only %lu bytes past block boundaries\n"
"starting at %a with block length %lu at base address %a\n",
......@@ -919,7 +933,7 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
vassert(valid(memptr, sizeof(void*)),
vassert(valid(memptr, sizeof(void*), memptr),
"\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
......@@ -934,13 +948,27 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
/*! \brief Return a non-zero value if a memory region of length `size`
* starting at address `addr` belongs to an allocated (tracked) heap memory
* block and a 0 otherwise. Note, this function is only safe if applied to a
* heap address. */
static int heap_allocated(uintptr_t addr, size_t size) { /* + */
* heap address.
*
* Note the third argument `base_ptr` that represents the base of a pointer, i.e.,
* `addr` of the form `base_ptr + i`, where `i` is some integer index.
* ::heap_allocated also returns zero if `base_ptr` and `addr` belong to different
* memory blocks, or if `base_ptr` lies within unallocated region. The intention
* here is to be able to detect dereferencing of a valid memory block through
* a pointer to a different block. Consider, for instance, some pointer `p` that
* points to a memory block `B`, and an index `i`, such that `p+i` references a
* memory location belonging to a different memory block (say `C`). From a
* low-level viewpoint, dereferencing `p+i` is safe (since it belongs to a properly
* allocated block). From our perspective, however, dereference of `p+i` is
* only legal if both `p` and `p+i` point to the same block. */
static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
/* Base address of the shadow segment the address belongs to */
uintptr_t *shadow = (uintptr_t*)HEAP_SHADOW(addr - addr%HEAP_SEGMENT);
/* Non-zero if the segment belongs to heap allocation */
if (shadow[0]) {
uintptr_t *base_shadow =
(uintptr_t*)HEAP_SHADOW(base_ptr - base_ptr%HEAP_SEGMENT);
uintptr_t *first_segment = (uintptr_t*)HEAP_SHADOW(shadow[0]);
/* shadow[0] - base address of the tracked block
* fist_segment[1] - length (i.e., location in the first segment
......@@ -948,7 +976,8 @@ static int heap_allocated(uintptr_t addr, size_t size) { /* + */
* offset is the difference between the address and base address (shadow[0])
* Then an address belongs to heap allocation if
* offset + size <= length */
return (addr - shadow[0]) + size <= first_segment[1];
return base_shadow[0] == shadow[0] &&
(addr - shadow[0]) + size <= first_segment[1];
}
return 0;
}
......
......@@ -35,7 +35,7 @@ let handle_error f env =
Env.Context.restore env
(* internal to [named_predicate_to_exp] but put it outside in order to not add
extra tedious parameter.
extra tedious parameter.
It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false
......@@ -163,8 +163,8 @@ let constant_to_exp ~loc t = function
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
| LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), false
| LChr c -> Cil.new_exp ~loc (Const (CChr c)), false
| LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} ->
if l <> u then
| LReal {r_literal=s; r_nearest=f; r_lower=l; r_upper=u} ->
if l <> u then
Options.warning ~current:true ~once:true
"approximating a real number by a float";
Cil.new_exp ~loc (Const (CReal (f, FLongDouble, Some s))), false
......@@ -225,11 +225,11 @@ let cast_integer_to_float lty lty_t e =
e
let rec thost_to_host kf env = function
| TVar { lv_origin = Some v } ->
| TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
| TVar ({ lv_origin = None } as logic_v) ->
Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
| TResult _typ ->
| TResult _typ ->
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let lhost = Misc.result_lhost kf in
......@@ -242,16 +242,16 @@ let rec thost_to_host kf env = function
and toffset_to_offset ?loc kf env = function
| TNoOffset -> NoOffset, env
| TField(f, offset) ->
| TField(f, offset) ->
let offset, env = toffset_to_offset ?loc kf env offset in
Field(f, offset), env
| TIndex(t, offset) ->
| TIndex(t, offset) ->
let e, env = term_to_exp kf env t in
let offset, env = toffset_to_offset kf env offset in
Index(e, offset), env
| TModel _ -> not_yet env "model"
and tlval_to_lval kf env (host, offset) =
and tlval_to_lval kf env (host, offset) =
let host, env, name = thost_to_host kf env host in
let offset, env = toffset_to_offset kf env offset in
let name = match offset with NoOffset -> name | Field _ | Index _ -> "" in
......@@ -260,13 +260,13 @@ and tlval_to_lval kf env (host, offset) =
(* the returned boolean says that the expression is an mpz_string;
the returned string is the name of the generated variable corresponding to
the term. *)
and context_insensitive_term_to_exp kf env t =
and context_insensitive_term_to_exp kf env t =
let loc = t.term_loc in
match t.term_node with
| TConst c ->
let c, is_mpz_string = constant_to_exp ~loc t c in
c, env, is_mpz_string, ""
| TLval lv ->
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
Cil.new_exp ~loc (Lval lv), env, false, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, false, "sizeof"
......@@ -287,7 +287,7 @@ and context_insensitive_term_to_exp kf env t =
| BNot -> "__gmpz_com", "bnot"
| LNot -> assert false
in
let _, e, env =
let _, e, env =
Env.new_var_and_mpz_init
~loc
env
......@@ -322,8 +322,8 @@ and context_insensitive_term_to_exp kf env t =
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = name_of_binop bop in
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
in
e, env, false, ""
else
......@@ -354,16 +354,16 @@ and context_insensitive_term_to_exp kf env t =
let name = name_of_binop bop ^ "_guard" in
comparison_to_exp ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
let mk_stmts _v e =
assert (Gmpz.is_t ty);
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
let cond =
Misc.mk_e_acsl_guard
(Env.annotation_kind env)
let cond =
Misc.mk_e_acsl_guard
(Env.annotation_kind env)
kf
guard
(Logic_const.prel ~loc (Req, t2, zero))
(Logic_const.prel ~loc (Req, t2, zero))
in
Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
......@@ -424,10 +424,10 @@ and context_insensitive_term_to_exp kf env t =
let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in
e, env, false, ""
| TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
| TAddrOf lv ->
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOf ~loc lv, env, false, "addrof"
| TStartOf lv ->
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOrStartOf ~loc lv, env, false, "startof"
| Tapp(li, [], args) when Builtins.mem li.l_var_info.lv_name ->
......@@ -468,7 +468,7 @@ and context_insensitive_term_to_exp kf env t =
let res3 = term_to_exp kf (Env.push env2) t3 in
let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
e, env, false, ""
| Tat(t, LogicLabel(_, label)) when label = "Here" ->
| Tat(t, LogicLabel(_, label)) when label = "Here" ->
let e, env = term_to_exp kf env t in
e, env, false, ""
| Tat(t', label) ->
......@@ -503,7 +503,7 @@ and context_insensitive_term_to_exp kf env t =
constructs. *)
and term_to_exp kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
Printer.pp_term t generate_rte;
let env = Env.rte env false in
let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
......@@ -550,18 +550,27 @@ and comparison_to_exp
(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
ctx
(fun v _ ->
[ Misc.mk_call ~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e ] ])
in
res, env, false, name
and get_c_term_type = function
| Ctype ty -> ty
| _ -> assert false
and mk_ptr_sizeof typ loc =
match Cil.unrollType typ with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
(* \valid, \offset and \initialized annotations *)
and mmodel_call_with_size ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
......@@ -573,50 +582,63 @@ and mmodel_call_with_size ~loc kf name ctx env t =
None
ctx
(fun v _ ->
let ty = match t.term_type with
| Ctype ty -> ty
| _ -> assert false
in
let sizeof = match Cil.unrollType ty with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
in
[ Misc.mk_call
~loc ~result:(Cil.var v) (Misc.mk_api_name name) [ e; sizeof ] ])
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = (Misc.mk_api_name name) in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
and mmodel_call_valid ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index e in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Misc.mk_api_name name in
let args = [ e; sizeof; base ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
and at_to_exp env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
That is this variable which is the resulting expression.
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
the one of [e]. *)
let loc = Stmt.loc stmt in
let res_v, res, new_env =
Env.new_var
~loc
~name:"at"
~name:"at"
~scope:Env.Function
env
t_opt
(Cil.typeOf e)
(Cil.typeOf e)
(fun _ _ -> [])
in
let env_ref = ref new_env in
(* visitor modifying in place the labeled statement in order to store [e]
in the resulting variable at this location (which is the only correct
one). *)
let o = object
let o = object
inherit Visitor.frama_c_inplace
method !vstmt_aux stmt =
method !vstmt_aux stmt =
(* either a standard C affectation or an mpz one according to type of
[e] *)
[e] *)
let new_stmt = Gmpz.init_set ~loc (Cil.var res_v) res e in
assert (!env_ref == new_env);
(* generate the new block of code for the labeled statement and the
corresponding environment *)
let block, new_env =
let block, new_env =
Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
in
let pre = match label with
......@@ -654,7 +676,7 @@ and named_predicate_content_to_exp ?name kf env p =
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
| Por(p1, p2) ->
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
let env' = Env.push env1 in
......@@ -662,21 +684,21 @@ and named_predicate_content_to_exp ?name kf env p =
let name = match name with None -> "or" | Some n -> n in
conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
| Pxor _ -> not_yet env "xor"
| Pimplies(p1, p2) ->
| Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
named_predicate_to_exp
named_predicate_to_exp
~name:"implies"
kf
env
(Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
| Piff(p1, p2) ->
| Piff(p1, p2) ->
(* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
named_predicate_to_exp
named_predicate_to_exp
~name:"equiv"
kf
env
(Logic_const.pand ~loc
(Logic_const.pimplies ~loc (p1, p2),
(Logic_const.pimplies ~loc (p1, p2),
Logic_const.pimplies ~loc (p2, p1)))
| Pnot p ->
let e, env = named_predicate_to_exp kf env p in
......@@ -688,9 +710,9 @@ and named_predicate_content_to_exp ?name kf env p =
conditional_to_exp loc None e1 res2 res3
| Plet _ -> not_yet env "let _ = _ in _"
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
| Pat(p, LogicLabel(_, label)) when label = "Here" ->
| Pat(p, LogicLabel(_, label)) when label = "Here" ->
named_predicate_to_exp kf env p
| Pat(p', label) ->
| Pat(p', label) ->
(* convert [t'] to [e] in a separated local env *)
let e, env = named_predicate_to_exp kf (Env.push env) p' in
let e, env, is_string = at_to_exp env None label e in
......@@ -698,13 +720,13 @@ and named_predicate_content_to_exp ?name kf env p =
e, env
| Pvalid_read(LogicLabel(_, label) as llabel, t) as pc
| (Pvalid(LogicLabel(_, label) as llabel, t) as pc) when label = "Here" ->
let call_valid t =
let call_valid t =
let name = match pc with
| Pvalid _ -> "valid"
| Pvalid_read _ -> "valid_read"