#!/usr/bin/env python3 # # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) # # SPDX-License-Identifier: BSD-2-Clause # ## # 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' # The C parser emits variables with a suffix to indicate their types; this lets # the C parser distinguish `char x` from `int x`. # # The suffix map should match the C parser types for `uint{8,16,32,64}_t` in # `include/stdint.h`. var_size_suffix_map = {k: 'unsigned' + v for (k, v) in {8: '_char', 16: '_short', 32: '', 64: '_longlong'}.items()} def return_name(base): # name of return value for standard word sizes return 'ret__' + var_size_suffix_map[base] def var_name(name, base): # converts C variable name to Isabelle variable name via type mangling. return name + '___' + var_size_suffix_map[base] # Headers to include depending on which environment we are generating code for. 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 (__builtin_expect(!!(%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))), %(sign_extend)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 (__builtin_expect(!!(%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))), %(sign_extend)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%(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)); %(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%(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)); %(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 (__builtin_expect(!!(%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))), %(sign_extend)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 (__builtin_expect(!!(%(sign_extend)d && (ret & (1%(suf)s << (%(extend_bit)d)))), %(sign_extend)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 \ %(name)s_CL" where "%(name)s_lift %(name)s \ \ %(fields)s \"''' block_lift_def_template = \ '''definition %(union)s_%(block)s_lift :: ''' \ '''"%(union)s_C \ %(union)s_%(block)s_CL" where "%(union)s_%(block)s_lift %(union)s \ case (%(union)s_lift %(union)s) of ''' \ '''Some (%(generator)s rec) \ 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 \ word%(base)d" where "%(name)s_get_tag %(name)s \ ''' union_get_tag_def_entry_template = \ '''if ((index (%(name)s_C.words_C %(name)s) %(tag_index)d)''' \ ''' AND 0x%(classmask)x \ 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 \ 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 \ 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 \ %(name)s_CL option" where "%(name)s_lift %(name)s \ (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 \ 'a) \ %(union)s_CL \ 'a" where "%(union)s_%(block)s_access f %(union)s \ (case %(union)s of %(generator)s rec \ f rec)"''' union_update_def_template = \ '''definition %(union)s_%(block)s_update :: "(%(union)s_%(block)s_CL \''' \ ''' %(union)s_%(block)s_CL) \ %(union)s_CL \ %(union)s_CL" where "%(union)s_%(block)s_update f %(union)s \ (case %(union)s of %(generator)s rec \ %(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: "\ w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \ \ 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 \ cslift s ''' + ptrname + '''" shows "\s. \ \ \s. s \\<^sub>c ''' + ptrname + '''\ ''' + retval + '''PROC %(name)s_ptr_''' + name + '''(\%(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 \ cslift s ''' + ptrname + '''" shows "\s. \ \ \s. s \\<^sub>c ''' + ptrname + " " + pre + '''\ ''' + retval + '''PROC %(name)s_%(block)s_ptr_''' + name + '''(\%(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, '\%(ret_name)s :== ', '', '''\\%(ret_name)s = ''' '''%(name)s_CL.%(field)s_CL ''' '''(%(name)s_lift (%(access_path)s))\''') def ptr_set_template(name, ptrname): return ptr_basic_template(name, ptrname, '', ', \v%(base)d', '''{t. \%(name)s. %(name)s_lift %(name)s = %(name)s_lift (%(access_path)s) \ %(name)s_CL.%(field)s_CL ''' ''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \ \ 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. \%(name)s. %(name)s_lift %(name)s = \ %(field_eqs)s \ \ 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, '\%(ret_name)s :== ', '', '''\\%(ret_name)s = %(name)s_get_tag (%(access_path)s)\''') def ptr_empty_union_new_template(ptrname): return ptr_union_basic_template('new', ptrname, '', '', '', '''{t. \%(name)s. ''' '''%(name)s_get_tag %(name)s = scast %(name)s_%(block)s \ 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. \%(name)s. ''' '''%(name)s_%(block)s_lift %(name)s = \ %(field_eqs)s \ \ %(name)s_get_tag %(name)s = scast %(name)s_%(block)s \ 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, '\%(ret_name)s :== ', '', '\ %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s', '''\\%(ret_name)s = ''' '''%(name)s_%(block)s_CL.%(field)s_CL ''' '''(%(name)s_%(block)s_lift %(access_path)s)\''') def ptr_union_set_template(ptrname): return ptr_union_basic_template('set_%(field)s', ptrname, '', ', \v%(base)d', '\ %(name)s_get_tag %(access_path)s = scast %(name)s_%(block)s', '''{t. \%(name)s. ''' '''%(name)s_%(block)s_lift %(name)s = %(name)s_%(block)s_lift %(access_path)s ''' '''\ %(name)s_%(block)s_CL.%(field)s_CL ''' ''':= %(sign_extend)s(\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \ \ %(name)s_get_tag %(name)s = scast %(name)s_%(block)s \ 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 \ %(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) \ 0 < &(p\[''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) \ ptr_aligned ((Ptr &(p\[''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 \ ptr_safe (Ptr &(p\[''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: "\ \ {\} \ret__%(rtype)s :== PROC %(name)s_get_%(tag_name)s(''' ''' \%(name)) \\ret__%(rtype)s = %(name)s_get_tag''' '''\<^bsup>\\<^esup>\"''', ''' 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: "\ s. \ \\<^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: "\s. \ \\<^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: "\ s. \ \ {s} \ret__struct_%(name)s_C :== PROC %(name)s_new(%(args)s) \ %(name)s_lift \ret__struct_%(name)s_C = \ %(field_eqs)s \ \"''', ''' 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: "\s. \ \ {s} \%(ret_name)s :== ''' '''PROC %(name)s_get_%(field)s(\%(name)s) \\%(ret_name)s = ''' '''%(name)s_CL.%(field)s_CL ''' '''(%(name)s_lift \<^bsup>s\<^esup>%(name)s)\"''', ''' 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: "\s. \ \ {s} \ret__struct_%(name)s_C :== ''' '''PROC %(name)s_set_%(field)s(\%(name)s, \v%(base)d) \%(name)s_lift \ret__struct_%(name)s_C = ''' '''%(name)s_lift \<^bsup>s\<^esup>%(name)s \ ''' '''%(name)s_CL.%(field)s_CL ''' ''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s) \\"''', ''' 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: "\s. \ \ {s} \%(ret_name)s :== ''' \ '''PROC %(name)s_get_%(tagname)s(\%(name)s) \\%(ret_name)s = ''' \ '''%(name)s_get_tag \<^bsup>s\<^esup>%(name)s\"''', ''' 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: "\s. \ \ {s} \ret__int :== PROC %(name)s_%(tagname)s_equals(\%(name)s, \%(name)s_type_tag) \\ret__int = of_bl [%(name)s_get_tag \<^bsup>s\<^esup>%(name)s = \<^bsup>s\<^esup>%(name)s_type_tag]\"''', ''' 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: "\s. \ \ {s} \ret__struct_%(name)s_C :== ''' \ '''PROC %(name)s_%(block)s_new() \%(name)s_get_tag \ret__struct_%(name)s_C = ''' \ '''scast %(name)s_%(block)s\"''', ''' 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: "\s. \ \ {s} \ret__struct_%(name)s_C :== ''' \ '''PROC %(name)s_%(block)s_new(%(args)s) \%(name)s_%(block)s_lift ''' \ '''\ret__struct_%(name)s_C = \ %(field_eqs)s \ \ %(name)s_get_tag \ret__struct_%(name)s_C = ''' \ '''scast %(name)s_%(block)s\"''', ''' 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: 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: "\s. \ \ ''' \ '''\s. %(name)s_get_tag \%(name)s = ''' \ '''scast %(name)s_%(block)s\ \%(ret_name)s :== ''' \ '''PROC %(name)s_%(block)s_get_%(field)s(\%(name)s) \\%(ret_name)s = ''' \ '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ '''(%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s)''' \ '''\"''', ''' 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: "\s. \ \ ''' \ '''\s. %(name)s_get_tag \%(name)s = ''' \ '''scast %(name)s_%(block)s\ \ret__struct_%(name)s_C :== ''' \ '''PROC %(name)s_%(block)s_set_%(field)s(\%(name)s, \v%(base)d) \%(name)s_%(block)s_lift \ret__struct_%(name)s_C = ''' \ '''%(name)s_%(block)s_lift \<^bsup>s\<^esup>%(name)s \ ''' \ '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ ''':= %(sign_extend)s (\<^bsup>s\<^esup>v%(base)d AND %(mask)s)\ \ %(name)s_get_tag \ret__struct_%(name)s_C = ''' \ '''scast %(name)s_%(block)s\"''', ''' 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 + ')', ['\\_. ' + 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(["\ret__unsigned_long", "\%(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(["\ret__unsigned_long", "\%(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 = ["\" + 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([ "\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([ "\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, var_name(field, self.base), 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([ "\ret__unsigned_long", "\%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([ "\ret__unsigned_long", "\%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([ "\ret__struct_%s_C" % self.name, "\%s" % self.name, "\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([ "\%s_ptr" % self.name, "\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 \ %s \" % \ (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 = ["\" + field for field in self.visible_order] 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(["\ret__struct_%s_C" % self.name] + arg_list)}, params.sorry)) # FIXME: ptr_new (doesn't seem to be used) field_eq_list = [] for field in self.visible_order: offset, size, high = self.field_map[field] 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([ "\ret__unsigned_long", "\%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([ "\ret__unsigned_long", "\%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([ "\ret__struct_%s_C" % self.name, "\%s" % self.name, "\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([ "\%s_ptr" % self.name, "\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()