cfc544ab49
In Python 3, dict value iterators aren't deterministic between runs, which causes nondeterministic definition output order. Some L4V proofs are sensitive to this order. Use sorted keys to guarantee order when iterating over values.
2896 lines
110 KiB
Python
Executable file
2896 lines
110 KiB
Python
Executable file
#!/usr/bin/env python3
|
|
|
|
#
|
|
# Copyright 2017, 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)
|
|
#
|
|
|
|
##
|
|
# A tool for generating bifield structures with get/set/new methods
|
|
# including Isabelle/HOL specifications and correctness proofs.
|
|
##
|
|
|
|
from __future__ import print_function, division
|
|
import sys
|
|
import os.path
|
|
import optparse
|
|
import re
|
|
import itertools
|
|
import tempfile
|
|
|
|
from six.moves import range
|
|
from functools import reduce
|
|
|
|
import lex
|
|
from ply import yacc
|
|
|
|
import umm
|
|
|
|
# Whether debugging is enabled (turn on with command line option --debug).
|
|
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'}
|
|
|
|
|
|
def return_name(base):
|
|
# name of return value for standard word sizes
|
|
return 'ret__unsigned' + ret_name_suffix_map[base]
|
|
|
|
|
|
# Headers to include depending on which environment we are generating code for.
|
|
INCLUDES = {
|
|
'sel4': ['assert.h', 'config.h', 'stdint.h', 'util.h'],
|
|
'libsel4': ['autoconf.h', 'sel4/simple_types.h', 'sel4/debug_assert.h'],
|
|
}
|
|
|
|
ASSERTS = {
|
|
'sel4': 'assert',
|
|
'libsel4': 'seL4_DebugAssert'
|
|
}
|
|
|
|
INLINE = {
|
|
'sel4': 'static inline',
|
|
'libsel4': 'LIBSEL4_INLINE_FUNC'
|
|
}
|
|
|
|
TYPES = {
|
|
"sel4": {
|
|
8: "uint8_t",
|
|
16: "uint16_t",
|
|
32: "uint32_t",
|
|
64: "uint64_t"
|
|
},
|
|
|
|
"libsel4": {
|
|
8: "seL4_Uint8",
|
|
16: "seL4_Uint16",
|
|
32: "seL4_Uint32",
|
|
64: "seL4_Uint64"
|
|
}
|
|
}
|
|
|
|
# Parser
|
|
|
|
reserved = ('BLOCK', 'BASE', 'FIELD', 'FIELD_HIGH', 'MASK', 'PADDING',
|
|
'TAGGED_UNION', 'TAG')
|
|
|
|
tokens = reserved + ('IDENTIFIER', 'INTLIT', 'LBRACE', 'RBRACE',
|
|
'LPAREN', 'RPAREN', 'COMMA')
|
|
|
|
t_LBRACE = r'{'
|
|
t_RBRACE = r'}'
|
|
t_LPAREN = r'\('
|
|
t_RPAREN = r'\)'
|
|
t_COMMA = r','
|
|
|
|
reserved_map = dict((r.lower(), r) for r in reserved)
|
|
|
|
|
|
def t_IDENTIFIER(t):
|
|
r'[A-Za-z_]\w+|[A-Za-z]'
|
|
t.type = reserved_map.get(t.value, 'IDENTIFIER')
|
|
return t
|
|
|
|
|
|
def t_INTLIT(t):
|
|
r'([1-9][0-9]*|0[oO]?[0-7]+|0[xX][0-9a-fA-F]+|0[bB][01]+|0)[lL]?'
|
|
t.value = int(t.value, 0)
|
|
return t
|
|
|
|
|
|
def t_NEWLINE(t):
|
|
r'\n+'
|
|
t.lexer.lineno += len(t.value)
|
|
|
|
|
|
def t_comment(t):
|
|
r'--.*|\#.*'
|
|
|
|
|
|
t_ignore = ' \t'
|
|
|
|
|
|
def t_error(t):
|
|
print("%s: Unexpected character '%s'" % (sys.argv[0], t.value[0]),
|
|
file=sys.stderr)
|
|
if DEBUG:
|
|
print('Token: %s' % str(t), file=sys.stderr)
|
|
sys.exit(1)
|
|
|
|
|
|
def p_start(t):
|
|
"""start : entity_list"""
|
|
t[0] = t[1]
|
|
|
|
|
|
def p_entity_list_empty(t):
|
|
"""entity_list : """
|
|
t[0] = (None, {}, {})
|
|
|
|
|
|
def p_entity_list_base(t):
|
|
"""entity_list : entity_list base"""
|
|
current_base, block_map, union_map = t[1]
|
|
block_map.setdefault(t[2], {})
|
|
union_map.setdefault(t[2], {})
|
|
t[0] = (t[2], block_map, union_map)
|
|
|
|
|
|
def p_entity_list_block(t):
|
|
"""entity_list : entity_list block"""
|
|
current_base, block_map, union_map = t[1]
|
|
block_map[current_base][t[2].name] = t[2]
|
|
t[0] = (current_base, block_map, union_map)
|
|
|
|
|
|
def p_entity_list_union(t):
|
|
"""entity_list : entity_list tagged_union"""
|
|
current_base, block_map, union_map = t[1]
|
|
union_map[current_base][t[2].name] = t[2]
|
|
t[0] = (current_base, block_map, union_map)
|
|
|
|
|
|
def p_base_simple(t):
|
|
"""base : BASE INTLIT"""
|
|
t[0] = (t[2], t[2], 0)
|
|
|
|
|
|
def p_base_mask(t):
|
|
"""base : BASE INTLIT LPAREN INTLIT COMMA INTLIT RPAREN"""
|
|
t[0] = (t[2], t[4], t[6])
|
|
|
|
|
|
def p_block(t):
|
|
"""block : BLOCK IDENTIFIER opt_visible_order_spec""" \
|
|
""" LBRACE fields RBRACE"""
|
|
t[0] = Block(name=t[2], fields=t[5], visible_order=t[3])
|
|
|
|
|
|
def p_opt_visible_order_spec_empty(t):
|
|
"""opt_visible_order_spec : """
|
|
t[0] = None
|
|
|
|
|
|
def p_opt_visible_order_spec(t):
|
|
"""opt_visible_order_spec : LPAREN visible_order_spec RPAREN"""
|
|
t[0] = t[2]
|
|
|
|
|
|
def p_visible_order_spec_empty(t):
|
|
"""visible_order_spec : """
|
|
t[0] = []
|
|
|
|
|
|
def p_visible_order_spec_single(t):
|
|
"""visible_order_spec : IDENTIFIER"""
|
|
t[0] = [t[1]]
|
|
|
|
|
|
def p_visible_order_spec(t):
|
|
"""visible_order_spec : visible_order_spec COMMA IDENTIFIER"""
|
|
t[0] = t[1] + [t[3]]
|
|
|
|
|
|
def p_fields_empty(t):
|
|
"""fields : """
|
|
t[0] = []
|
|
|
|
|
|
def p_fields_field(t):
|
|
"""fields : fields FIELD IDENTIFIER INTLIT"""
|
|
t[0] = t[1] + [(t[3], t[4], False)]
|
|
|
|
|
|
def p_fields_field_high(t):
|
|
"""fields : fields FIELD_HIGH IDENTIFIER INTLIT"""
|
|
t[0] = t[1] + [(t[3], t[4], True)]
|
|
|
|
|
|
def p_fields_padding(t):
|
|
"""fields : fields PADDING INTLIT"""
|
|
t[0] = t[1] + [(None, t[3], False)]
|
|
|
|
|
|
def p_tagged_union(t):
|
|
"""tagged_union : TAGGED_UNION IDENTIFIER IDENTIFIER""" \
|
|
""" LBRACE masks tags RBRACE"""
|
|
t[0] = TaggedUnion(name=t[2], tagname=t[3], classes=t[5], tags=t[6])
|
|
|
|
|
|
def p_tags_empty(t):
|
|
"""tags :"""
|
|
t[0] = []
|
|
|
|
|
|
def p_tags(t):
|
|
"""tags : tags TAG IDENTIFIER INTLIT"""
|
|
t[0] = t[1] + [(t[3], t[4])]
|
|
|
|
|
|
def p_masks_empty(t):
|
|
"""masks :"""
|
|
t[0] = []
|
|
|
|
|
|
def p_masks(t):
|
|
"""masks : masks MASK INTLIT INTLIT"""
|
|
t[0] = t[1] + [(t[3], t[4])]
|
|
|
|
|
|
def p_error(t):
|
|
print("Syntax error at token '%s'" % t.value, file=sys.stderr)
|
|
sys.exit(1)
|
|
|
|
# Templates
|
|
|
|
# C templates
|
|
|
|
|
|
typedef_template = \
|
|
"""struct %(name)s {
|
|
%(type)s words[%(multiple)d];
|
|
};
|
|
typedef struct %(name)s %(name)s_t;"""
|
|
|
|
generator_template = \
|
|
"""%(inline)s %(block)s_t CONST
|
|
%(block)s_new(%(gen_params)s) {
|
|
%(block)s_t %(block)s;
|
|
|
|
%(asserts)s
|
|
|
|
%(gen_inits)s
|
|
|
|
return %(block)s;
|
|
}"""
|
|
|
|
ptr_generator_template = \
|
|
"""%(inline)s void
|
|
%(block)s_ptr_new(%(ptr_params)s) {
|
|
%(asserts)s
|
|
|
|
%(ptr_inits)s
|
|
}"""
|
|
|
|
reader_template = \
|
|
"""%(inline)s %(type)s CONST
|
|
%(block)s_get_%(field)s(%(block)s_t %(block)s) {
|
|
%(type)s ret;
|
|
ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
|
|
/* Possibly sign extend */
|
|
if (%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))) {
|
|
ret |= 0x%(high_bits)x;
|
|
}
|
|
return ret;
|
|
}"""
|
|
|
|
ptr_reader_template = \
|
|
"""%(inline)s %(type)s PURE
|
|
%(block)s_ptr_get_%(field)s(%(block)s_t *%(block)s_ptr) {
|
|
%(type)s ret;
|
|
ret = (%(block)s_ptr->words[%(index)d] & 0x%(mask)x%(suf)s) """ \
|
|
"""%(r_shift_op)s %(shift)d;
|
|
/* Possibly sign extend */
|
|
if (%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))) {
|
|
ret |= 0x%(high_bits)x;
|
|
}
|
|
return ret;
|
|
}"""
|
|
|
|
writer_template = \
|
|
"""%(inline)s %(block)s_t CONST
|
|
%(block)s_set_%(field)s(%(block)s_t %(block)s, %(type)s v%(base)d) {
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
%(block)s.words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
|
|
return %(block)s;
|
|
}"""
|
|
|
|
ptr_writer_template = \
|
|
"""%(inline)s void
|
|
%(block)s_ptr_set_%(field)s(%(block)s_t *%(block)s_ptr, %(type)s v%(base)d) {
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
%(block)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(block)s_ptr->words[%(index)d] |= (v%(base)d %(w_shift_op)s """ \
|
|
"""%(shift)d) & 0x%(mask)x;
|
|
}"""
|
|
|
|
union_generator_template = \
|
|
"""%(inline)s %(union)s_t CONST
|
|
%(union)s_%(block)s_new(%(gen_params)s) {
|
|
%(union)s_t %(union)s;
|
|
|
|
%(asserts)s
|
|
|
|
%(gen_inits)s
|
|
|
|
return %(union)s;
|
|
}"""
|
|
|
|
ptr_union_generator_template = \
|
|
"""%(inline)s void
|
|
%(union)s_%(block)s_ptr_new(%(ptr_params)s) {
|
|
%(asserts)s
|
|
|
|
%(ptr_inits)s
|
|
}"""
|
|
|
|
union_reader_template = \
|
|
"""%(inline)s %(type)s CONST
|
|
%(union)s_%(block)s_get_%(field)s(%(union)s_t %(union)s) {
|
|
%(type)s ret;
|
|
%(assert)s(((%(union)s.words[%(tagindex)d] >> %(tagshift)d) & 0x%(tagmask)x) ==
|
|
%(union)s_%(block)s);
|
|
|
|
ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
|
|
/* Possibly sign extend */
|
|
if (%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))) {
|
|
ret |= 0x%(high_bits)x;
|
|
}
|
|
return ret;
|
|
}"""
|
|
|
|
ptr_union_reader_template = \
|
|
"""%(inline)s %(type)s PURE
|
|
%(union)s_%(block)s_ptr_get_%(field)s(%(union)s_t *%(union)s_ptr) {
|
|
%(type)s ret;
|
|
%(assert)s(((%(union)s_ptr->words[%(tagindex)d] >> """ \
|
|
"""%(tagshift)d) & 0x%(tagmask)x) ==
|
|
%(union)s_%(block)s);
|
|
|
|
ret = (%(union)s_ptr->words[%(index)d] & 0x%(mask)x%(suf)s) """ \
|
|
"""%(r_shift_op)s %(shift)d;
|
|
/* Possibly sign extend */
|
|
if (%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))) {
|
|
ret |= 0x%(high_bits)x;
|
|
}
|
|
return ret;
|
|
}"""
|
|
|
|
union_writer_template = \
|
|
"""%(inline)s %(union)s_t CONST
|
|
%(union)s_%(block)s_set_%(field)s(%(union)s_t %(union)s, %(type)s v%(base)d) {
|
|
%(assert)s(((%(union)s.words[%(tagindex)d] >> %(tagshift)d) & 0x%(tagmask)x) ==
|
|
%(union)s_%(block)s);
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
|
|
%(union)s.words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
|
|
return %(union)s;
|
|
}"""
|
|
|
|
ptr_union_writer_template = \
|
|
"""%(inline)s void
|
|
%(union)s_%(block)s_ptr_set_%(field)s(%(union)s_t *%(union)s_ptr,
|
|
%(type)s v%(base)d) {
|
|
%(assert)s(((%(union)s_ptr->words[%(tagindex)d] >> """ \
|
|
"""%(tagshift)d) & 0x%(tagmask)x) ==
|
|
%(union)s_%(block)s);
|
|
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
|
|
%(union)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(union)s_ptr->words[%(index)d] |= """ \
|
|
"""(v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
|
|
}"""
|
|
|
|
tag_reader_header_template = \
|
|
"""%(inline)s %(type)s CONST
|
|
%(union)s_get_%(tagname)s(%(union)s_t %(union)s) {
|
|
"""
|
|
|
|
tag_reader_entry_template = \
|
|
""" if ((%(union)s.words[%(index)d] & 0x%(classmask)x) != 0x%(classmask)x)
|
|
return (%(union)s.words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s;
|
|
"""
|
|
|
|
tag_reader_final_template = \
|
|
""" return (%(union)s.words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s;"""
|
|
|
|
tag_reader_footer_template = \
|
|
"""
|
|
}"""
|
|
|
|
tag_eq_reader_header_template = \
|
|
"""%(inline)s int CONST
|
|
%(union)s_%(tagname)s_equals(%(union)s_t %(union)s, %(type)s %(union)s_type_tag) {
|
|
"""
|
|
|
|
tag_eq_reader_entry_template = \
|
|
""" if ((%(union)s_type_tag & 0x%(classmask)x) != 0x%(classmask)x)
|
|
return ((%(union)s.words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s) == %(union)s_type_tag;
|
|
"""
|
|
|
|
tag_eq_reader_final_template = \
|
|
""" return ((%(union)s.words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s) == %(union)s_type_tag;"""
|
|
|
|
tag_eq_reader_footer_template = \
|
|
"""
|
|
}"""
|
|
|
|
ptr_tag_reader_header_template = \
|
|
"""%(inline)s %(type)s PURE
|
|
%(union)s_ptr_get_%(tagname)s(%(union)s_t *%(union)s_ptr) {
|
|
"""
|
|
|
|
ptr_tag_reader_entry_template = \
|
|
""" if ((%(union)s_ptr->words[%(index)d] & 0x%(classmask)x) != 0x%(classmask)x)
|
|
return (%(union)s_ptr->words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s;
|
|
"""
|
|
|
|
ptr_tag_reader_final_template = \
|
|
""" return (%(union)s_ptr->words[%(index)d] >> %(shift)d) & 0x%(mask)x%(suf)s;"""
|
|
|
|
ptr_tag_reader_footer_template = \
|
|
"""
|
|
}"""
|
|
|
|
tag_writer_template = \
|
|
"""%(inline)s %(union)s_t CONST
|
|
%(union)s_set_%(tagname)s(%(union)s_t %(union)s, %(type)s v%(base)d) {
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
|
|
%(union)s.words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(union)s.words[%(index)d] |= (v%(base)d << %(shift)d) & 0x%(mask)x%(suf)s;
|
|
return %(union)s;
|
|
}"""
|
|
|
|
ptr_tag_writer_template = \
|
|
"""%(inline)s void
|
|
%(union)s_ptr_set_%(tagname)s(%(union)s_t *%(union)s_ptr, %(type)s v%(base)d) {
|
|
/* fail if user has passed bits that we will override */
|
|
%(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
|
|
|
|
%(union)s_ptr->words[%(index)d] &= ~0x%(mask)x%(suf)s;
|
|
%(union)s_ptr->words[%(index)d] |= (v%(base)d << %(shift)d) & 0x%(mask)x%(suf)s;
|
|
}"""
|
|
|
|
# HOL definition templates
|
|
|
|
lift_def_template = \
|
|
'''definition
|
|
%(name)s_lift :: "%(name)s_C \<Rightarrow> %(name)s_CL"
|
|
where
|
|
"%(name)s_lift %(name)s \<equiv> \<lparr>
|
|
%(fields)s \<rparr>"'''
|
|
|
|
block_lift_def_template = \
|
|
'''definition %(union)s_%(block)s_lift :: ''' \
|
|
'''"%(union)s_C \<Rightarrow> %(union)s_%(block)s_CL"
|
|
where
|
|
"%(union)s_%(block)s_lift %(union)s \<equiv>
|
|
case (%(union)s_lift %(union)s) of ''' \
|
|
'''Some (%(generator)s rec) \<Rightarrow> rec"'''
|
|
|
|
block_lift_lemma_template = \
|
|
'''lemma %(union)s_%(block)s_lift:
|
|
"(%(union)s_get_tag c = scast %(union)s_%(block)s) = ''' \
|
|
'''(%(union)s_lift c = Some (%(generator)s (%(union)s_%(block)s_lift c)))"
|
|
unfolding %(union)s_lift_def %(union)s_%(block)s_lift_def
|
|
by (clarsimp simp: %(union)s_tag_defs Let_def)'''
|
|
|
|
union_get_tag_def_header_template = \
|
|
'''definition
|
|
%(name)s_get_tag :: "%(name)s_C \<Rightarrow> word%(base)d"
|
|
where
|
|
"%(name)s_get_tag %(name)s \<equiv>
|
|
'''
|
|
|
|
union_get_tag_def_entry_template = \
|
|
'''if ((index (%(name)s_C.words_C %(name)s) %(tag_index)d)''' \
|
|
''' AND 0x%(classmask)x \<noteq> 0x%(classmask)x)
|
|
then ((index (%(name)s_C.words_C %(name)s) %(tag_index)d)'''\
|
|
''' >> %(tag_shift)d) AND mask %(tag_size)d
|
|
else '''
|
|
|
|
union_get_tag_def_final_template = \
|
|
'''((index (%(name)s_C.words_C %(name)s) %(tag_index)d)'''\
|
|
''' >> %(tag_shift)d) AND mask %(tag_size)d'''
|
|
|
|
union_get_tag_def_footer_template = '''"'''
|
|
|
|
union_get_tag_eq_x_def_header_template = \
|
|
'''lemma %(name)s_get_tag_eq_x:
|
|
"(%(name)s_get_tag c = x) = (('''
|
|
|
|
union_get_tag_eq_x_def_entry_template = \
|
|
'''if ((x << %(tag_shift)d) AND 0x%(classmask)x \<noteq> 0x%(classmask)x)
|
|
then ((index (%(name)s_C.words_C c) %(tag_index)d)''' \
|
|
''' >> %(tag_shift)d) AND mask %(tag_size)d
|
|
else '''
|
|
|
|
union_get_tag_eq_x_def_final_template = \
|
|
'''((index (%(name)s_C.words_C c) %(tag_index)d)''' \
|
|
''' >> %(tag_shift)d) AND mask %(tag_size)d'''
|
|
|
|
union_get_tag_eq_x_def_footer_template = ''') = x)"
|
|
by (auto simp add: %(name)s_get_tag_def mask_def word_bw_assocs)'''
|
|
|
|
union_tag_mask_helpers_header_template = \
|
|
'''lemma %(name)s_%(block)s_tag_mask_helpers:'''
|
|
|
|
union_tag_mask_helpers_entry_template = '''
|
|
"w && %(full_mask)s = %(full_value)s \<Longrightarrow> w'''\
|
|
''' && %(part_mask)s = %(part_value)s"
|
|
'''
|
|
|
|
union_tag_mask_helpers_footer_template = \
|
|
''' by (auto elim: word_sub_mask simp: mask_def)'''
|
|
|
|
union_lift_def_template = \
|
|
'''definition
|
|
%(name)s_lift :: "%(name)s_C \<Rightarrow> %(name)s_CL option"
|
|
where
|
|
"%(name)s_lift %(name)s \<equiv>
|
|
(let tag = %(name)s_get_tag %(name)s in
|
|
%(tag_cases)s
|
|
else None)"'''
|
|
|
|
union_access_def_template = \
|
|
'''definition
|
|
%(union)s_%(block)s_access :: "(%(union)s_%(block)s_CL \<Rightarrow> 'a)
|
|
\<Rightarrow> %(union)s_CL \<Rightarrow> 'a"
|
|
where
|
|
"%(union)s_%(block)s_access f %(union)s \<equiv>
|
|
(case %(union)s of %(generator)s rec \<Rightarrow> f rec)"'''
|
|
|
|
union_update_def_template = \
|
|
'''definition
|
|
%(union)s_%(block)s_update :: "(%(union)s_%(block)s_CL \<Rightarrow>''' \
|
|
''' %(union)s_%(block)s_CL) \<Rightarrow>
|
|
%(union)s_CL \<Rightarrow> %(union)s_CL"
|
|
where
|
|
"%(union)s_%(block)s_update f %(union)s \<equiv>
|
|
(case %(union)s of %(generator)s rec \<Rightarrow>
|
|
%(generator)s (f rec))"'''
|
|
|
|
# HOL proof templates
|
|
|
|
# FIXME: avoid [simp]
|
|
struct_lemmas_template = \
|
|
'''
|
|
lemmas %(name)s_ptr_guards[simp] =
|
|
%(name)s_ptr_words_NULL
|
|
%(name)s_ptr_words_aligned
|
|
%(name)s_ptr_words_ptr_safe'''
|
|
|
|
# FIXME: move to global theory
|
|
defs_global_lemmas = '''
|
|
lemma word_sub_mask:
|
|
"\<lbrakk> w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \<rbrakk>
|
|
\<Longrightarrow> w && m2 = v2"
|
|
by (clarsimp simp: word_bw_assocs)
|
|
'''
|
|
|
|
# Proof templates are stored as a list of
|
|
# (header, body, stuff to go afterwards).
|
|
# This makes it easy to replace the proof body with a sorry.
|
|
|
|
# ptrname should be a function of s
|
|
|
|
|
|
def ptr_basic_template(name, ptrname, retval, args, post):
|
|
return ('''lemma (in ''' + loc_name + ''') %(name)s_ptr_''' + name + '''_spec:
|
|
defines "ptrval s \<equiv> cslift s ''' + ptrname + '''"
|
|
shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ''' + ptrname + '''\<rbrace>
|
|
''' + retval + '''PROC %(name)s_ptr_''' + name + '''(\<acute>%(name)s_ptr''' + args + ''')
|
|
''' + post + ''' " ''')
|
|
|
|
|
|
def ptr_union_basic_template(name, ptrname, retval, args, pre, post):
|
|
return ('''lemma (in ''' + loc_name + ''') %(name)s_%(block)s_ptr_''' + name + '''_spec:
|
|
defines "ptrval s \<equiv> cslift s ''' + ptrname + '''"
|
|
shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ''' + ptrname + " " + pre + '''\<rbrace>
|
|
''' + retval + '''PROC %(name)s_%(block)s_ptr_''' + name + '''(\<acute>%(name)s_ptr''' + args + ''')
|
|
''' + post + ''' " ''')
|
|
|
|
|
|
direct_ptr_name = '\<^bsup>s\<^esup>%(name)s_ptr'
|
|
path_ptr_name = '(cparent \<^bsup>s\<^esup>%(name)s_ptr [%(path)s] :: %(toptp)s ptr)'
|
|
|
|
|
|
def ptr_get_template(ptrname):
|
|
return ptr_basic_template('get_%(field)s', ptrname, '\<acute>%(ret_name)s :== ', '',
|
|
'''\<lbrace>\<acute>%(ret_name)s = '''
|
|
'''%(name)s_CL.%(field)s_CL '''
|
|
'''(%(name)s_lift (%(access_path)s))\<rbrace>''')
|
|
|
|
|
|
def ptr_set_template(name, ptrname):
|
|
return ptr_basic_template(name, ptrname, '', ', \<acute>v%(base)d',
|
|
'''{t. \<exists>%(name)s.
|
|
%(name)s_lift %(name)s =
|
|
%(name)s_lift (%(access_path)s) \<lparr> %(name)s_CL.%(field)s_CL '''
|
|
''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr> \<and>
|
|
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
|
(''' + ptrname + ''')
|
|
%(update_path)s)
|
|
(t_hrs_' (globals s))
|
|
}''')
|
|
|
|
|
|
def ptr_new_template(ptrname):
|
|
return ptr_basic_template('new', ptrname, '', ', %(args)s',
|
|
'''{t. \<exists>%(name)s. %(name)s_lift %(name)s = \<lparr>
|
|
%(field_eqs)s \<rparr> \<and>
|
|
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
|
(''' + ptrname + ''')
|
|
%(update_path)s)
|
|
(t_hrs_' (globals s))
|
|
}''')
|
|
|
|
|
|
def ptr_get_tag_template(ptrname):
|
|
return ptr_basic_template('get_%(tagname)s', ptrname, '\<acute>%(ret_name)s :== ', '',
|
|
'''\<lbrace>\<acute>%(ret_name)s = %(name)s_get_tag (%(access_path)s)\<rbrace>''')
|
|
|
|
|
|
def ptr_empty_union_new_template(ptrname):
|
|
return ptr_union_basic_template('new', ptrname, '', '', '',
|
|
'''{t. \<exists>%(name)s. '''
|
|
'''%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \<and>
|
|
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
|
(''' + ptrname + ''')
|
|
%(update_path)s)
|
|
(t_hrs_' (globals s))
|
|
}''')
|
|
|
|
|
|
def ptr_union_new_template(ptrname):
|
|
return ptr_union_basic_template('new', ptrname, '', ', %(args)s', '',
|
|
'''{t. \<exists>%(name)s. '''
|
|
'''%(name)s_%(block)s_lift %(name)s = \<lparr>
|
|
%(field_eqs)s \<rparr> \<and>
|
|
%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \<and>
|
|
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
|
(''' + ptrname + ''')
|
|
%(update_path)s)
|
|
(t_hrs_' (globals s))
|
|
}''')
|
|
|
|
|
|
def ptr_union_get_template(ptrname):
|
|
return ptr_union_basic_template('get_%(field)s', ptrname,
|
|
'\<acute>%(ret_name)s :== ', '',
|
|
'\<and> %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s',
|
|
'''\<lbrace>\<acute>%(ret_name)s = '''
|
|
'''%(name)s_%(block)s_CL.%(field)s_CL '''
|
|
'''(%(name)s_%(block)s_lift %(access_path)s)\<rbrace>''')
|
|
|
|
|
|
def ptr_union_set_template(ptrname):
|
|
return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \<acute>v%(base)d',
|
|
'\<and> %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s',
|
|
'''{t. \<exists>%(name)s. '''
|
|
'''%(name)s_%(block)s_lift %(name)s =
|
|
%(name)s_%(block)s_lift %(access_path)s '''
|
|
'''\<lparr> %(name)s_%(block)s_CL.%(field)s_CL '''
|
|
''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr> \<and>
|
|
%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \<and>
|
|
t_hrs_' (globals t) = hrs_mem_update (heap_update
|
|
(''' + ptrname + ''')
|
|
%(update_path)s)
|
|
(t_hrs_' (globals s))
|
|
}''')
|
|
|
|
|
|
proof_templates = {
|
|
|
|
'lift_collapse_proof': [
|
|
'''lemma %(name)s_lift_%(block)s:
|
|
"%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \<Longrightarrow>
|
|
%(name)s_lift %(name)s =
|
|
Some (%(value)s)"''',
|
|
''' apply(simp add:%(name)s_lift_def %(name)s_tag_defs)
|
|
done'''],
|
|
|
|
'words_NULL_proof': [
|
|
'''lemma %(name)s_ptr_words_NULL:
|
|
"c_guard (p::%(name)s_C ptr) \<Longrightarrow>
|
|
0 < &(p\<rightarrow>[''words_C''])"''',
|
|
''' apply(fastforce intro:c_guard_NULL_fl simp:typ_uinfo_t_def)
|
|
done'''],
|
|
|
|
'words_aligned_proof': [
|
|
'''lemma %(name)s_ptr_words_aligned:
|
|
"c_guard (p::%(name)s_C ptr) \<Longrightarrow>
|
|
ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::'''
|
|
'''((word%(base)d[%(words)d]) ptr))"''',
|
|
''' apply(fastforce intro:c_guard_ptr_aligned_fl simp:typ_uinfo_t_def)
|
|
done'''],
|
|
|
|
'words_ptr_safe_proof': [
|
|
'''lemma %(name)s_ptr_words_ptr_safe:
|
|
"ptr_safe (p::%(name)s_C ptr) d \<Longrightarrow>
|
|
ptr_safe (Ptr &(p\<rightarrow>[''words_C''])::'''
|
|
'''((word%(base)d[%(words)d]) ptr)) d"''',
|
|
''' apply(fastforce intro:ptr_safe_mono simp:typ_uinfo_t_def)
|
|
done'''],
|
|
|
|
'get_tag_fun_spec_proof': [
|
|
'''lemma (in ''' + loc_name + ''') fun_spec:
|
|
"\<Gamma> \<turnstile> {\<sigma>}
|
|
\<acute>ret__%(rtype)s :== PROC %(name)s_get_%(tag_name)s('''
|
|
''' \<acute>%(name))
|
|
\<lbrace>\<acute>ret__%(rtype)s = %(name)s_get_tag'''
|
|
'''\<^bsup>\<sigma>\<^esup>\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(simp add:$(name)s_get_tag_def word_sle_def
|
|
mask_def ucast_def)
|
|
done'''],
|
|
|
|
'const_modifies_proof': [
|
|
'''lemma (in ''' + loc_name + ''') %(fun_name)s_modifies:
|
|
"\<forall> s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
|
|
PROC %(fun_name)s(%(args)s)
|
|
{t. t may_not_modify_globals s}"''',
|
|
''' by (vcg spec=modifies strip_guards=true)'''],
|
|
|
|
'ptr_set_modifies_proof': [
|
|
'''lemma (in ''' + loc_name + ''') %(fun_name)s_modifies:
|
|
"\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s}
|
|
PROC %(fun_name)s(%(args)s)
|
|
{t. t may_only_modify_globals s in [t_hrs]}"''',
|
|
''' by (vcg spec=modifies strip_guards=true)'''],
|
|
|
|
|
|
'new_spec': [
|
|
'''lemma (in ''' + loc_name + ''') %(name)s_new_spec:
|
|
"\<forall> s. \<Gamma> \<turnstile> {s}
|
|
\<acute>ret__struct_%(name)s_C :== PROC %(name)s_new(%(args)s)
|
|
\<lbrace> %(name)s_lift \<acute>ret__struct_%(name)s_C = \<lparr>
|
|
%(field_eqs)s \<rparr> \<rbrace>"''',
|
|
''' apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp simp: guard_simps)
|
|
apply (simp add: %(name)s_lift_def)
|
|
apply ((intro conjI sign_extend_eq)?;
|
|
(simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs word_and_max_simps)?)
|
|
done'''],
|
|
|
|
'ptr_new_spec_direct': [
|
|
ptr_new_template(direct_ptr_name),
|
|
'''sorry (* ptr_new_spec_direct *)'''],
|
|
|
|
'ptr_new_spec_path': [
|
|
ptr_new_template(path_ptr_name),
|
|
'''sorry (* ptr_new_spec_path *)'''],
|
|
|
|
|
|
'get_spec': [
|
|
'''lemma (in ''' + loc_name + ''') %(name)s_get_%(field)s_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>%(ret_name)s :== '''
|
|
'''PROC %(name)s_get_%(field)s(\<acute>%(name)s)
|
|
\<lbrace>\<acute>%(ret_name)s = '''
|
|
'''%(name)s_CL.%(field)s_CL '''
|
|
'''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\<rbrace>"''',
|
|
''' apply (rule allI, rule conseqPre, vcg)
|
|
apply clarsimp
|
|
apply (simp add: %(name)s_lift_def mask_shift_simps guard_simps)
|
|
apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
|
|
shift_over_ao_dists word_oa_dist word_and_max_simps)?
|
|
done'''],
|
|
|
|
'set_spec': [
|
|
'''lemma (in ''' + loc_name + ''') %(name)s_set_%(field)s_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>ret__struct_%(name)s_C :== '''
|
|
'''PROC %(name)s_set_%(field)s(\<acute>%(name)s, \<acute>v%(base)d)
|
|
\<lbrace>%(name)s_lift \<acute>ret__struct_%(name)s_C = '''
|
|
'''%(name)s_lift \<^bsup>s\<^esup>%(name)s \<lparr> '''
|
|
'''%(name)s_CL.%(field)s_CL '''
|
|
''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \<rparr>\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp simp: guard_simps ucast_id
|
|
%(name)s_lift_def
|
|
mask_def shift_over_ao_dists
|
|
multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs
|
|
NOT_eq)
|
|
apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
|
|
shift_over_ao_dists word_and_max_simps)?
|
|
done'''],
|
|
|
|
# where the top level type is the bitfield type --- these are split because they have different proofs
|
|
'ptr_get_spec_direct': [
|
|
ptr_get_template(direct_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp simp: h_t_valid_clift_Some_iff)
|
|
apply (simp add: %(name)s_lift_def guard_simps mask_def typ_heap_simps ucast_def)
|
|
apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
|
|
shift_over_ao_dists word_oa_dist word_and_max_simps)?
|
|
done'''],
|
|
|
|
'ptr_get_spec_path': [
|
|
ptr_get_template(path_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp simp: guard_simps)
|
|
apply (frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp)
|
|
apply (frule clift_subtype, simp, simp, simp)
|
|
apply (simp add: h_val_field_clift' typ_heap_simps)
|
|
apply (simp add: thread_state_lift_def)
|
|
apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
|
|
shift_over_ao_dists word_oa_dist word_and_max_simps)?
|
|
apply (simp add: mask_shift_simps)?
|
|
done'''],
|
|
|
|
'ptr_set_spec_direct': [
|
|
ptr_set_template('set_%(field)s', direct_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp simp: guard_simps)
|
|
apply (clarsimp simp add: packed_heap_update_collapse_hrs typ_heap_simps)?
|
|
apply (rule exI, rule conjI[rotated], rule refl)
|
|
apply (clarsimp simp: h_t_valid_clift_Some_iff %(name)s_lift_def typ_heap_simps)
|
|
apply ((intro conjI sign_extend_eq)?;
|
|
(simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs word_and_max_simps))?
|
|
done'''],
|
|
|
|
'ptr_set_spec_path': [
|
|
ptr_set_template('set_%(field)s', path_ptr_name),
|
|
''' (* Invoke vcg *)
|
|
unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp)
|
|
|
|
(* Infer h_t_valid for all three levels of indirection *)
|
|
apply (frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply (frule h_t_valid_c_guard_field[where f="[''words_C'']"],
|
|
simp, simp add: typ_uinfo_t_def)
|
|
|
|
(* Discharge guards, including c_guard for pointers *)
|
|
apply (simp add: h_t_valid_c_guard guard_simps)
|
|
|
|
(* Lift field updates to bitfield struct updates *)
|
|
apply (simp add: heap_update_field_hrs h_t_valid_c_guard typ_heap_simps)
|
|
|
|
(* Collapse multiple updates *)
|
|
apply(simp add: packed_heap_update_collapse_hrs)
|
|
|
|
(* Instantiate the toplevel object *)
|
|
apply(frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp)
|
|
|
|
(* Instantiate the next-level object in terms of the last *)
|
|
apply(frule clift_subtype, simp+)
|
|
|
|
(* Resolve pointer accesses *)
|
|
apply(simp add: h_val_field_clift')
|
|
|
|
(* Rewrite bitfield struct updates as enclosing struct updates *)
|
|
apply(frule h_t_valid_c_guard)
|
|
apply(simp add: parent_update_child)
|
|
|
|
(* Equate the updated values *)
|
|
apply(rule exI, rule conjI[rotated], simp add: h_val_clift')
|
|
|
|
(* Rewrite struct updates *)
|
|
apply(simp add: o_def %(name)s_lift_def)
|
|
|
|
(* Solve bitwise arithmetic *)
|
|
apply ((intro conjI sign_extend_eq)?;
|
|
(simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs word_and_max_simps))?
|
|
done'''],
|
|
|
|
|
|
'get_tag_spec': [
|
|
'''lemma (in ''' + loc_name + ''') %(name)s_get_%(tagname)s_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>%(ret_name)s :== ''' \
|
|
'''PROC %(name)s_get_%(tagname)s(\<acute>%(name)s)
|
|
\<lbrace>\<acute>%(ret_name)s = ''' \
|
|
'''%(name)s_get_tag \<^bsup>s\<^esup>%(name)s\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(simp add:%(name)s_get_tag_def
|
|
mask_shift_simps
|
|
guard_simps)
|
|
done'''],
|
|
|
|
'get_tag_equals_spec': [
|
|
'''lemma (in ''' + loc_name + ''') %(name)s_%(tagname)s_equals_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>ret__int :==
|
|
PROC %(name)s_%(tagname)s_equals(\<acute>%(name)s, \<acute>%(name)s_type_tag)
|
|
\<lbrace>\<acute>ret__int = of_bl [%(name)s_get_tag \<^bsup>s\<^esup>%(name)s = \<^bsup>s\<^esup>%(name)s_type_tag]\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(simp add:%(name)s_get_tag_eq_x
|
|
mask_shift_simps
|
|
guard_simps)
|
|
done'''],
|
|
|
|
'ptr_get_tag_spec_direct': [
|
|
ptr_get_tag_template(direct_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp simp:guard_simps)
|
|
apply(frule h_t_valid_field[where f="[''words_C'']"], simp+)
|
|
apply(frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp)
|
|
apply(simp add:h_val_clift' clift_field)
|
|
apply(simp add:%(name)s_get_tag_def)
|
|
apply(simp add:mask_shift_simps)
|
|
done'''],
|
|
|
|
'ptr_get_tag_spec_path': [
|
|
ptr_get_tag_template(path_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply(clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff)
|
|
apply(frule clift_subtype, simp+)
|
|
apply(simp add: %(name)s_get_tag_def mask_shift_simps guard_simps)
|
|
done'''],
|
|
|
|
|
|
'empty_union_new_spec': [
|
|
'''lemma (in ''' + loc_name + ''') ''' \
|
|
'''%(name)s_%(block)s_new_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>ret__struct_%(name)s_C :== ''' \
|
|
'''PROC %(name)s_%(block)s_new()
|
|
\<lbrace>%(name)s_get_tag \<acute>ret__struct_%(name)s_C = ''' \
|
|
'''scast %(name)s_%(block)s\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp simp:guard_simps
|
|
%(name)s_lift_def
|
|
Let_def
|
|
%(name)s_get_tag_def
|
|
mask_shift_simps
|
|
%(name)s_tag_defs
|
|
word_of_int_hom_syms)
|
|
done'''],
|
|
|
|
'union_new_spec': [
|
|
'''lemma (in ''' + loc_name + ''') ''' \
|
|
'''%(name)s_%(block)s_new_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> {s}
|
|
\<acute>ret__struct_%(name)s_C :== ''' \
|
|
'''PROC %(name)s_%(block)s_new(%(args)s)
|
|
\<lbrace>%(name)s_%(block)s_lift ''' \
|
|
'''\<acute>ret__struct_%(name)s_C = \<lparr>
|
|
%(field_eqs)s \<rparr> \<and>
|
|
%(name)s_get_tag \<acute>ret__struct_%(name)s_C = ''' \
|
|
'''scast %(name)s_%(block)s\<rbrace>"''',
|
|
''' apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists)
|
|
apply (rule context_conjI[THEN iffD1[OF conj_commute]],
|
|
fastforce simp: %(name)s_get_tag_eq_x %(name)s_%(block)s_def
|
|
mask_def shift_over_ao_dists word_bw_assocs word_ao_dist)
|
|
apply (simp add: %(name)s_%(block)s_lift_def)
|
|
apply (erule %(name)s_lift_%(block)s[THEN subst[OF sym]]; simp?)
|
|
apply ((intro conjI sign_extend_eq)?;
|
|
(simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs word_and_max_simps))?
|
|
done'''],
|
|
|
|
'ptr_empty_union_new_spec_direct': [
|
|
ptr_empty_union_new_template(direct_ptr_name),
|
|
'''sorry (* ptr_empty_union_new_spec_direct *)'''],
|
|
|
|
'ptr_empty_union_new_spec_path': [
|
|
ptr_empty_union_new_template(path_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply(clarsimp simp: h_t_valid_clift_Some_iff)
|
|
apply(frule clift_subtype, simp+)
|
|
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)
|
|
|
|
apply(simp add: o_def, rule exI, rule conjI[OF _ refl])
|
|
|
|
apply(simp add: %(name)s_get_tag_def %(name)s_tag_defs
|
|
guard_simps mask_shift_simps)
|
|
done
|
|
'''],
|
|
|
|
'ptr_union_new_spec_direct': [
|
|
ptr_union_new_template(direct_ptr_name),
|
|
'''sorry (* ptr_union_new_spec_direct *)'''],
|
|
|
|
'ptr_union_new_spec_path': [
|
|
ptr_union_new_template(path_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp)
|
|
apply (frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply (drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
|
|
apply (frule clift_subtype, simp, simp)
|
|
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)
|
|
apply (simp add: o_def %(name)s_%(block)s_lift_def)
|
|
apply (simp only: %(name)s_lift_%(block)s cong: rev_conj_cong)
|
|
apply (rule exI, rule conjI[rotated], rule conjI[OF _ refl])
|
|
apply (simp_all add: %(name)s_get_tag_eq_x %(name)s_tag_defs mask_shift_simps)
|
|
apply (intro conjI sign_extend_eq; simp add: mask_def word_ao_dist word_bw_assocs)?
|
|
done'''],
|
|
|
|
'union_get_spec': [
|
|
'''lemma (in ''' + loc_name + ''') ''' \
|
|
'''%(name)s_%(block)s_get_%(field)s_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> ''' \
|
|
'''\<lbrace>s. %(name)s_get_tag \<acute>%(name)s = ''' \
|
|
'''scast %(name)s_%(block)s\<rbrace>
|
|
\<acute>%(ret_name)s :== ''' \
|
|
'''PROC %(name)s_%(block)s_get_%(field)s(\<acute>%(name)s)
|
|
\<lbrace>\<acute>%(ret_name)s = ''' \
|
|
'''%(name)s_%(block)s_CL.%(field)s_CL ''' \
|
|
'''(%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s)''' \
|
|
'''\<rbrace>"''',
|
|
''' apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp simp:guard_simps)
|
|
apply(simp add:%(name)s_%(block)s_lift_def)
|
|
apply(subst %(name)s_lift_%(block)s)
|
|
apply(simp add:o_def
|
|
%(name)s_get_tag_def
|
|
%(name)s_%(block)s_def
|
|
mask_def
|
|
word_size
|
|
shift_over_ao_dists)
|
|
apply(subst %(name)s_lift_%(block)s, simp)?
|
|
apply(simp add:o_def
|
|
%(name)s_get_tag_def
|
|
%(name)s_%(block)s_def
|
|
mask_def
|
|
word_size
|
|
shift_over_ao_dists
|
|
multi_shift_simps
|
|
word_bw_assocs
|
|
word_oa_dist
|
|
word_and_max_simps
|
|
ucast_def
|
|
sign_extend_def'
|
|
nth_is_and_neq_0)
|
|
done'''],
|
|
|
|
'union_set_spec': [
|
|
'''lemma (in ''' + loc_name + ''') ''' \
|
|
'''%(name)s_%(block)s_set_%(field)s_spec:
|
|
"\<forall>s. \<Gamma> \<turnstile> ''' \
|
|
'''\<lbrace>s. %(name)s_get_tag \<acute>%(name)s = ''' \
|
|
'''scast %(name)s_%(block)s\<rbrace>
|
|
\<acute>ret__struct_%(name)s_C :== ''' \
|
|
'''PROC %(name)s_%(block)s_set_%(field)s(\<acute>%(name)s, \<acute>v%(base)d)
|
|
\<lbrace>%(name)s_%(block)s_lift \<acute>ret__struct_%(name)s_C = ''' \
|
|
'''%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s \<lparr> ''' \
|
|
'''%(name)s_%(block)s_CL.%(field)s_CL ''' \
|
|
''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s)\<rparr> \<and>
|
|
%(name)s_get_tag \<acute>ret__struct_%(name)s_C = ''' \
|
|
'''scast %(name)s_%(block)s\<rbrace>"''',
|
|
''' apply (rule allI, rule conseqPre, vcg)
|
|
apply clarsimp
|
|
apply (rule context_conjI[THEN iffD1[OF conj_commute]],
|
|
fastforce simp: %(name)s_get_tag_eq_x %(name)s_lift_def %(name)s_tag_defs
|
|
mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs)
|
|
apply (simp add: %(name)s_%(block)s_lift_def %(name)s_lift_def %(name)s_tag_defs)
|
|
apply ((intro conjI sign_extend_eq)?;
|
|
(simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
|
|
word_ao_dist word_bw_assocs word_and_max_simps))?
|
|
done'''],
|
|
|
|
'ptr_union_get_spec_direct': [
|
|
ptr_union_get_template(direct_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff guard_simps
|
|
mask_shift_simps sign_extend_def' nth_is_and_neq_0
|
|
%(name)s_lift_%(block)s %(name)s_%(block)s_lift_def)
|
|
done
|
|
'''],
|
|
|
|
'ptr_union_get_spec_path': [
|
|
ptr_union_get_template(path_ptr_name),
|
|
'''unfolding ptrval_def
|
|
apply(rule allI, rule conseqPre, vcg)
|
|
apply(clarsimp)
|
|
apply(frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply(drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
|
|
apply(frule clift_subtype, simp, simp)
|
|
apply(clarsimp simp: typ_heap_simps c_guard_clift)
|
|
apply(simp add: guard_simps mask_shift_simps)
|
|
apply(simp add:%(name)s_%(block)s_lift_def)
|
|
apply(subst %(name)s_lift_%(block)s)
|
|
apply(simp add: mask_def)+
|
|
done
|
|
(* ptr_union_get_spec_path *)'''],
|
|
|
|
'ptr_union_set_spec_direct': [
|
|
ptr_union_set_template(direct_ptr_name),
|
|
'''sorry (* ptr_union_set_spec_direct *)'''],
|
|
|
|
|
|
'ptr_union_set_spec_path': [
|
|
ptr_union_set_template(path_ptr_name),
|
|
''' unfolding ptrval_def
|
|
apply (rule allI, rule conseqPre, vcg)
|
|
apply (clarsimp)
|
|
apply (frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def)
|
|
apply (drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE)
|
|
apply (frule clift_subtype, simp, simp)
|
|
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)
|
|
apply (simp add: o_def %(name)s_%(block)s_lift_def)
|
|
apply (simp only: %(name)s_lift_%(block)s cong: rev_conj_cong)
|
|
apply (rule exI, rule conjI[rotated], rule conjI[OF _ refl])
|
|
apply (simp_all add: %(name)s_get_tag_eq_x %(name)s_tag_defs mask_shift_simps)
|
|
apply (intro conjI sign_extend_eq; simp add: mask_def word_ao_dist word_bw_assocs)?
|
|
done'''],
|
|
|
|
}
|
|
|
|
|
|
def make_proof(name, substs, sorry=False):
|
|
result = proof_templates[name][0] % substs + '\n'
|
|
|
|
if sorry:
|
|
result += '\nsorry'
|
|
else:
|
|
result += proof_templates[name][1] % substs
|
|
|
|
if len(proof_templates[name]) > 2:
|
|
result += '\n' + '\n'.join(proof_templates[name][2:]) % substs
|
|
|
|
return result
|
|
|
|
# AST objects
|
|
|
|
|
|
def emit_named(name, params, string):
|
|
# Emit a named definition/proof, only when the given name is in
|
|
# params.names
|
|
|
|
if(name in params.names):
|
|
print(string, file=params.output)
|
|
print(file=params.output)
|
|
|
|
# This calculates substs for each proof, which is probably inefficient. Meh
|
|
|
|
|
|
def emit_named_ptr_proof(fn_name, params, name, type_map, toptps, prf_prefix, substs):
|
|
name_C = name + '_C'
|
|
|
|
if name_C in type_map:
|
|
toptp, path = type_map[name_C]
|
|
|
|
substs['access_path'] = '(' + reduce(lambda x, y: y +
|
|
' (' + x + ')', ['the (ptrval s)'] + path) + ')'
|
|
|
|
if len(path) == 0:
|
|
substs['update_path'] = name
|
|
emit_named(fn_name, params, make_proof(prf_prefix + '_direct', substs, params.sorry))
|
|
else:
|
|
substs['toptp'] = toptp
|
|
# the split here gives us the field name (less any qualifiers) as the typ_heap
|
|
# stuff doesn't use the qualifier
|
|
substs['path'] = ', '.join(map(lambda x: "''%s''" % x.split('.')[-1], path))
|
|
|
|
# The self.name here is the variable name (so not _C)
|
|
path.reverse()
|
|
substs['update_path'] = '(' + reduce(lambda x, y: y + '_update (' + x + ')',
|
|
['\\<lambda>_. ' + name] + path) + '(the (ptrval s))' + ')'
|
|
emit_named(fn_name, params, make_proof(prf_prefix + '_path', substs, params.sorry))
|
|
|
|
|
|
def field_mask_proof(base, base_bits, sign_extend, high, size):
|
|
if high:
|
|
if base_bits == base or sign_extend:
|
|
# equivalent to below, but nicer in proofs
|
|
return "NOT (mask %d)" % (base_bits - size)
|
|
else:
|
|
return "(mask %d << %d)" % (size, base_bits - size)
|
|
else:
|
|
return "mask %d" % size
|
|
|
|
|
|
def sign_extend_proof(high, base_bits, base_sign_extend):
|
|
if high and base_sign_extend:
|
|
return "sign_extend %d " % (base_bits - 1)
|
|
else:
|
|
return ""
|
|
|
|
|
|
def det_values(*dicts):
|
|
"""Deterministically iterate over the values of each dict in `dicts`."""
|
|
def values(d):
|
|
return (d[key] for key in sorted(d.keys()))
|
|
return itertools.chain(*(values(d) for d in dicts))
|
|
|
|
|
|
class TaggedUnion:
|
|
def __init__(self, name, tagname, classes, tags):
|
|
self.name = name
|
|
self.tagname = tagname
|
|
self.constant_suffix = ''
|
|
|
|
# Check for duplicate tags
|
|
used_names = set()
|
|
used_values = set()
|
|
for name, value in tags:
|
|
if name in used_names:
|
|
raise ValueError("Duplicate tag name %s" % name)
|
|
if value in used_values:
|
|
raise ValueError("Duplicate tag value %d" % value)
|
|
|
|
used_names.add(name)
|
|
used_values.add(value)
|
|
self.classes = dict(classes)
|
|
self.tags = tags
|
|
|
|
def resolve(self, params, symtab):
|
|
# Grab block references for tags
|
|
self.tags = [(name, value, symtab[name]) for name, value in self.tags]
|
|
self.make_classes(params)
|
|
|
|
# Ensure that block sizes and tag size & position match for
|
|
# all tags in the union
|
|
union_base = None
|
|
union_size = None
|
|
for name, value, ref in self.tags:
|
|
_tag_offset, _tag_size, _tag_high = ref.field_map[self.tagname]
|
|
|
|
if union_base is None:
|
|
union_base = ref.base
|
|
elif union_base != ref.base:
|
|
raise ValueError("Base mismatch for element %s"
|
|
" of tagged union %s" % (name, self.name))
|
|
|
|
if union_size is None:
|
|
union_size = ref.size
|
|
elif union_size != ref.size:
|
|
raise ValueError("Size mismatch for element %s"
|
|
" of tagged union %s" % (name, self.name))
|
|
|
|
if _tag_offset != self.tag_offset[_tag_size]:
|
|
raise ValueError("Tag offset mismatch for element %s"
|
|
" of tagged union %s" % (name, self.name))
|
|
|
|
self.assert_value_in_class(name, value, _tag_size)
|
|
|
|
if _tag_high:
|
|
raise ValueError("Tag field is high-aligned for element %s"
|
|
" of tagged union %s" % (name, self.name))
|
|
|
|
# Flag block as belonging to a tagged union
|
|
ref.tagged = True
|
|
|
|
self.union_base = union_base
|
|
self.union_size = union_size
|
|
|
|
def set_base(self, base, base_bits, base_sign_extend, suffix):
|
|
self.base = base
|
|
self.multiple = self.union_size // base
|
|
self.constant_suffix = suffix
|
|
self.base_bits = base_bits
|
|
self.base_sign_extend = base_sign_extend
|
|
|
|
tag_index = None
|
|
for w in self.tag_offset:
|
|
tag_offset = self.tag_offset[w]
|
|
|
|
if tag_index is None:
|
|
tag_index = tag_offset // base
|
|
|
|
if (tag_offset // base) != tag_index:
|
|
raise ValueError(
|
|
"The tag field of tagged union %s"
|
|
" is in a different word (%s) to the others (%s)."
|
|
% (self.name, hex(tag_offset // base), hex(tag_index)))
|
|
|
|
def generate_hol_proofs(self, params, type_map):
|
|
output = params.output
|
|
|
|
# Add fixed simp rule for struct
|
|
print("lemmas %(name)s_C_words_C_fl_simp[simp] = "
|
|
"%(name)s_C_words_C_fl[simplified]" %
|
|
{"name": self.name}, file=output)
|
|
print(file=output)
|
|
|
|
# Generate struct field pointer proofs
|
|
substs = {"name": self.name,
|
|
"words": self.multiple,
|
|
"base": self.base}
|
|
|
|
print(make_proof('words_NULL_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
print(make_proof('words_aligned_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
print(make_proof('words_ptr_safe_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
# Generate struct lemmas
|
|
print(struct_lemmas_template % {"name": self.name},
|
|
file=output)
|
|
print(file=output)
|
|
|
|
# Generate get_tag specs
|
|
substs = {"name": self.name,
|
|
"tagname": self.tagname,
|
|
"ret_name": return_name(self.base)}
|
|
|
|
if not params.skip_modifies:
|
|
emit_named("%(name)s_get_%(tagname)s" % substs, params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%(name)s_get_%(tagname)s" % substs,
|
|
"args": ', '.join(["\<acute>ret__unsigned_long",
|
|
"\<acute>%(name)s" % substs])},
|
|
params.sorry))
|
|
emit_named("%(name)s_ptr_get_%(tagname)s" % substs, params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%(name)s_ptr_get_%(tagname)s" % substs,
|
|
"args": ', '.join(["\<acute>ret__unsigned_long",
|
|
"\<acute>%(name)s_ptr" % substs])},
|
|
params.sorry))
|
|
|
|
emit_named("%s_get_%s" % (self.name, self.tagname), params,
|
|
make_proof('get_tag_spec', substs, params.sorry))
|
|
|
|
emit_named("%s_%s_equals" % (self.name, self.tagname), params,
|
|
make_proof('get_tag_equals_spec', substs, params.sorry))
|
|
|
|
# Only generate ptr lemmas for those types reachable from top level types
|
|
emit_named_ptr_proof("%s_ptr_get_%s" % (self.name, self.tagname), params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_get_tag_spec', substs)
|
|
|
|
for name, value, ref in self.tags:
|
|
# Generate struct_new specs
|
|
arg_list = ["\<acute>" + field
|
|
for field in ref.visible_order
|
|
if field != self.tagname]
|
|
|
|
# Generate modifies proof
|
|
if not params.skip_modifies:
|
|
emit_named("%s_%s_new" % (self.name, ref.name), params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_%s_new" %
|
|
(self.name, ref.name),
|
|
"args": ', '.join([
|
|
"\<acute>ret__struct_%(name)s_C" % substs] +
|
|
arg_list)},
|
|
params.sorry))
|
|
|
|
emit_named("%s_%s_ptr_new" % (self.name, ref.name), params,
|
|
make_proof('ptr_set_modifies_proof',
|
|
{"fun_name": "%s_%s_ptr_new" %
|
|
(self.name, ref.name),
|
|
"args": ', '.join([
|
|
"\<acute>ret__struct_%(name)s_C" % substs] +
|
|
arg_list)},
|
|
params.sorry))
|
|
|
|
if len(arg_list) == 0:
|
|
# For an empty block:
|
|
emit_named("%s_%s_new" % (self.name, ref.name), params,
|
|
make_proof('empty_union_new_spec',
|
|
{"name": self.name,
|
|
"block": ref.name},
|
|
params.sorry))
|
|
|
|
emit_named_ptr_proof("%s_%s_ptr_new" % (self.name, ref.name), params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_empty_union_new_spec',
|
|
{"name": self.name,
|
|
"block": ref.name})
|
|
else:
|
|
field_eq_list = []
|
|
for field in ref.visible_order:
|
|
offset, size, high = ref.field_map[field]
|
|
|
|
if field == self.tagname:
|
|
continue
|
|
|
|
mask = field_mask_proof(self.base, self.base_bits,
|
|
self.base_sign_extend, high, size)
|
|
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))
|
|
field_eqs = ',\n '.join(field_eq_list)
|
|
|
|
emit_named("%s_%s_new" % (self.name, ref.name), params,
|
|
make_proof('union_new_spec',
|
|
{"name": self.name,
|
|
"block": ref.name,
|
|
"args": ', '.join(arg_list),
|
|
"field_eqs": field_eqs},
|
|
params.sorry))
|
|
|
|
emit_named_ptr_proof("%s_%s_ptr_new" % (self.name, ref.name), params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_union_new_spec',
|
|
{"name": self.name,
|
|
"block": ref.name,
|
|
"args": ', '.join(arg_list),
|
|
"field_eqs": field_eqs})
|
|
|
|
_, size, _ = ref.field_map[self.tagname]
|
|
if any([w for w in self.widths if w < size]):
|
|
tag_mask_helpers = ("%s_%s_tag_mask_helpers"
|
|
% (self.name, ref.name))
|
|
else:
|
|
tag_mask_helpers = ""
|
|
|
|
# Generate get/set specs
|
|
for (field, offset, size, high) in ref.fields:
|
|
if field == self.tagname:
|
|
continue
|
|
|
|
mask = field_mask_proof(self.base, self.base_bits,
|
|
self.base_sign_extend, high, size)
|
|
sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend)
|
|
|
|
substs = {"name": self.name,
|
|
"block": ref.name,
|
|
"field": field,
|
|
"mask": mask,
|
|
"sign_extend": sign_extend,
|
|
"tag_mask_helpers": tag_mask_helpers,
|
|
"ret_name": return_name(self.base),
|
|
"base": self.base}
|
|
|
|
# Get modifies spec
|
|
if not params.skip_modifies:
|
|
emit_named("%s_%s_get_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_%s_get_%s" %
|
|
(self.name, ref.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__unsigned_long",
|
|
"\<acute>%s" % self.name])},
|
|
params.sorry))
|
|
|
|
emit_named("%s_%s_ptr_get_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_%s_ptr_get_%s" %
|
|
(self.name, ref.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__unsigned_long",
|
|
"\<acute>%s_ptr" % self.name])},
|
|
params.sorry))
|
|
|
|
# Get spec
|
|
emit_named("%s_%s_get_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('union_get_spec', substs, params.sorry))
|
|
|
|
# Set modifies spec
|
|
if not params.skip_modifies:
|
|
emit_named("%s_%s_set_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_%s_set_%s" %
|
|
(self.name, ref.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__struct_%s_C" % self.name,
|
|
"\<acute>%s" % self.name,
|
|
"\<acute>v%(base)d"])},
|
|
params.sorry))
|
|
|
|
emit_named("%s_%s_ptr_set_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('ptr_set_modifies_proof',
|
|
{"fun_name": "%s_%s_ptr_set_%s" %
|
|
(self.name, ref.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>%s_ptr" % self.name,
|
|
"\<acute>v%(base)d"])},
|
|
params.sorry))
|
|
|
|
# Set spec
|
|
emit_named("%s_%s_set_%s" % (self.name, ref.name, field),
|
|
params,
|
|
make_proof('union_set_spec', substs, params.sorry))
|
|
|
|
# Pointer get spec
|
|
emit_named_ptr_proof("%s_%s_ptr_get_%s" % (self.name, ref.name, field),
|
|
params, self.name, type_map, params.toplevel_types,
|
|
'ptr_union_get_spec', substs)
|
|
|
|
# Pointer set spec
|
|
emit_named_ptr_proof("%s_%s_ptr_set_%s" % (self.name, ref.name, field),
|
|
params, self.name, type_map, params.toplevel_types,
|
|
'ptr_union_set_spec', substs)
|
|
|
|
def generate_hol_defs(self, params):
|
|
output = params.output
|
|
|
|
empty_blocks = {}
|
|
|
|
def gen_name(ref_name, capitalise=False):
|
|
# Create datatype generator/type name for a block
|
|
if capitalise:
|
|
return "%s_%s" % \
|
|
(self.name[0].upper() + self.name[1:], ref_name)
|
|
else:
|
|
return "%s_%s" % (self.name, ref_name)
|
|
|
|
# Generate block records with tag field removed
|
|
for name, value, ref in self.tags:
|
|
if ref.generate_hol_defs(params,
|
|
suppressed_field=self.tagname,
|
|
prefix="%s_" % self.name,
|
|
in_union=True):
|
|
empty_blocks[ref] = True
|
|
|
|
constructor_exprs = []
|
|
for name, value, ref in self.tags:
|
|
if ref in empty_blocks:
|
|
constructor_exprs.append(gen_name(name, True))
|
|
else:
|
|
constructor_exprs.append("%s %s_CL" %
|
|
(gen_name(name, True), gen_name(name)))
|
|
|
|
print("datatype %s_CL =\n %s\n" %
|
|
(self.name, '\n | '.join(constructor_exprs)),
|
|
file=output)
|
|
|
|
# Generate get_tag definition
|
|
subs = {"name": self.name,
|
|
"base": self.base}
|
|
|
|
templates = ([union_get_tag_def_entry_template] * (len(self.widths) - 1)
|
|
+ [union_get_tag_def_final_template])
|
|
|
|
fs = (union_get_tag_def_header_template % subs
|
|
+ "".join([template %
|
|
dict(subs,
|
|
tag_size=width,
|
|
classmask=self.word_classmask(width),
|
|
tag_index=self.tag_offset[width] // self.base,
|
|
tag_shift=self.tag_offset[width] % self.base)
|
|
for template, width in zip(templates, self.widths)])
|
|
+ union_get_tag_def_footer_template % subs)
|
|
|
|
print(fs, file=output)
|
|
print(file=output)
|
|
|
|
# Generate get_tag_eq_x lemma
|
|
templates = ([union_get_tag_eq_x_def_entry_template]
|
|
* (len(self.widths) - 1)
|
|
+ [union_get_tag_eq_x_def_final_template])
|
|
|
|
fs = (union_get_tag_eq_x_def_header_template % subs
|
|
+ "".join([template %
|
|
dict(subs,
|
|
tag_size=width,
|
|
classmask=self.word_classmask(width),
|
|
tag_index=self.tag_offset[width] // self.base,
|
|
tag_shift=self.tag_offset[width] % self.base)
|
|
for template, width in zip(templates, self.widths)])
|
|
+ union_get_tag_eq_x_def_footer_template % subs)
|
|
|
|
print(fs, file=output)
|
|
print(file=output)
|
|
|
|
# Generate mask helper lemmas
|
|
|
|
for name, value, ref in self.tags:
|
|
offset, size, _ = ref.field_map[self.tagname]
|
|
part_widths = [w for w in self.widths if w < size]
|
|
if part_widths:
|
|
subs = {"name": self.name,
|
|
"block": name,
|
|
"full_mask": hex(2 ** size - 1),
|
|
"full_value": hex(value)}
|
|
|
|
fs = (union_tag_mask_helpers_header_template % subs
|
|
+ "".join([union_tag_mask_helpers_entry_template %
|
|
dict(subs, part_mask=hex(2 ** pw - 1),
|
|
part_value=hex(value & (2 ** pw - 1)))
|
|
for pw in part_widths])
|
|
+ union_tag_mask_helpers_footer_template)
|
|
|
|
print(fs, file=output)
|
|
print(file=output)
|
|
|
|
# Generate lift definition
|
|
collapse_proofs = ""
|
|
tag_cases = []
|
|
for name, value, ref in self.tags:
|
|
field_inits = []
|
|
|
|
for field in ref.visible_order:
|
|
offset, size, high = ref.field_map[field]
|
|
|
|
if field == self.tagname:
|
|
continue
|
|
|
|
index = offset // self.base
|
|
sign_extend = ""
|
|
|
|
if high:
|
|
shift_op = "<<"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if shift < 0:
|
|
shift = -shift
|
|
shift_op = ">>"
|
|
if self.base_sign_extend:
|
|
sign_extend = "sign_extend %d " % (self.base_bits - 1)
|
|
else:
|
|
shift_op = ">>"
|
|
shift = offset % self.base
|
|
|
|
initialiser = \
|
|
"%s_CL.%s_CL = %s(((index (%s_C.words_C %s) %d) %s %d)" % \
|
|
(gen_name(name), field, sign_extend, self.name, self.name,
|
|
index, shift_op, shift)
|
|
|
|
if size < self.base:
|
|
mask = field_mask_proof(self.base, self.base_bits,
|
|
self.base_sign_extend, high, size)
|
|
initialiser += " AND " + mask
|
|
|
|
field_inits.append("\n " + initialiser + ")")
|
|
|
|
if len(field_inits) == 0:
|
|
value = gen_name(name, True)
|
|
else:
|
|
value = "%s \<lparr> %s \<rparr>" % \
|
|
(gen_name(name, True), ','.join(field_inits))
|
|
|
|
tag_cases.append("if tag = scast %s then Some (%s)" %
|
|
(gen_name(name), value))
|
|
|
|
collapse_proofs += \
|
|
make_proof("lift_collapse_proof",
|
|
{"name": self.name,
|
|
"block": name,
|
|
"value": value},
|
|
params.sorry)
|
|
collapse_proofs += "\n\n"
|
|
|
|
print(union_lift_def_template %
|
|
{"name": self.name,
|
|
"tag_cases": '\n else '.join(tag_cases)},
|
|
file=output)
|
|
print(file=output)
|
|
|
|
print(collapse_proofs, file=output)
|
|
|
|
block_lift_lemmas = "lemmas %s_lifts = \n" % self.name
|
|
# Generate lifted access/update definitions, and abstract lifters
|
|
for name, value, ref in self.tags:
|
|
# Don't generate accessors if the block (minus tag) is empty
|
|
if ref in empty_blocks:
|
|
continue
|
|
|
|
substs = {"union": self.name,
|
|
"block": name,
|
|
"generator": gen_name(name, True)}
|
|
|
|
for t in [union_access_def_template, union_update_def_template]:
|
|
print(t % substs, file=output)
|
|
print(file=output)
|
|
|
|
print(block_lift_def_template % substs, file=output)
|
|
print(file=output)
|
|
|
|
print(block_lift_lemma_template % substs, file=output)
|
|
print(file=output)
|
|
|
|
block_lift_lemmas += "\t%(union)s_%(block)s_lift\n" % substs
|
|
|
|
print(block_lift_lemmas, file=output)
|
|
print(file=output)
|
|
|
|
def generate(self, params):
|
|
output = params.output
|
|
|
|
# Generate typedef
|
|
print(typedef_template %
|
|
{"type": TYPES[options.environment][self.base],
|
|
"name": self.name,
|
|
"multiple": self.multiple}, file=output)
|
|
print(file=output)
|
|
|
|
# Generate tag enum
|
|
print("enum %s_tag {" % self.name, file=output)
|
|
if len(self.tags) > 0:
|
|
for name, value, ref in self.tags[:-1]:
|
|
print(" %s_%s = %d," % (self.name, name, value),
|
|
file=output)
|
|
name, value, ref = self.tags[-1]
|
|
print(" %s_%s = %d" % (self.name, name, value),
|
|
file=output)
|
|
print("};", file=output)
|
|
print("typedef enum %s_tag %s_tag_t;" %
|
|
(self.name, self.name), file=output)
|
|
print(file=output)
|
|
|
|
subs = {
|
|
'inline': INLINE[options.environment],
|
|
'union': self.name,
|
|
'type': TYPES[options.environment][self.union_base],
|
|
'tagname': self.tagname,
|
|
'suf': self.constant_suffix}
|
|
|
|
# Generate tag reader
|
|
templates = ([tag_reader_entry_template] * (len(self.widths) - 1)
|
|
+ [tag_reader_final_template])
|
|
|
|
fs = (tag_reader_header_template % subs
|
|
+ "".join([template %
|
|
dict(subs,
|
|
mask=2 ** width - 1,
|
|
classmask=self.word_classmask(width),
|
|
index=self.tag_offset[width] // self.base,
|
|
shift=self.tag_offset[width] % self.base)
|
|
for template, width in zip(templates, self.widths)])
|
|
+ tag_reader_footer_template % subs)
|
|
|
|
emit_named("%s_get_%s" % (self.name, self.tagname), params, fs)
|
|
|
|
# Generate tag eq reader
|
|
templates = ([tag_eq_reader_entry_template] * (len(self.widths) - 1)
|
|
+ [tag_eq_reader_final_template])
|
|
|
|
fs = (tag_eq_reader_header_template % subs
|
|
+ "".join([template %
|
|
dict(subs,
|
|
mask=2 ** width - 1,
|
|
classmask=self.word_classmask(width),
|
|
index=self.tag_offset[width] // self.base,
|
|
shift=self.tag_offset[width] % self.base)
|
|
for template, width in zip(templates, self.widths)])
|
|
+ tag_eq_reader_footer_template % subs)
|
|
|
|
emit_named("%s_%s_equals" % (self.name, self.tagname), params, fs)
|
|
|
|
# Generate pointer lifted tag reader
|
|
templates = ([ptr_tag_reader_entry_template] * (len(self.widths) - 1)
|
|
+ [ptr_tag_reader_final_template])
|
|
|
|
fs = (ptr_tag_reader_header_template % subs
|
|
+ "".join([template %
|
|
dict(subs,
|
|
mask=2 ** width - 1,
|
|
classmask=self.word_classmask(width),
|
|
index=self.tag_offset[width] // self.base,
|
|
shift=self.tag_offset[width] % self.base)
|
|
for template, width in zip(templates, self.widths)])
|
|
+ ptr_tag_reader_footer_template % subs)
|
|
|
|
emit_named("%s_ptr_get_%s" % (self.name, self.tagname), params, fs)
|
|
|
|
for name, value, ref in self.tags:
|
|
# Generate generators
|
|
param_fields = [field for field in ref.visible_order if field != self.tagname]
|
|
param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
|
|
for field in param_fields]
|
|
|
|
if len(param_list) == 0:
|
|
gen_params = 'void'
|
|
else:
|
|
gen_params = ', '.join(param_list)
|
|
|
|
ptr_params = ', '.join(["%s_t *%s_ptr" % (self.name, self.name)] + param_list)
|
|
|
|
field_updates = {word: [] for word in range(self.multiple)}
|
|
field_asserts = [" /* fail if user has passed bits that we will override */"]
|
|
|
|
for field in ref.visible_order:
|
|
offset, size, high = ref.field_map[field]
|
|
|
|
if field == self.tagname:
|
|
f_value = "(%s)%s_%s" % (TYPES[options.environment][self.base], self.name, name)
|
|
else:
|
|
f_value = field
|
|
|
|
index = offset // self.base
|
|
if high:
|
|
shift_op = ">>"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if self.base_sign_extend:
|
|
high_bits = ((self.base_sign_extend << (
|
|
self.base - self.base_bits)) - 1) << self.base_bits
|
|
else:
|
|
high_bits = 0
|
|
if shift < 0:
|
|
shift = -shift
|
|
shift_op = "<<"
|
|
else:
|
|
shift_op = "<<"
|
|
shift = offset % self.base
|
|
high_bits = 0
|
|
if size < self.base:
|
|
if high:
|
|
mask = ((1 << size) - 1) << (self.base_bits - size)
|
|
else:
|
|
mask = (1 << size) - 1
|
|
suf = self.constant_suffix
|
|
|
|
field_asserts.append(
|
|
" %s((%s & ~0x%x%s) == ((%d && (%s & (1%s << %d))) ? 0x%x : 0));"
|
|
% (ASSERTS[options.environment], f_value, mask, suf, self.base_sign_extend,
|
|
f_value, suf, self.base_bits - 1, high_bits))
|
|
|
|
field_updates[index].append(
|
|
"(%s & 0x%x%s) %s %d" % (f_value, mask, suf, shift_op, shift))
|
|
|
|
else:
|
|
field_updates[index].append("%s %s %d" % (f_value, shift_op, shift))
|
|
|
|
word_inits = [
|
|
("words[%d] = 0" % index) + ''.join(["\n | %s" % up for up in ups]) + ';'
|
|
for (index, ups) in field_updates.items()]
|
|
|
|
def mk_inits(prefix):
|
|
return '\n'.join([" %s%s" % (prefix, word_init) for word_init in word_inits])
|
|
|
|
print_params = {
|
|
"inline": INLINE[options.environment],
|
|
"block": name,
|
|
"union": self.name,
|
|
"gen_params": gen_params,
|
|
"ptr_params": ptr_params,
|
|
"gen_inits": mk_inits("%s." % self.name),
|
|
"ptr_inits": mk_inits("%s_ptr->" % self.name),
|
|
"asserts": ' \n'.join(field_asserts)
|
|
}
|
|
|
|
generator = union_generator_template % print_params
|
|
ptr_generator = ptr_union_generator_template % print_params
|
|
|
|
emit_named("%s_%s_new" % (self.name, name), params, generator)
|
|
emit_named("%s_%s_ptr_new" % (self.name, name), params, ptr_generator)
|
|
|
|
# Generate field readers/writers
|
|
tagnameoffset, tagnamesize, _ = ref.field_map[self.tagname]
|
|
tagmask = (2 ** tagnamesize) - 1
|
|
for field, offset, size, high in ref.fields:
|
|
# Don't duplicate tag accessors
|
|
if field == self.tagname:
|
|
continue
|
|
|
|
index = offset // self.base
|
|
if high:
|
|
write_shift = ">>"
|
|
read_shift = "<<"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if shift < 0:
|
|
shift = -shift
|
|
write_shift = "<<"
|
|
read_shift = ">>"
|
|
if self.base_sign_extend:
|
|
high_bits = ((self.base_sign_extend << (
|
|
self.base - self.base_bits)) - 1) << self.base_bits
|
|
else:
|
|
high_bits = 0
|
|
else:
|
|
write_shift = "<<"
|
|
read_shift = ">>"
|
|
shift = offset % self.base
|
|
high_bits = 0
|
|
mask = ((1 << size) - 1) << (offset % self.base)
|
|
|
|
subs = {
|
|
"inline": INLINE[options.environment],
|
|
"block": ref.name,
|
|
"field": field,
|
|
"type": TYPES[options.environment][ref.base],
|
|
"assert": ASSERTS[options.environment],
|
|
"index": index,
|
|
"shift": shift,
|
|
"r_shift_op": read_shift,
|
|
"w_shift_op": write_shift,
|
|
"mask": mask,
|
|
"tagindex": tagnameoffset // self.base,
|
|
"tagshift": tagnameoffset % self.base,
|
|
"tagmask": tagmask,
|
|
"union": self.name,
|
|
"suf": self.constant_suffix,
|
|
"high_bits": high_bits,
|
|
"sign_extend": self.base_sign_extend and high,
|
|
"extend_bit": self.base_bits - 1,
|
|
"base": self.base}
|
|
|
|
# Reader
|
|
emit_named("%s_%s_get_%s" % (self.name, ref.name, field),
|
|
params, union_reader_template % subs)
|
|
|
|
# Writer
|
|
emit_named("%s_%s_set_%s" % (self.name, ref.name, field),
|
|
params, union_writer_template % subs)
|
|
|
|
# Pointer lifted reader
|
|
emit_named("%s_%s_ptr_get_%s" % (self.name, ref.name, field),
|
|
params, ptr_union_reader_template % subs)
|
|
|
|
# Pointer lifted writer
|
|
emit_named("%s_%s_ptr_set_%s" % (self.name, ref.name, field),
|
|
params, ptr_union_writer_template % subs)
|
|
|
|
def make_names(self):
|
|
"Return the set of candidate function names for a union"
|
|
|
|
substs = {"union": self.name,
|
|
"tagname": self.tagname}
|
|
names = [t % substs for t in [
|
|
"%(union)s_get_%(tagname)s",
|
|
"%(union)s_ptr_get_%(tagname)s",
|
|
"%(union)s_%(tagname)s_equals"]]
|
|
|
|
for name, value, ref in self.tags:
|
|
names += ref.make_names(self)
|
|
|
|
return names
|
|
|
|
def represent_value(self, value, width):
|
|
max_width = max(self.classes.keys())
|
|
|
|
tail_str = ("{:0{}b}".format(value, width)
|
|
+ "_" * (self.tag_offset[width] - self.class_offset))
|
|
head_str = "_" * ((max_width + self.tag_offset[max_width]
|
|
- self.class_offset) - len(tail_str))
|
|
|
|
return head_str + tail_str
|
|
|
|
def represent_class(self, width):
|
|
max_width = max(self.classes.keys())
|
|
|
|
cmask = self.classes[width]
|
|
return ("{:0{}b}".format(cmask, max_width).replace("0", "-")
|
|
+ " ({:#x})".format(cmask))
|
|
|
|
def represent_field(self, width):
|
|
max_width = max(self.classes.keys())
|
|
offset = self.tag_offset[width] - self.class_offset
|
|
|
|
return ("{:0{}b}".format((2 ** width - 1) << offset, max_width)
|
|
.replace("0", "-").replace("1", "#"))
|
|
|
|
def assert_value_in_class(self, name, value, width):
|
|
max_width = max(self.classes.keys())
|
|
ovalue = value << self.tag_offset[width]
|
|
cvalue = value << (self.tag_offset[width] - self.class_offset)
|
|
|
|
offset_field = (2 ** width - 1) << self.tag_offset[width]
|
|
if (ovalue | offset_field) != offset_field:
|
|
raise ValueError(
|
|
"The value for element %s of tagged union %s,\n"
|
|
" %s\nexceeds the field bounds\n"
|
|
" %s."
|
|
% (name, self.name,
|
|
self.represent_value(value, width),
|
|
self.represent_field(width)))
|
|
|
|
for w, mask in [(lw, self.classes[lw])
|
|
for lw in self.widths if lw < width]:
|
|
if (cvalue & mask) != mask:
|
|
raise ValueError(
|
|
"The value for element %s of tagged union %s,\n"
|
|
" %s\nis invalid: it has %d bits but fails"
|
|
" to match the earlier mask at %d bits,\n"
|
|
" %s."
|
|
% (name, self.name,
|
|
self.represent_value(value, width),
|
|
width, w, self.represent_class(w)))
|
|
|
|
if (self.widths.index(width) + 1 < len(self.widths) and
|
|
(cvalue & self.classes[width]) == self.classes[width]):
|
|
raise ValueError(
|
|
"The value for element %s of tagged union %s,\n"
|
|
" %s (%d/%s)\nis invalid: it must not match the "
|
|
"mask for %d bits,\n %s."
|
|
% (name, self.name,
|
|
("{:0%db}" % width).format(cvalue),
|
|
value, hex(value),
|
|
width,
|
|
self.represent_class(width)))
|
|
|
|
def word_classmask(self, width):
|
|
"Return a class mask for testing a whole word, i.e., one."
|
|
"that is positioned absolutely relative to the lsb of the"
|
|
"relevant word."
|
|
|
|
return (self.classes[width] << (self.class_offset % self.base))
|
|
|
|
def make_classes(self, params):
|
|
"Calculate an encoding for variable width tagnames"
|
|
|
|
# Check self.classes, which maps from the bit width of tagname in a
|
|
# particular block to a classmask that identifies when a value belongs
|
|
# to wider tagname.
|
|
#
|
|
# For example, given three possible field widths -- 4, 8, and 12 bits --
|
|
# one possible encoding is:
|
|
#
|
|
# * * _ _ (** != 11)
|
|
# 0 _ _ _ 1 1 _ _
|
|
# _ _ _ _ 1 _ _ _ 1 1 _ _
|
|
#
|
|
# where the 3rd and 4th lsbs signify whether the field should be
|
|
# interpreted using a 4-bit mask (if 00, 01, or 10) or as an 8 or 16 bit
|
|
# mask (if 11). And, in the latter case, the 8th lsb signifies whether
|
|
# to intrepret it as an 8 bit field (if 0) or a 16 bit field (if 1).
|
|
#
|
|
# In this example we have:
|
|
# 4-bit class: classmask = 0b00001100
|
|
# 8-bit class: classmask = 0b10001100
|
|
# 16-bit class: classmask = 0b10001100
|
|
#
|
|
# More generally, the fields need not all start at the same offset
|
|
# (measured "left" from the lsb), for example:
|
|
#
|
|
# ...# ###. .... .... 4-bit field at offset 9
|
|
# ..## #### ##.. .... 8-bit field at offset 6
|
|
# #### #### #### .... 12-bit field at offset 4
|
|
#
|
|
# In this case, the class_offset is the minimum offset (here 4).
|
|
# Classmasks are declared relative to the field, but converted
|
|
# internally to be relative to the class_offset; tag_offsets
|
|
# are absolute (relative to the lsb); values are relative to
|
|
# the tag_offset (i.e., within the field). for example:
|
|
#
|
|
# ...1 100. .... 4-bit class: classmask=0xc tag_offset=9
|
|
# ..01 1000 10.. 8-bit class: classmask=0x62 tag_offset=6
|
|
# 0001 1000 1000 16-bit class: classmask=0x188 tag_offset=4
|
|
|
|
used = set()
|
|
self.tag_offset = {}
|
|
for name, _, ref in self.tags:
|
|
offset, size, _ = ref.field_map[self.tagname]
|
|
used.add(size)
|
|
self.tag_offset[size] = offset
|
|
|
|
self.class_offset = min(self.tag_offset.values())
|
|
|
|
# internally, classmasks are relative to the class_offset, so
|
|
# that we can compare them to each other.
|
|
for w in self.classes:
|
|
self.classes[w] <<= self.tag_offset[w] - self.class_offset
|
|
|
|
used_widths = sorted(list(used))
|
|
assert(len(used_widths) > 0)
|
|
|
|
if not self.classes:
|
|
self.classes = {used_widths[0]: 0}
|
|
|
|
# sanity checks on classes
|
|
classes = self.classes
|
|
widths = sorted(self.classes.keys())
|
|
context = "masks for %s.%s" % (self.name, self.tagname)
|
|
class_offset = self.class_offset
|
|
|
|
for uw in used_widths:
|
|
if uw not in classes:
|
|
raise ValueError("%s: none defined for a field of %d bits."
|
|
% (context, uw))
|
|
|
|
for mw in classes.keys():
|
|
if mw not in used_widths:
|
|
raise ValueError(
|
|
"%s: there is a mask with %d bits but no corresponding fields."
|
|
% (context, mw))
|
|
|
|
for w in widths:
|
|
offset_field = (2 ** w - 1) << self.tag_offset[w]
|
|
if (classes[w] << class_offset) | offset_field != offset_field:
|
|
raise ValueError(
|
|
"{:s}: the mask for {:d} bits:\n {:s}\n"
|
|
"exceeds the field bounds:\n {:s}."
|
|
.format(context, w, self.represent_class(w),
|
|
self.represent_field(w)))
|
|
|
|
if len(widths) > 1 and classes[widths[0]] == 0:
|
|
raise ValueError("%s: the first (width %d) is zero." % (
|
|
context, widths[0]))
|
|
|
|
if any([classes[widths[i-1]] == classes[widths[i]]
|
|
for i in range(1, len(widths) - 1)]):
|
|
raise ValueError("%s: there is a non-final duplicate!" % context)
|
|
|
|
# smaller masks are included within larger masks
|
|
pre_mask = None
|
|
pre_width = None
|
|
for w in widths:
|
|
if pre_mask is not None and (classes[w] & pre_mask) != pre_mask:
|
|
raise ValueError(
|
|
"{:s}: the mask\n 0b{:b} for width {:d} does not include "
|
|
"the mask\n 0b{:b} for width {:d}.".format(
|
|
context, classes[w], w, pre_mask, pre_width))
|
|
pre_width = w
|
|
pre_mask = classes[w]
|
|
|
|
if params.showclasses:
|
|
print("-----%s.%s" % (self.name, self.tagname), file=sys.stderr)
|
|
for w in widths:
|
|
print("{:2d} = {:s}".format(w, self.represent_class(w)),
|
|
file=sys.stderr)
|
|
|
|
self.widths = widths
|
|
|
|
|
|
class Block:
|
|
def __init__(self, name, fields, visible_order):
|
|
offset = 0
|
|
_fields = []
|
|
self.size = sum(size for _name, size, _high in fields)
|
|
offset = self.size
|
|
self.constant_suffix = ''
|
|
|
|
if visible_order is None:
|
|
self.visible_order = []
|
|
|
|
for _name, _size, _high in fields:
|
|
offset -= _size
|
|
if not _name is None:
|
|
if visible_order is None:
|
|
self.visible_order.append(_name)
|
|
_fields.append((_name, offset, _size, _high))
|
|
|
|
self.name = name
|
|
self.tagged = False
|
|
self.fields = _fields
|
|
self.field_map = dict((name, (offset, size, high))
|
|
for name, offset, size, high in _fields)
|
|
|
|
if not visible_order is None:
|
|
missed_fields = set(self.field_map.keys())
|
|
|
|
for _name in visible_order:
|
|
if _name not in self.field_map:
|
|
raise ValueError("Nonexistent field '%s' in visible_order"
|
|
% _name)
|
|
missed_fields.remove(_name)
|
|
|
|
if len(missed_fields) > 0:
|
|
raise ValueError("Fields %s missing from visible_order" %
|
|
str([x for x in missed_fields]))
|
|
|
|
self.visible_order = visible_order
|
|
|
|
def set_base(self, base, base_bits, base_sign_extend, suffix):
|
|
self.base = base
|
|
self.constant_suffix = suffix
|
|
self.base_bits = base_bits
|
|
self.base_sign_extend = base_sign_extend
|
|
if self.size % base != 0:
|
|
raise ValueError("Size of block %s not a multiple of base"
|
|
% self.name)
|
|
self.multiple = self.size // base
|
|
for name, offset, size, high in self.fields:
|
|
if offset // base != (offset+size-1) // base:
|
|
raise ValueError("Field %s of block %s "
|
|
"crosses a word boundary"
|
|
% (name, self.name))
|
|
|
|
def generate_hol_defs(self, params, suppressed_field=None,
|
|
prefix="", in_union=False):
|
|
output = params.output
|
|
|
|
# Don't generate raw records for blocks in tagged unions
|
|
if self.tagged and not in_union:
|
|
return
|
|
|
|
_name = prefix + self.name
|
|
|
|
# Generate record def
|
|
out = "record %s_CL =\n" % _name
|
|
|
|
empty = True
|
|
|
|
for field in self.visible_order:
|
|
if suppressed_field == field:
|
|
continue
|
|
|
|
empty = False
|
|
|
|
out += ' %s_CL :: "word%d"\n' % (field, self.base)
|
|
|
|
word_updates = ""
|
|
|
|
if not empty:
|
|
print(out, file=output)
|
|
|
|
# Generate lift definition
|
|
if not in_union:
|
|
field_inits = []
|
|
|
|
for name in self.visible_order:
|
|
offset, size, high = self.field_map[name]
|
|
|
|
index = offset // self.base
|
|
sign_extend = ""
|
|
|
|
if high:
|
|
shift_op = "<<"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if shift < 0:
|
|
shift = -shift
|
|
shift_op = ">>"
|
|
if self.base_sign_extend:
|
|
sign_extend = "sign_extend %d " % (self.base_bits - 1)
|
|
else:
|
|
shift_op = ">>"
|
|
shift = offset % self.base
|
|
|
|
initialiser = \
|
|
"%s_CL.%s_CL = %s(((index (%s_C.words_C %s) %d) %s %d)" % \
|
|
(self.name, name, sign_extend, self.name, self.name,
|
|
index, shift_op, shift)
|
|
|
|
if size < self.base:
|
|
mask = field_mask_proof(self.base, self.base_bits,
|
|
self.base_sign_extend, high, size)
|
|
|
|
initialiser += " AND " + mask
|
|
|
|
field_inits.append(initialiser + ")")
|
|
|
|
print(lift_def_template %
|
|
{"name": self.name,
|
|
"fields": ',\n '.join(field_inits)},
|
|
file=output)
|
|
print(file=output)
|
|
|
|
return empty
|
|
|
|
def generate_hol_proofs(self, params, type_map):
|
|
output = params.output
|
|
|
|
if self.tagged:
|
|
return
|
|
|
|
# Add fixed simp rule for struct
|
|
print("lemmas %(name)s_C_words_C_fl_simp[simp] = "
|
|
"%(name)s_C_words_C_fl[simplified]" %
|
|
{"name": self.name}, file=output)
|
|
print(file=output)
|
|
|
|
# Generate struct field pointer proofs
|
|
substs = {"name": self.name,
|
|
"words": self.multiple,
|
|
"base": self.base}
|
|
|
|
print(make_proof('words_NULL_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
print(make_proof('words_aligned_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
print(make_proof('words_ptr_safe_proof',
|
|
substs, params.sorry), file=output)
|
|
print(file=output)
|
|
|
|
# Generate struct lemmas
|
|
print(struct_lemmas_template % {"name": self.name},
|
|
file=output)
|
|
print(file=output)
|
|
|
|
# Generate struct_new specs
|
|
arg_list = ["\<acute>" + field for
|
|
(field, offset, size, high) in self.fields]
|
|
|
|
if not params.skip_modifies:
|
|
emit_named("%s_new" % self.name, params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_new" % self.name,
|
|
"args": ', '.join(["\<acute>ret__struct_%s_C" %
|
|
self.name] +
|
|
arg_list)},
|
|
params.sorry))
|
|
# FIXME: ptr_new (doesn't seem to be used)
|
|
|
|
field_eq_list = []
|
|
for (field, offset, size, high) in self.fields:
|
|
mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
|
|
sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend)
|
|
|
|
field_eq_list.append("%s_CL.%s_CL = %s(\<^bsup>s\<^esup>%s AND %s)" %
|
|
(self.name, field, sign_extend, field, mask))
|
|
field_eqs = ',\n '.join(field_eq_list)
|
|
|
|
emit_named("%s_new" % self.name, params,
|
|
make_proof('new_spec',
|
|
{"name": self.name,
|
|
"args": ', '.join(arg_list),
|
|
"field_eqs": field_eqs},
|
|
params.sorry))
|
|
|
|
emit_named_ptr_proof("%s_ptr_new" % self.name, params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_new_spec',
|
|
{"name": self.name,
|
|
"args": ', '.join(arg_list),
|
|
"field_eqs": field_eqs})
|
|
|
|
# Generate get/set specs
|
|
for (field, offset, size, high) in self.fields:
|
|
mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size)
|
|
sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend)
|
|
|
|
substs = {"name": self.name,
|
|
"field": field,
|
|
"mask": mask,
|
|
"sign_extend": sign_extend,
|
|
"ret_name": return_name(self.base),
|
|
"base": self.base}
|
|
|
|
if not params.skip_modifies:
|
|
# Get modifies spec
|
|
emit_named("%s_get_%s" % (self.name, field), params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_get_%s" % (self.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__unsigned_long",
|
|
"\<acute>%s" % self.name])},
|
|
params.sorry))
|
|
|
|
# Ptr get modifies spec
|
|
emit_named("%s_ptr_get_%s" % (self.name, field), params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_ptr_get_%s" % (self.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__unsigned_long",
|
|
"\<acute>%s_ptr" % self.name])},
|
|
params.sorry))
|
|
|
|
# Get spec
|
|
emit_named("%s_get_%s" % (self.name, field), params,
|
|
make_proof('get_spec', substs, params.sorry))
|
|
|
|
if not params.skip_modifies:
|
|
# Set modifies spec
|
|
emit_named("%s_set_%s" % (self.name, field), params,
|
|
make_proof('const_modifies_proof',
|
|
{"fun_name": "%s_set_%s" % (self.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>ret__struct_%s_C" % self.name,
|
|
"\<acute>%s" % self.name,
|
|
"\<acute>v%(base)d"])},
|
|
params.sorry))
|
|
|
|
emit_named("%s_ptr_set_%s" % (self.name, field), params,
|
|
make_proof('ptr_set_modifies_proof',
|
|
{"fun_name": "%s_ptr_set_%s" % (self.name, field),
|
|
"args": ', '.join([
|
|
"\<acute>%s_ptr" % self.name,
|
|
"\<acute>v%(base)d"])},
|
|
params.sorry))
|
|
|
|
# Set spec
|
|
emit_named("%s_set_%s" % (self.name, field), params,
|
|
make_proof('set_spec', substs, params.sorry))
|
|
|
|
emit_named_ptr_proof("%s_ptr_get_%s" % (self.name, field), params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_get_spec', substs)
|
|
emit_named_ptr_proof("%s_ptr_set_%s" % (self.name, field), params, self.name,
|
|
type_map, params.toplevel_types,
|
|
'ptr_set_spec', substs)
|
|
|
|
def generate(self, params):
|
|
output = params.output
|
|
|
|
# Don't generate raw accessors for blocks in tagged unions
|
|
if self.tagged:
|
|
return
|
|
|
|
# Type definition
|
|
print(typedef_template %
|
|
{"type": TYPES[options.environment][self.base],
|
|
"name": self.name,
|
|
"multiple": self.multiple}, file=output)
|
|
print(file=output)
|
|
|
|
# Generator
|
|
param_fields = [field for field in self.visible_order]
|
|
param_list = ["%s %s" % (TYPES[options.environment][self.base], field)
|
|
for field in param_fields]
|
|
|
|
if len(param_list) == 0:
|
|
gen_params = 'void'
|
|
else:
|
|
gen_params = ', '.join(param_list)
|
|
|
|
ptr_params = ', '.join(["%s_t *%s_ptr" % (self.name, self.name)] + param_list)
|
|
|
|
field_updates = {word: [] for word in range(self.multiple)}
|
|
field_asserts = [" /* fail if user has passed bits that we will override */"]
|
|
|
|
for field, offset, size, high in self.fields:
|
|
index = offset // self.base
|
|
if high:
|
|
shift_op = ">>"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if self.base_sign_extend:
|
|
high_bits = ((self.base_sign_extend << (
|
|
self.base - self.base_bits)) - 1) << self.base_bits
|
|
else:
|
|
high_bits = 0
|
|
if shift < 0:
|
|
shift = -shift
|
|
shift_op = "<<"
|
|
else:
|
|
shift_op = "<<"
|
|
shift = offset % self.base
|
|
high_bits = 0
|
|
if size < self.base:
|
|
if high:
|
|
mask = ((1 << size) - 1) << (self.base_bits - size)
|
|
else:
|
|
mask = (1 << size) - 1
|
|
suf = self.constant_suffix
|
|
|
|
field_asserts.append(
|
|
" %s((%s & ~0x%x%s) == ((%d && (%s & (1%s << %d))) ? 0x%x : 0));"
|
|
% (ASSERTS[options.environment], field, mask, suf, self.base_sign_extend,
|
|
field, suf, self.base_bits - 1, high_bits))
|
|
|
|
field_updates[index].append(
|
|
"(%s & 0x%x%s) %s %d" % (field, mask, suf, shift_op, shift))
|
|
|
|
else:
|
|
field_updates[index].append("%s %s %d;" % (field, shift_op, shift))
|
|
|
|
word_inits = [
|
|
("words[%d] = 0" % index) + ''.join(["\n | %s" % up for up in ups]) + ';'
|
|
for (index, ups) in field_updates.items()]
|
|
|
|
def mk_inits(prefix):
|
|
return '\n'.join([" %s%s" % (prefix, word_init) for word_init in word_inits])
|
|
|
|
print_params = {
|
|
"inline": INLINE[options.environment],
|
|
"block": self.name,
|
|
"gen_params": gen_params,
|
|
"ptr_params": ptr_params,
|
|
"gen_inits": mk_inits("%s." % self.name),
|
|
"ptr_inits": mk_inits("%s_ptr->" % self.name),
|
|
"asserts": ' \n'.join(field_asserts)
|
|
}
|
|
|
|
generator = generator_template % print_params
|
|
ptr_generator = ptr_generator_template % print_params
|
|
|
|
emit_named("%s_new" % self.name, params, generator)
|
|
emit_named("%s_ptr_new" % self.name, params, ptr_generator)
|
|
|
|
# Accessors
|
|
for field, offset, size, high in self.fields:
|
|
index = offset // self.base
|
|
if high:
|
|
write_shift = ">>"
|
|
read_shift = "<<"
|
|
shift = self.base_bits - size - (offset % self.base)
|
|
if shift < 0:
|
|
shift = -shift
|
|
write_shift = "<<"
|
|
read_shift = ">>"
|
|
if self.base_sign_extend:
|
|
high_bits = ((self.base_sign_extend << (
|
|
self.base - self.base_bits)) - 1) << self.base_bits
|
|
else:
|
|
high_bits = 0
|
|
else:
|
|
write_shift = "<<"
|
|
read_shift = ">>"
|
|
shift = offset % self.base
|
|
high_bits = 0
|
|
mask = ((1 << size) - 1) << (offset % self.base)
|
|
|
|
subs = {
|
|
"inline": INLINE[options.environment],
|
|
"block": self.name,
|
|
"field": field,
|
|
"type": TYPES[options.environment][self.base],
|
|
"assert": ASSERTS[options.environment],
|
|
"index": index,
|
|
"shift": shift,
|
|
"r_shift_op": read_shift,
|
|
"w_shift_op": write_shift,
|
|
"mask": mask,
|
|
"suf": self.constant_suffix,
|
|
"high_bits": high_bits,
|
|
"sign_extend": self.base_sign_extend and high,
|
|
"extend_bit": self.base_bits - 1,
|
|
"base": self.base}
|
|
|
|
# Reader
|
|
emit_named("%s_get_%s" % (self.name, field), params,
|
|
reader_template % subs)
|
|
|
|
# Writer
|
|
emit_named("%s_set_%s" % (self.name, field), params,
|
|
writer_template % subs)
|
|
|
|
# Pointer lifted reader
|
|
emit_named("%s_ptr_get_%s" % (self.name, field), params,
|
|
ptr_reader_template % subs)
|
|
|
|
# Pointer lifted writer
|
|
emit_named("%s_ptr_set_%s" % (self.name, field), params,
|
|
ptr_writer_template % subs)
|
|
|
|
def make_names(self, union=None):
|
|
"Return the set of candidate function names for a block"
|
|
|
|
if union is None:
|
|
# Don't generate raw accessors for blocks in tagged unions
|
|
if self.tagged:
|
|
return []
|
|
|
|
substs = {"block": self.name}
|
|
|
|
# A standalone block
|
|
field_templates = [
|
|
"%(block)s_get_%(field)s",
|
|
"%(block)s_set_%(field)s",
|
|
"%(block)s_ptr_get_%(field)s",
|
|
"%(block)s_ptr_set_%(field)s"]
|
|
|
|
names = [t % substs for t in [
|
|
"%(block)s_new",
|
|
"%(block)s_ptr_new"]]
|
|
else:
|
|
substs = {"block": self.name,
|
|
"union": union.name}
|
|
|
|
# A tagged union block
|
|
field_templates = [
|
|
"%(union)s_%(block)s_get_%(field)s",
|
|
"%(union)s_%(block)s_set_%(field)s",
|
|
"%(union)s_%(block)s_ptr_get_%(field)s",
|
|
"%(union)s_%(block)s_ptr_set_%(field)s"]
|
|
|
|
names = [t % substs for t in [
|
|
"%(union)s_%(block)s_new",
|
|
"%(union)s_%(block)s_ptr_new"]]
|
|
|
|
for field, offset, size, high in self.fields:
|
|
if not union is None and field == union.tagname:
|
|
continue
|
|
|
|
substs["field"] = field
|
|
names += [t % substs for t in field_templates]
|
|
|
|
return names
|
|
|
|
|
|
temp_output_files = []
|
|
|
|
|
|
class OutputFile(object):
|
|
def __init__(self, filename, mode='w', atomic=True):
|
|
"""Open an output file for writing, recording its filename.
|
|
If atomic is True, use a temporary file for writing.
|
|
Call finish_output to finalise all temporary files."""
|
|
self.filename = os.path.abspath(filename)
|
|
if atomic:
|
|
dirname, basename = os.path.split(self.filename)
|
|
self.file = tempfile.NamedTemporaryFile(
|
|
mode=mode, dir=dirname, prefix=basename + '.', delete=False)
|
|
if DEBUG:
|
|
print('Temp file: %r -> %r' % (self.file.name, self.filename), file=sys.stderr)
|
|
global temp_output_files
|
|
temp_output_files.append(self)
|
|
else:
|
|
self.file = open(filename, mode)
|
|
|
|
def write(self, *args, **kwargs):
|
|
self.file.write(*args, **kwargs)
|
|
|
|
|
|
def finish_output():
|
|
global temp_output_files
|
|
for f in temp_output_files:
|
|
os.rename(f.file.name, f.filename)
|
|
temp_output_files = []
|
|
|
|
|
|
# Toplevel
|
|
if __name__ == '__main__':
|
|
# Parse arguments to set mode and grab I/O filenames
|
|
params = {}
|
|
in_filename = None
|
|
in_file = sys.stdin
|
|
out_file = sys.stdout
|
|
mode = 'c_defs'
|
|
|
|
parser = optparse.OptionParser()
|
|
parser.add_option('--c_defs', action='store_true', default=False)
|
|
parser.add_option('--environment', action='store', default='sel4',
|
|
choices=list(INCLUDES.keys()))
|
|
parser.add_option('--hol_defs', action='store_true', default=False)
|
|
parser.add_option('--hol_proofs', action='store_true', default=False)
|
|
parser.add_option('--sorry_lemmas', action='store_true',
|
|
dest='sorry', default=False)
|
|
parser.add_option('--prune', action='append',
|
|
dest="prune_files", default=[])
|
|
parser.add_option('--toplevel', action='append',
|
|
dest="toplevel_types", default=[])
|
|
parser.add_option('--umm_types', action='store',
|
|
dest="umm_types_file", default=None)
|
|
parser.add_option('--multifile_base', action='store', default=None)
|
|
parser.add_option('--cspec-dir', action='store', default=None,
|
|
help="Location of the 'cspec' directory containing 'KernelState_C'.")
|
|
parser.add_option('--thy-output-path', action='store', default=None,
|
|
help="Path that the output theory files will be located in.")
|
|
parser.add_option('--skip_modifies', action='store_true', default=False)
|
|
parser.add_option('--showclasses', action='store_true', default=False)
|
|
parser.add_option('--debug', action='store_true', default=False)
|
|
|
|
options, args = parser.parse_args()
|
|
DEBUG = options.debug
|
|
|
|
if len(args) > 0:
|
|
in_filename = args[0]
|
|
in_file = open(in_filename)
|
|
|
|
if len(args) > 1:
|
|
out_file = OutputFile(args[1])
|
|
|
|
#
|
|
# If generating Isabelle scripts, ensure we have enough information for
|
|
# relative paths required by Isabelle.
|
|
#
|
|
if options.hol_defs or options.hol_proofs:
|
|
# Ensure directory that we need to include is known.
|
|
if options.cspec_dir is None:
|
|
parser.error("'cspec_dir' not defined.")
|
|
|
|
# Ensure that if an output file was not specified, an output path was.
|
|
if len(args) <= 1:
|
|
if options.thy_output_path is None:
|
|
parser.error("Theory output path was not specified")
|
|
if out_file == sys.stdout:
|
|
parser.error(
|
|
'Output file name must be given when generating HOL definitions or proofs')
|
|
out_file.filename = os.path.abspath(options.thy_output_path)
|
|
|
|
if options.hol_proofs and not options.umm_types_file:
|
|
parser.error('--umm_types must be specified when generating HOL proofs')
|
|
|
|
del parser
|
|
|
|
options.output = out_file
|
|
|
|
# Parse the spec
|
|
lexer = lex.lex()
|
|
yacc.yacc(debug=0, write_tables=0)
|
|
blocks = {}
|
|
unions = {}
|
|
_, block_map, union_map = yacc.parse(input=in_file.read(), lexer=lexer)
|
|
base_list = [8, 16, 32, 64]
|
|
# assumes that unsigned int = 32 bit on 32-bit and 64-bit platforms,
|
|
# and that unsigned long long = 64 bit on 64-bit platforms.
|
|
# Should still work fine if ull = 128 bit, but will not work
|
|
# if unsigned int is less than 32 bit.
|
|
suffix_map = {8: 'u', 16: 'u', 32: 'u', 64: 'ull'}
|
|
for base_info, block_list in block_map.items():
|
|
base, base_bits, base_sign_extend = base_info
|
|
for name, b in block_list.items():
|
|
if not base in base_list:
|
|
raise ValueError("Invalid base size: %d" % base)
|
|
suffix = suffix_map[base]
|
|
b.set_base(base, base_bits, base_sign_extend, suffix)
|
|
blocks[name] = b
|
|
|
|
symtab = {}
|
|
symtab.update(blocks)
|
|
for base, union_list in union_map.items():
|
|
unions.update(union_list)
|
|
symtab.update(unions)
|
|
for base_info, union_list in union_map.items():
|
|
base, base_bits, base_sign_extend = base_info
|
|
for u in union_list.values():
|
|
if not base in base_list:
|
|
raise ValueError("Invalid base size: %d" % base)
|
|
suffix = suffix_map[base]
|
|
u.resolve(options, symtab)
|
|
u.set_base(base, base_bits, base_sign_extend, suffix)
|
|
|
|
if not in_filename is None:
|
|
base_filename = os.path.basename(in_filename).split('.')[0]
|
|
|
|
# Generate the module name from the input filename
|
|
module_name = base_filename
|
|
|
|
# Prune list of names to generate
|
|
name_list = []
|
|
for e in det_values(blocks, unions):
|
|
name_list += e.make_names()
|
|
|
|
name_list = set(name_list)
|
|
if len(options.prune_files) > 0:
|
|
search_re = re.compile('[a-zA-Z0-9_]+')
|
|
|
|
pruned_names = set()
|
|
for filename in options.prune_files:
|
|
f = open(filename)
|
|
string = f.read()
|
|
|
|
matched_tokens = set(search_re.findall(string))
|
|
pruned_names.update(matched_tokens & name_list)
|
|
else:
|
|
pruned_names = name_list
|
|
|
|
options.names = pruned_names
|
|
|
|
# Generate the output
|
|
if options.hol_defs:
|
|
# Fetch kernel
|
|
if options.multifile_base is None:
|
|
print("theory %s_defs" % module_name, file=out_file)
|
|
print("imports \"%s/KernelState_C\"" % (
|
|
os.path.relpath(options.cspec_dir,
|
|
os.path.dirname(out_file.filename))), file=out_file)
|
|
print("begin", file=out_file)
|
|
print(file=out_file)
|
|
|
|
print(defs_global_lemmas, file=out_file)
|
|
print(file=out_file)
|
|
|
|
for e in det_values(blocks, unions):
|
|
e.generate_hol_defs(options)
|
|
|
|
print("end", file=out_file)
|
|
else:
|
|
print("theory %s_defs" % module_name, file=out_file)
|
|
print("imports", file=out_file)
|
|
print(" \"%s/KernelState_C\"" % (
|
|
os.path.relpath(options.cspec_dir,
|
|
os.path.dirname(out_file.filename))), file=out_file)
|
|
for e in det_values(blocks, unions):
|
|
print(" %s_%s_defs" % (module_name, e.name),
|
|
file=out_file)
|
|
print("begin", file=out_file)
|
|
print("end", file=out_file)
|
|
|
|
for e in det_values(blocks, unions):
|
|
base_filename = \
|
|
os.path.basename(options.multifile_base).split('.')[0]
|
|
submodule_name = base_filename + "_" + \
|
|
e.name + "_defs"
|
|
out_file = OutputFile(options.multifile_base + "_" +
|
|
e.name + "_defs" + ".thy")
|
|
|
|
print("theory %s imports \"%s/KernelState_C\" begin" % (
|
|
submodule_name, os.path.relpath(options.cspec_dir,
|
|
os.path.dirname(out_file.filename))),
|
|
file=out_file)
|
|
print(file=out_file)
|
|
|
|
options.output = out_file
|
|
e.generate_hol_defs(options)
|
|
|
|
print("end", file=out_file)
|
|
elif options.hol_proofs:
|
|
def is_bit_type(tp):
|
|
return umm.is_base(tp) & (umm.base_name(tp) in
|
|
map(lambda e: e.name + '_C', det_values(blocks, unions)))
|
|
|
|
tps = umm.build_types(options.umm_types_file)
|
|
type_map = {}
|
|
|
|
# invert type map
|
|
for toptp in options.toplevel_types:
|
|
paths = umm.paths_to_type(tps, is_bit_type, toptp)
|
|
|
|
for path, tp in paths:
|
|
tp = umm.base_name(tp)
|
|
|
|
if tp in type_map:
|
|
raise ValueError("Type %s has multiple parents" % tp)
|
|
|
|
type_map[tp] = (toptp, path)
|
|
|
|
if options.multifile_base is None:
|
|
print("theory %s_proofs" % module_name, file=out_file)
|
|
print("imports %s_defs" % module_name, file=out_file)
|
|
print("begin", file=out_file)
|
|
print(file=out_file)
|
|
print(file=out_file)
|
|
|
|
for e in det_values(blocks, unions):
|
|
e.generate_hol_proofs(options, type_map)
|
|
|
|
print("end", file=out_file)
|
|
else:
|
|
# top types are broken here.
|
|
print("theory %s_proofs" % module_name, file=out_file)
|
|
print("imports", file=out_file)
|
|
for e in det_values(blocks, unions):
|
|
print(" %s_%s_proofs" % (module_name, e.name),
|
|
file=out_file)
|
|
print("begin", file=out_file)
|
|
print("end", file=out_file)
|
|
|
|
for e in det_values(blocks, unions):
|
|
base_filename = \
|
|
os.path.basename(options.multifile_base).split('.')[0]
|
|
submodule_name = base_filename + "_" + \
|
|
e.name + "_proofs"
|
|
out_file = OutputFile(options.multifile_base + "_" +
|
|
e.name + "_proofs" + ".thy")
|
|
|
|
print(("theory %s imports "
|
|
+ "%s_%s_defs begin") % (
|
|
submodule_name, base_filename, e.name),
|
|
file=out_file)
|
|
print(file=out_file)
|
|
|
|
options.output = out_file
|
|
e.generate_hol_proofs(options, type_map)
|
|
|
|
print("end", file=out_file)
|
|
else:
|
|
guard = re.sub(r'[^a-zA-Z0-9_]', '_', out_file.filename.upper())
|
|
print("#ifndef %(guard)s\n#define %(guard)s\n" %
|
|
{'guard': guard}, file=out_file)
|
|
print('\n'.join(map(lambda x: '#include <%s>' % x,
|
|
INCLUDES[options.environment])), file=out_file)
|
|
for e in det_values(blocks, unions):
|
|
e.generate(options)
|
|
print("#endif", file=out_file)
|
|
|
|
finish_output()
|