portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

bitfield_gen: fixups for MCS

Browse source 
Changes the 'size suffix map' to be useful in more places. In general,
when we use the 'short name' of a variable in these generated proofs, we
run the risk of a change in variable declaration order breaking the
resulting proofs (since declaration order is how the C parser chooses
which variables get the short name). Best practice is to use the long
names whenever possible.

Uses the suffix map for some generated proofs.

Removes an unnecessary simp step.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
This commit is contained in:
Edward Pierzchalski 2020-07-20 15:04:54 +10:00
parent d989d2b85c
commit 4c0f16c7b8
1 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
tools/bitfield_gen.py
View file

@ -32,13 +32,24 @@ DEBUG = False
# name of locale the bitfield proofs should be in
loc_name = 'kernel_all_substitute'
# Isabelle word size suffixes for return value names
ret_name_suffix_map = {8: '', 16: '', 32: '', 64: '_longlong'}
# The C parser emits variables with a suffix to indicate their types; this lets
# the C parser distinguish `char x` from `int x`.
#
# The suffix map should match the C parser types for `uint{8,16,32,64}_t` in
# `include/stdint.h`.
var_size_suffix_map = {k: 'unsigned' + v for (k, v) in
{8: '_char', 16: '_short', 32: '',
64: '_longlong'}.items()}
def return_name(base):
# name of return value for standard word sizes
return 'ret__unsigned' + ret_name_suffix_map[base]
return 'ret__' + var_size_suffix_map[base]
def var_name(name, base):
# converts C variable name to Isabelle variable name via type mangling.
return name + '___' + var_size_suffix_map[base]
# Headers to include depending on which environment we are generating code for.
@ -1014,9 +1025,6 @@ done'''],
apply(clarsimp simp: typ_heap_simps c_guard_clift
packed_heap_update_collapse_hrs)
apply(simp add: guard_simps mask_shift_simps
%(name)s_tag_defs[THEN tag_eq_to_tag_masked_eq])
apply(simp add: parent_update_child[OF c_guard_clift]
typ_heap_simps c_guard_clift)
@ -1441,7 +1449,8 @@ class TaggedUnion:
sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend)
field_eq_list.append(
"%s_%s_CL.%s_CL = %s(\<^bsup>s\<^esup>%s AND %s)" %
(self.name, ref.name, field, sign_extend, field, mask))
(self.name, ref.name, field, sign_extend,
var_name(field, self.base), mask))
field_eqs = ',\n '.join(field_eq_list)
emit_named("%s_%s_new" % (self.name, ref.name), params,