adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

autocorres: fix bug between heap abs and signed word abs 

Jira VER-1112
This commit is contained in:
Japheth Lim 2019-06-13 16:05:07 +10:00
parent 96d0a37f5a
commit ec74efcb9e
5 changed files with 151 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
tools/autocorres/WordAbstract.thy
View File

@ -245,6 +245,14 @@ lemma abstract_val_ucast:
apply (clarsimp simp: uint_up_ucast is_up)
done
(* Base rule for heap-lifted signed words. See the function mk_sword_heap_get_rule. *)
lemma abstract_val_heap_sword_template:
"\<lbrakk> introduce_typ_abs_fn (sint :: ('a::len) signed word \<Rightarrow> int);
abstract_val P p' id p \<rbrakk>
\<Longrightarrow> abstract_val P (sint (ucast (heap_get s p' :: 'a word) :: 'a signed word))
sint (ucast (heap_get s p) :: 'a signed word)"
by simp
lemma abstract_val_scast:
"\<lbrakk> introduce_typ_abs_fn (sint :: ('a::len) signed word \<Rightarrow> int);
abstract_val P C' sint C \<rbrakk>

20
tools/autocorres/autocorres.ML
View File

@ -598,27 +598,29 @@ let
do_opt trace_opt add_trace (prefix "l2_" o make_function_name)
val skip_heap_abs = !(#skip_heap_abs opt) = SOME true
val hl_results =
val (hl_results, maybe_heap_info) =
if skip_heap_abs
then l2_results
then (l2_results, NONE)
else let
val (l2_results', HL_setup) =
HeapLift.prepare_heap_lift
filename prog_info l2_results lthy all_simpl_info
make_lifted_globals_field_name gen_word_heaps heap_abs_syntax;
in HeapLift.translate
filename prog_info l2_results' existing_l2_info existing_hl_info
HL_setup no_heap_abs force_heap_abs
heap_abs_syntax keep_going
(these (!(#trace_heap_lift opt))) do_opt trace_opt add_trace
(prefix "hl_" o make_function_name)
in (HeapLift.translate
filename prog_info l2_results' existing_l2_info existing_hl_info
HL_setup no_heap_abs force_heap_abs
heap_abs_syntax keep_going
(these (!(#trace_heap_lift opt))) do_opt trace_opt add_trace
(prefix "hl_" o make_function_name),
SOME (#heap_info HL_setup))
end
val wa_results =
if skip_word_abs
then hl_results
else WordAbstract.translate
filename prog_info hl_results existing_hl_info existing_wa_info
filename prog_info maybe_heap_info
hl_results existing_hl_info existing_wa_info
unsigned_word_abs no_signed_word_abs
(these (!(#trace_word_abs opt))) do_opt trace_opt add_trace
(prefix "wa_" o make_function_name)

65
tools/autocorres/tests/proof-tests/SignedWordAbsHeap.thy Normal file
View File

@ -0,0 +1,65 @@
(*
*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*)
theory SignedWordAbsHeap
imports
AutoCorres.AutoCorres
begin
text \<open>
Regression test for signed word abs on the lifted heap.
Jira issue ID: VER-1112
For the gory details, see the comment for the function
WordAbstract.mk_sword_heap_get_rule.
\<close>
external_file "signed_word_abs_heap.c"
install_C_file "signed_word_abs_heap.c"
autocorres [
ts_rules=nondet,
unsigned_word_abs=foo bar
]
"signed_word_abs_heap.c"
context signed_word_abs_heap begin
text \<open>
Previously, lifted word heap accesses would always be translated to
unsigned @{type nat}s, instead of signed @{typ int}s where appropriate.
\<close>
thm foo'_def bar'_def
lemma bar_123_456:
"\<lbrace>\<lambda>s. heap_w32 s p = 123 \<and> is_valid_w32 s p\<rbrace>
bar' (ptr_coerce p) 456
\<lbrace>\<lambda>r s. r = 579 \<and> heap_w32 s p = 579\<rbrace>!"
unfolding bar'_def
apply wp
apply (clarsimp simp: fun_upd_apply)
done
text \<open>
Previously, this was unprovable.
\<close>
lemma bar_n123_456:
"\<lbrace>\<lambda>s. heap_w32 s p = -123 \<and> is_valid_w32 s p\<rbrace>
bar' (ptr_coerce p) 456
\<lbrace>\<lambda>r s. r = 333 \<and> heap_w32 s p = 333\<rbrace>!"
unfolding bar'_def
apply wp
apply (clarsimp simp: fun_upd_apply)
done
end
end

25
tools/autocorres/tests/proof-tests/signed_word_abs_heap.c Normal file
View File

@ -0,0 +1,25 @@
/*
*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*/
int foo(int *p, int e) {
int a = *p;
if (e == 0) {
return 0;
} else {
return e + a;
}
}
int bar(int *p, int e) {
*p += e;
return *p;
}

47
tools/autocorres/word_abstract.ML
View File

@ -28,13 +28,23 @@ val apply_tac = Utils.apply_tac
val the' = Utils.the'
type WARules = {
ctype : typ, atype : typ,
signed : bool,
lentype : typ, ctype : typ, atype : typ,
abs_fn : term, inv_fn : term,
rules : thm list
}
fun WARules_update rules_upd {signed, lentype, ctype, atype, abs_fn, inv_fn, rules} =
{signed = signed, lentype = lentype, ctype = ctype, atype = atype,
abs_fn = abs_fn, inv_fn = inv_fn,
rules = rules_upd rules}
val word_sizes = [@{typ 64}, @{typ 32}, @{typ 16}, @{typ 8}]
fun mk_word_abs_rule T =
{
signed = false,
lentype = T,
ctype = fastype_of (@{mk_term "x :: (?'W::len) word" ('W)} T),
atype = @{typ nat},
abs_fn = @{mk_term "unat :: (?'W::len) word => nat" ('W)} T,
@ -43,10 +53,12 @@ fun mk_word_abs_rule T =
}
val word_abs : WARules list =
map mk_word_abs_rule [@{typ 32}, @{typ 16}, @{typ 8}]
map mk_word_abs_rule word_sizes
fun mk_sword_abs_rule T =
{
signed = true,
lentype = T,
ctype = fastype_of (@{mk_term "x :: (?'W::len) signed word" ('W)} T),
atype = @{typ int},
abs_fn = @{mk_term "sint :: (?'W::len) signed word => int" ('W)} T,
@ -55,7 +67,22 @@ fun mk_sword_abs_rule T =
}
val sword_abs : WARules list =
map mk_sword_abs_rule [@{typ 32}, @{typ 16}, @{typ 8}]
map mk_sword_abs_rule word_sizes
(* Make rules for signed word reads from the lifted heap.
*
* The lifted heap stores all words as unsigned, but we need to avoid
* generating unsigned arith guards when accessing signed words.
* These rules are placed early in the ruleset and kick in before the
* unsigned abstract_val rules get to run. *)
fun mk_sword_heap_get_rule ctxt heap_info (rules: WARules) =
let val uwordT = Type (@{type_name word}, [#lentype rules])
in case try (HeapLift.get_heap_getter heap_info) uwordT of
NONE => NONE
| SOME getter => SOME (@{thm abstract_val_heap_sword_template}
|> Drule.infer_instantiate ctxt
[(("heap_get", 0), Thm.cterm_of ctxt getter)])
end
(* Get abstract version of a HOL type. *)
fun get_abs_type (rules : WARules list) T =
@ -161,6 +188,8 @@ end
fun translate
(filename: string)
(prog_info: ProgramInfo.prog_info)
(* Needed for mk_sword_heap_get_rule *)
(heap_info: HeapLiftBase.heap_info option)
(* Note that we refer to the previous phase as "l2"; it may be
* from the L2 or HL phase. *)
(l2_results: FunctionInfo.phase_results)
@ -187,7 +216,15 @@ let
fun convert lthy l2_infos f: AutoCorresUtil.convert_result =
let
val old_fn_info = the (Symtab.lookup l2_infos f);
val wa_rules = rules_for f;
(* Add heap lift workaround for each word length that is in the heap. *)
fun add_sword_heap_get_rules rules =
if not (#signed rules) then [] else
case heap_info of
NONE => []
| SOME hi => the_list (mk_sword_heap_get_rule lthy hi rules)
val wa_rules = rules_for f
val sword_heap_rules = map add_sword_heap_get_rules wa_rules
(* Fix measure variable. *)
val ([measure_var_name], lthy) = Variable.variant_fixes ["rec_measure'"] lthy;
@ -260,7 +297,7 @@ let
* FIXME: move this out of convert?
*)
val rules = Utils.get_rules lthy @{named_theorems word_abs}
@ List.concat (map #rules wa_rules)
@ List.concat (sword_heap_rules @ map #rules wa_rules)
@ @{thms word_abs_default}
val fo_rules = [@{thm abstract_val_fun_app}]