From e2143c03133ea896b9186e4916ecf30d369b0af9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Jan 2014 16:03:57 +0100 Subject: [PATCH] ltlparse, eltlparse: avoid unnecessary calls to strlen(). * src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh (flex_set_buffer): Take a std::string as argument and call yy_scan_bytes() with the string size() instead of calling yy_scan_string() which does strlen() on the supplied string. * src/ltlparse/ltlparse.yy: Adjust calls. * src/eltlparse/eltlscan.ll, src/eltlparse/parsedecl.hh, src/eltlparse/eltlparse.yy: Use a similar interface. This also fixes a memory leak as the scanned buffer was not released. --- src/eltlparse/eltlparse.yy | 7 ++++--- src/eltlparse/eltlscan.ll | 18 +++++++++++++++--- src/eltlparse/parsedecl.hh | 7 ++++--- src/ltlparse/ltlparse.yy | 12 ++++++------ src/ltlparse/ltlscan.ll | 9 +++++---- src/ltlparse/parsedecl.hh | 4 ++-- 6 files changed, 36 insertions(+), 21 deletions(-) diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 16e32bfff..3525a1b70 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -** Recherche et Développement de l'Epita (LRDE). +** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +** de Recherche et Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. ** @@ -552,7 +552,7 @@ namespace spot environment& env, bool debug) { - flex_scan_string(eltl_string.c_str()); + flex_set_buffer(eltl_string); const formula* result = 0; nfamap nmap; aliasmap amap; @@ -561,6 +561,7 @@ namespace spot parser.set_debug_level(debug); parser.parse(); error_list = pe.list_; + flex_unset_buffer(); return result; } } diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll index 408af9f9e..371d3f1e2 100644 --- a/src/eltlparse/eltlscan.ll +++ b/src/eltlparse/eltlscan.ll @@ -1,4 +1,5 @@ -/* Copyright (C) 2008 Laboratoire de Recherche et Développement +/* -*- coding: utf-8 -*- +** Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -19,6 +20,7 @@ %option noyywrap %option prefix="eltlyy" %option outfile="lex.yy.c" +%option stack %{ #include @@ -190,9 +192,19 @@ namespace spot } void - flex_scan_string(const char* s) + flex_set_buffer(const std::string& buf) { - yy_scan_string(s); + yypush_buffer_state(YY_CURRENT_BUFFER); + (void) yy_scan_bytes(buf.c_str(), buf.size()); + yy_push_state(0); + } + + void + flex_unset_buffer() + { + (void)&yy_top_state; // shut up a g++ warning. + yy_pop_state(); + yypop_buffer_state(); } } } diff --git a/src/eltlparse/parsedecl.hh b/src/eltlparse/parsedecl.hh index 5bfa7fd7b..e55fee06f 100644 --- a/src/eltlparse/parsedecl.hh +++ b/src/eltlparse/parsedecl.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -35,7 +35,8 @@ namespace spot { int flex_open(const std::string& name); void flex_close(); - void flex_scan_string(const char* s); + void flex_set_buffer(const std::string& buf); + void flex_unset_buffer(); } } diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 1bb71d4b6..3c7fc36a6 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -** et Développement de l'Epita (LRDE). +** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +** Recherche et Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Université Pierre et Marie Curie. @@ -983,7 +983,7 @@ namespace spot bool debug, bool lenient) { const formula* result = 0; - flex_set_buffer(ltl_string.c_str(), + flex_set_buffer(ltl_string, ltlyy::parser::token::START_LTL, lenient); ltlyy::parser parser(error_list, env, result); @@ -1000,7 +1000,7 @@ namespace spot bool debug, bool lenient) { const formula* result = 0; - flex_set_buffer(ltl_string.c_str(), + flex_set_buffer(ltl_string, ltlyy::parser::token::START_BOOL, lenient); ltlyy::parser parser(error_list, env, result); @@ -1017,7 +1017,7 @@ namespace spot bool debug) { const formula* result = 0; - flex_set_buffer(ltl_string.c_str(), + flex_set_buffer(ltl_string, ltlyy::parser::token::START_LBT, false); ltlyy::parser parser(error_list, env, result); @@ -1035,7 +1035,7 @@ namespace spot bool lenient) { const formula* result = 0; - flex_set_buffer(sere_string.c_str(), + flex_set_buffer(sere_string, ltlyy::parser::token::START_SERE, lenient); ltlyy::parser parser(error_list, env, result); diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 8322ae307..be0e6ad6c 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 2013, Laboratoire de Recherche et -** Développement de l'Epita (LRDE). +** Copyright (C) 2010, 2011, 2012, 2013, 2014, Laboratoire de +** Recherche et Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** et Marie Curie. @@ -315,10 +315,11 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" %% void -flex_set_buffer(const char* buf, int start_tok, bool lenient) +flex_set_buffer(const std::string& buf, + int start_tok, bool lenient) { yypush_buffer_state(YY_CURRENT_BUFFER); - yy_scan_string(buf); + (void) yy_scan_bytes(buf.c_str(), buf.size()); start_token = start_tok; if (start_tok == token::START_LBT) yy_push_state(lbt); diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh index 343c02634..9d3522464 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/ltlparse/parsedecl.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -32,7 +32,7 @@ spot::ltl::parse_error_list& error_list) YY_DECL; -void flex_set_buffer(const char *buf, int start_tok, bool lenient); +void flex_set_buffer(const std::string& buf, int start_tok, bool lenient); void flex_unset_buffer(); #endif // SPOT_LTLPARSE_PARSEDECL_HH