From nobody Sun Dec 14 12:32:38 2025 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 9A94FC43334 for ; Thu, 16 Jun 2022 08:46:23 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1359779AbiFPIqS (ORCPT ); Thu, 16 Jun 2022 04:46:18 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34618 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1359766AbiFPIp6 (ORCPT ); Thu, 16 Jun 2022 04:45:58 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 9A7465DBF1; Thu, 16 Jun 2022 01:45:44 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 928A161D58; Thu, 16 Jun 2022 08:45:43 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id C06F1C3411F; Thu, 16 Jun 2022 08:45:38 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1655369143; bh=rP28sJePyrZSun7tv9P2hpI1QdYZIeV8UXSwoUZbzus=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=TQkTv6r0bfqIG2OiiPEqOaa8g/UEg6zAlnRmEJOIvJegqVE4UZgmmUN3rNb4WsrEO pIbPu+M2YLTLFEuLcoeTX9hxgjgZ5LeMem6f17XUgLbkVQuiP8T8QWp2kFJjwLyIR4 0AUn2LF88tNo9bC5P2BYnEfDzTkBNj00M1oXAe9MEY5Reyba4a2X4cwQdOl0Yn+Ydr uQVh4m5D1+iTudX2B0lc0ETSJvNHXRmsLQVPRSHiL+kR2YeVbJBjfgdm9RXDdEI2Pn UHMHMSD7LP8z5DGyt20pjfp5q7HIuSqtlCwCeMX54uB/TUh/Xg9KFQb8d4Z/ZKn78e 3tRQd4Bf7yDzw== From: Daniel Bristot de Oliveira To: Steven Rostedt Cc: Daniel Bristot de Oliveira , Wim Van Sebroeck , Guenter Roeck , Jonathan Corbet , Ingo Molnar , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , Marco Elver , Dmitry Vyukov , "Paul E. McKenney" , Shuah Khan , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org, linux-trace-devel@vger.kernel.org Subject: [PATCH V4 06/20] tools/rv: Add dot2c Date: Thu, 16 Jun 2022 10:44:48 +0200 Message-Id: <5b1e664b0c33f4da0430922718adc71a5d58d86c.1655368610.git.bristot@kernel.org> X-Mailer: git-send-email 2.35.1 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" dot2c is a tool that transforms an automata in the graphiviz .dot file into an C representation of the automata. usage: dot2c [-h] dot_file dot2c: converts a .dot file into a C structure positional arguments: dot_file The dot file to be converted optional arguments: -h, --help show this help message and exit Cc: Wim Van Sebroeck Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Steven Rostedt Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: linux-doc@vger.kernel.org Cc: linux-kernel@vger.kernel.org Cc: linux-trace-devel@vger.kernel.org Signed-off-by: Daniel Bristot de Oliveira --- tools/verification/dot2/Makefile | 21 +++ tools/verification/dot2/automata.py | 179 ++++++++++++++++++++ tools/verification/dot2/dot2c | 30 ++++ tools/verification/dot2/dot2c.py | 244 ++++++++++++++++++++++++++++ 4 files changed, 474 insertions(+) create mode 100644 tools/verification/dot2/Makefile create mode 100644 tools/verification/dot2/automata.py create mode 100644 tools/verification/dot2/dot2c create mode 100644 tools/verification/dot2/dot2c.py diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Mak= efile new file mode 100644 index 000000000000..235d182f6b2c --- /dev/null +++ b/tools/verification/dot2/Makefile @@ -0,0 +1,21 @@ +INSTALL=3Dinstall + +prefix ?=3D /usr +bindir ?=3D $(prefix)/bin +mandir ?=3D $(prefix)/share/man +miscdir ?=3D $(prefix)/share/dot2 +srcdir ?=3D $(prefix)/src + +PYLIB ?=3D $(shell python3 -c 'import sysconfig; print (sysconfig.get_pa= th("purelib"))') + +.PHONY: all +all: + +.PHONY: clean +clean: + +.PHONY: install +install: + $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py + $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py + $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/= automata.py new file mode 100644 index 000000000000..171ad4497983 --- /dev/null +++ b/tools/verification/dot2/automata.py @@ -0,0 +1,179 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# automata object: parse a dot file into a python object +# For more information, see: +# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/ +# +# This program was written in the development of this paper: +# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. +# "Efficient Formal Verification for the Linux Kernel." International +# Conference on Software Engineering and Formal Methods. Springer, Cham, = 2019. +# +# Copyright 2018-2020 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +import ntpath + +class Automata: + """Automata class: Reads a dot file and part it as an automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + def __init__(self, file_path): + self.__dot_path=3Dfile_path + self.name=3Dself.__get_model_name() + self.__dot_lines =3D self.__open_dot() + self.states, self.initial_state, self.final_states =3D self.__get_= state_variables() + self.events =3D self.__get_event_variables() + self.function =3D self.__create_matrix() + + def __get_model_name(self): + basename=3Dntpath.basename(self.__dot_path) + if basename.endswith(".dot") =3D=3D False: + print("not a dot file") + raise Exception("not a dot file: %s" % self.__dot_path) + + model_name=3Dbasename[0:-4] + if model_name.__len__() =3D=3D 0: + raise Exception("not a dot file: %s" % self.__dot_path) + + return model_name + + def __open_dot(self): + cursor =3D 0 + dot_lines =3D [] + try: + dot_file =3D open(self.__dot_path) + except: + raise Exception("Cannot open the file: %s" % self.__dot_path) + + dot_lines =3D dot_file.read().splitlines() + dot_file.close() + + # checking the first line: + line =3D dot_lines[cursor].split() + + if (line[0] !=3D "digraph") and (line[1] !=3D "state_automaton"): + raise Exception("Not a valid .dot format: %s" % self.__dot_pat= h) + else: + cursor =3D cursor + 1 + return dot_lines + + def __get_cursor_begin_states(self): + cursor =3D 0 + while self.__dot_lines[cursor].split()[0] !=3D "{node": + cursor +=3D 1 + return cursor + + def __get_cursor_begin_events(self): + cursor =3D 0 + while self.__dot_lines[cursor].split()[0] !=3D "{node": + cursor +=3D 1 + while self.__dot_lines[cursor].split()[0] =3D=3D "{node": + cursor +=3D 1 + # skip initial state transition + cursor +=3D 1 + return cursor + + def __get_state_variables(self): + # wait for node declaration + states =3D [] + final_states=3D[] + + has_final_states =3D False + cursor =3D self.__get_cursor_begin_states() + + # process nodes + while self.__dot_lines[cursor].split()[0] =3D=3D "{node": + line =3D self.__dot_lines[cursor].split() + raw_state =3D line[-1] + + # "enabled_fired"}; -> enabled_fired + state =3D raw_state.replace('"', '').replace('};', '').replace= (',','_') + if state[0:7] =3D=3D "__init_": + initial_state =3D state[7:] + else: + states.append(state) + if self.__dot_lines[cursor].__contains__("doublecircle") = =3D=3D True: + final_states.append(state) + has_final_states =3D True + + if self.__dot_lines[cursor].__contains__("ellipse") =3D=3D= True: + final_states.append(state) + has_final_states =3D True + + cursor =3D cursor + 1 + + states =3D sorted(set(states)) + states.remove(initial_state) + + # Insert the initial state at the bein og the states + states.insert(0, initial_state) + + if has_final_states =3D=3D False: + final_states.append(initial_state) + + return states, initial_state, final_states + + def __get_event_variables(self): + # here we are at the begin of transitions, take a note, we will re= turn later. + cursor =3D self.__get_cursor_begin_events() + + events =3D [] + while self.__dot_lines[cursor][1] =3D=3D '"': + # transitions have the format: + # "all_fired" -> "both_fired" [ label =3D "disable_irq" ]; + # ------------ event is here ------------^^^^^ + if self.__dot_lines[cursor].split()[1] =3D=3D "->": + line =3D self.__dot_lines[cursor].split() + event =3D line[-2].replace('"','') + + # when a transition has more than one lables, they are lik= e this + # "local_irq_enable\nhw_local_irq_enable_n" + # so split them. + + event =3D event.replace("\\n", " ") + for i in event.split(): + events.append(i) + cursor =3D cursor + 1 + + return sorted(set(events)) + + def __create_matrix(self): + # transform the array into a dictionary + events =3D self.events + states =3D self.states + events_dict =3D {} + states_dict =3D {} + nr_event =3D 0 + for event in events: + events_dict[event] =3D nr_event + nr_event +=3D 1 + + nr_state =3D 0 + for state in states: + states_dict[state] =3D nr_state + nr_state =3D nr_state + 1 + + # declare the matrix.... + matrix =3D [['-1' for x in range(nr_event)] for y in range(nr_stat= e)] + + # and we are back! Let's fill the matrix + cursor =3D self.__get_cursor_begin_events() + + while self.__dot_lines[cursor][1] =3D=3D '"': + if self.__dot_lines[cursor].split()[1] =3D=3D "->": + line =3D self.__dot_lines[cursor].split() + origin_state =3D line[0].replace('"','').replace(',','_') + dest_state =3D line[2].replace('"','').replace(',','_') + possible_events =3D line[-2].replace('"','').replace("\\n"= , " ") + for event in possible_events.split(): + matrix[states_dict[origin_state]][events_dict[event]] = =3D dest_state + cursor =3D cursor + 1 + + return matrix diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c new file mode 100644 index 000000000000..0165f203dedc --- /dev/null +++ b/tools/verification/dot2/dot2c @@ -0,0 +1,30 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# dot2m: transform dot files into C structures. +# For more information, see: +# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/ +# +# This program was written in the development of this paper: +# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. +# "Efficient Formal Verification for the Linux Kernel." International +# Conference on Software Engineering and Formal Methods. Springer, Cham, = 2019. +# +# Copyright 2018-2020 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +if __name__ =3D=3D '__main__': + from dot2 import dot2c + import argparse + import ntpath + import sys + + parser =3D argparse.ArgumentParser(description=3D'dot2c: converts a .d= ot file into a C structure') + parser.add_argument('dot_file', help=3D'The dot file to be converted') + + + args =3D parser.parse_args() + d=3Ddot2c.Dot2c(args.dot_file) + d.print_model_classic() diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot= 2c.py new file mode 100644 index 000000000000..07f040ebf882 --- /dev/null +++ b/tools/verification/dot2/dot2c.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# dot2c: transform dot files into C structures. +# For more information, see: +# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/ +# +# This program was written in the development of this paper: +# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. +# "Efficient Formal Verification for the Linux Kernel." International +# Conference on Software Engineering and Formal Methods. Springer, Cham, = 2019. +# +# Copyright 2018-2022 Red Hat, Inc. +# +# Author: +# Daniel Bristot de Oliveira + +from dot2.automata import Automata + +class Dot2c(Automata): + enum_suffix=3D"" + enum_states_def=3D"states" + enum_events_def=3D"events" + struct_automaton_def=3D"automaton" + var_automaton_def=3D"aut" + + def __init__(self, file_path): + super().__init__(file_path) + self.line_length=3D80 + + def __buff_to_string(self, buff): + string=3D"" + + for line in buff: + string=3Dstring + line + "\n" + + # cut off the last \n + return string[:-1] + + def __get_enum_states_content(self): + buff=3D[] + buff.append("\t%s%s =3D 0," % (self.initial_state, self.enum_suffi= x)) + for state in self.states: + if state !=3D self.initial_state: + buff.append("\t%s%s," % (state, self.enum_suffix)) + buff.append("\tstate_max%s" % (self.enum_suffix)) + + return buff + + def get_enum_states_string(self): + buff=3Dself.__get_enum_states_content() + return self.__buff_to_string(buff) + + def format_states_enum(self): + buff=3D[] + buff.append("enum %s {" % self.enum_states_def) + buff.append(self.get_enum_states_string()) + buff.append("};\n") + + return buff + + def __get_enum_events_content(self): + buff=3D[] + first=3DTrue + for event in self.events: + if first: + buff.append("\t%s%s =3D 0," % (event, self.enum_suffix)) + first=3DFalse + else: + buff.append("\t%s%s," % (event, self.enum_suffix)) + buff.append("\tevent_max%s" % self.enum_suffix) + + return buff + + def get_enum_events_string(self): + buff=3Dself.__get_enum_events_content() + return self.__buff_to_string(buff) + + def format_events_enum(self): + buff=3D[] + buff.append("enum %s {" % self.enum_events_def) + buff.append(self.get_enum_events_string()) + buff.append("};\n") + + return buff + + def get_minimun_type(self): + min_type=3D"char" + + if self.states.__len__() > 255: + min_type=3D"short" + + if self.states.__len__() > 65535: + min_type=3D"int" + + return min_type + + def format_automaton_definition(self): + min_type =3D self.get_minimun_type() + buff=3D[] + buff.append("struct %s {" % self.struct_automaton_def) + buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffi= x)) + buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffi= x)) + buff.append("\t%s function[state_max%s][event_max%s];" % (min_type= , self.enum_suffix, self.enum_suffix)) + buff.append("\t%s initial_state;" % min_type) + buff.append("\tchar final_states[state_max%s];" % (self.enum_suffi= x)) + buff.append("};\n") + return buff + + def format_aut_init_header(self): + buff=3D[] + buff.append("struct %s %s =3D {" % (self.struct_automaton_def, sel= f.var_automaton_def)) + return buff + + def __get_string_vector_per_line_content(self, buff): + first=3DTrue + string=3D"" + for entry in buff: + if first: + string =3D string + "\t\t\"" + entry + first=3DFalse; + else: + string =3D string + "\",\n\t\t\"" + entry + string =3D string + "\"" + + return string + + def get_aut_init_events_string(self): + return self.__get_string_vector_per_line_content(self.events) + + def get_aut_init_states_string(self): + return self.__get_string_vector_per_line_content(self.states) + + def format_aut_init_events_string(self): + buff=3D[] + buff.append("\t.event_names =3D {") + buff.append(self.get_aut_init_events_string()) + buff.append("\t},") + return buff + + def format_aut_init_states_string(self): + buff=3D[] + buff.append("\t.state_names =3D {") + buff.append(self.get_aut_init_states_string()) + buff.append("\t},") + + return buff + + def __get_max_strlen_of_states(self): + return max(self.states, key=3Dlen).__len__() + + def __get_state_string_length(self): + maxlen =3D self.__get_max_strlen_of_states() + self.enum_suffix.__= len__() + return "%" + str(maxlen) + "s" + + def get_aut_init_function(self): + nr_states=3Dself.states.__len__() + nr_events=3Dself.events.__len__() + buff=3D[] + + strformat =3D self.__get_state_string_length() + + for x in range(nr_states): + line=3D"\t\t{ " + for y in range(nr_events): + next_state =3D self.function[x][y] + if next_state !=3D '-1': + next_state =3D self.function[x][y] + self.enum_suffix + + if y !=3D nr_events-1: + line =3D line + strformat % next_state + ", " + else: + line =3D line + strformat % next_state + " }," + buff.append(line) + + return self.__buff_to_string(buff) + + def format_aut_init_function(self): + buff=3D[] + buff.append("\t.function =3D {") + buff.append(self.get_aut_init_function()) + buff.append("\t},") + + return buff + + def get_aut_init_initial_state(self): + return self.initial_state + + def format_aut_init_initial_state(self): + buff=3D[] + initial_state=3Dself.get_aut_init_initial_state() + buff.append("\t.initial_state =3D " + initial_state + self.enum_su= ffix + ",") + + return buff + + def get_aut_init_final_states(self): + line=3D"" + first=3DTrue + for state in self.states: + if first =3D=3D False: + line =3D line + ', ' + else: + first =3D False + + if self.final_states.__contains__(state): + line =3D line + '1' + else: + line =3D line + '0' + return line + + def format_aut_init_final_states(self): + buff=3D[] + buff.append("\t.final_states =3D { %s }," % self.get_aut_init_final= _states()) + + return buff + + def __get_automaton_initialization_footer_string(self): + footer=3D"};\n" + return footer + + def format_aut_init_footer(self): + buff=3D[] + buff.append(self.__get_automaton_initialization_footer_string()) + + return buff + + def format_model(self): + buff=3D[] + buff +=3D self.format_states_enum() + buff +=3D self.format_events_enum() + buff +=3D self.format_automaton_definition() + buff +=3D self.format_aut_init_header() + buff +=3D self.format_aut_init_states_string() + buff +=3D self.format_aut_init_events_string() + buff +=3D self.format_aut_init_function() + buff +=3D self.format_aut_init_initial_state() + buff +=3D self.format_aut_init_final_states() + buff +=3D self.format_aut_init_footer() + + return buff + + def print_model_classic(self): + buff=3Dself.format_model() + print(self.__buff_to_string(buff)) --=20 2.35.1