Skip to content

goto-gcc options parsing and new goto-cc specific options for large-scale builds #81

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 17 commits into from
Jan 22, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/ansi-c/parser.y
Original file line number Diff line number Diff line change
Expand Up @@ -2705,6 +2705,10 @@ asm_definition:
{
// Not obvious what to do with this.
}
| '{' TOK_ASM_STRING '}'
{
// Not obvious what to do with this.
}
;

function_definition:
Expand Down
54 changes: 43 additions & 11 deletions src/ansi-c/scanner.l
Original file line number Diff line number Diff line change
Expand Up @@ -290,8 +290,7 @@ void ansi_c_scanner_init()
<GRAMMAR,GCC_ATTRIBUTE3>{string_lit} {
PARSER.string_literal.clear();
PARSER.string_literal.append(yytext);
newstack(yyansi_clval);
PARSER.set_source_location(stack(yyansi_clval));
loc();
// String literals can be continued in
// the next line
yy_push_state(STRING_LITERAL);
Expand Down Expand Up @@ -381,6 +380,23 @@ void ansi_c_scanner_init()
<GRAMMAR>{cppstart}"define"{ws}.* { /* ignore */ }
<GRAMMAR>{cppstart}"undef"{ws}.* { /* ignore */ }

<GRAMMAR>{cppstart}"asm" {
if(PARSER.mode==configt::ansi_ct::flavourt::GCC) // really, this is BCC
{
BEGIN(ASM_BLOCK);
PARSER.string_literal.clear();
loc();
return '{';
}
else
return make_identifier();
}

<GRAMMAR>{cppstart}"endasm" {
loc();
return '}';
}

<GRAMMAR>{cppdirective} {
yyansi_cerror("Preprocessor directive found");
return TOK_SCANNER_ERROR;
Expand Down Expand Up @@ -1374,7 +1390,11 @@ __decltype { if(PARSER.cpp98 &&

"{" {
PARSER.tag_following=false;
if(PARSER.asm_block_following) { BEGIN(ASM_BLOCK); }
if(PARSER.asm_block_following)
{
BEGIN(ASM_BLOCK);
PARSER.string_literal.clear();
}
loc();
return yytext[0];
}
Expand All @@ -1392,7 +1412,12 @@ __decltype { if(PARSER.cpp98 &&
<MSC_ANNOTATION>"]" { BEGIN(GRAMMAR); }
<MSC_ANNOTATION>. { /* ignore */ }

<MSC_ASM>{ws}"{" { BEGIN(ASM_BLOCK); loc(); return '{'; }
<MSC_ASM>{ws}"{" {
BEGIN(ASM_BLOCK);
PARSER.string_literal.clear();
loc();
return '{';
}
<MSC_ASM>[^{^}^\n]* { loc();
source_locationt l=stack(yyansi_clval).source_location();
stack(yyansi_clval)=string_constantt(yytext);
Expand All @@ -1401,13 +1426,20 @@ __decltype { if(PARSER.cpp98 &&
return TOK_ASM_STRING;
}

<ASM_BLOCK>[^}]* { loc();
source_locationt l=stack(yyansi_clval).source_location();
stack(yyansi_clval)=string_constantt(yytext);
stack(yyansi_clval).add_source_location()=l;
return TOK_ASM_STRING; }
<ASM_BLOCK>"}" { PARSER.asm_block_following=false;
BEGIN(GRAMMAR); loc(); return '}'; }
<ASM_BLOCK>{
{ws} { /* ignore */ }
{newline} { /* ignore */ }
[^#}\n][^\n}]*[\n] { PARSER.string_literal.append(yytext); }
[^#}\n][^\n}]* { PARSER.string_literal.append(yytext); }
. { // anything else: back to normal
PARSER.asm_block_following=false;
loc();
stack(yyansi_clval)=string_constantt(PARSER.string_literal);
BEGIN(GRAMMAR);
yyless(0); // put back
return TOK_ASM_STRING;
}
}

<IGNORE_PARENS>")" { PARSER.parenthesis_counter--;
if(PARSER.parenthesis_counter==0)
Expand Down
3 changes: 2 additions & 1 deletion src/goto-cc/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@ SRC = goto_cc_main.cpp goto_cc_mode.cpp gcc_mode.cpp \
gcc_cmdline.cpp ms_cl_cmdline.cpp ld_cmdline.cpp \
compile.cpp armcc_cmdline.cpp \
goto_cc_languages.cpp goto_cc_cmdline.cpp \
ms_cl_mode.cpp armcc_mode.cpp cw_mode.cpp ld_mode.cpp
ms_cl_mode.cpp armcc_mode.cpp cw_mode.cpp bcc_cmdline.cpp \
as_mode.cpp as_cmdline.cpp as86_cmdline.cpp

OBJ += ../big-int/big-int$(LIBEXT) \
../goto-programs/goto-programs$(LIBEXT) \
Expand Down
6 changes: 4 additions & 2 deletions src/goto-cc/armcc_mode.h
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,10 @@ class armcc_modet:public goto_cc_modet
virtual int doit();
virtual void help_mode();

explicit armcc_modet(armcc_cmdlinet &_armcc_cmdline):
goto_cc_modet(_armcc_cmdline),
armcc_modet(
armcc_cmdlinet &_armcc_cmdline,
const std::string &_base_name):
goto_cc_modet(_armcc_cmdline, _base_name),
cmdline(_armcc_cmdline)
{
}
Expand Down
158 changes: 158 additions & 0 deletions src/goto-cc/as86_cmdline.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
/*******************************************************************\

Module: A special command line object for as86 (of Bruce's C Compiler)

Author: Michael Tautschnig

\*******************************************************************/

#include <cassert>
#include <iostream>

#include <util/prefix.h>

#include "as86_cmdline.h"

/*******************************************************************\

Function: as86_cmdlinet::parse

Inputs: argument count, argument strings

Outputs: none

Purpose: parses the commandline options into a cmdlinet

\*******************************************************************/

// non-as86 options
const char *goto_as86_options_with_argument[]=
{
"--verbosity",
"--function",
"--native-assembler",
"--print-rejected-preprocessed-source",
NULL
};

const char *as86_options_without_argument[]=
{
"-0",
"-1",
"-2",
"-3",
"-a",
"-g",
"-j",
"-O",
"-u",
"-u-", // both -u and -u- seem to be accepted
"-v",
"-w-",
NULL
};

const char *as86_options_with_argument[]=
{
"-lm",
"-l",
"-n",
"-o",
"-b",
"-s",
"-t",
NULL
};

bool as86_cmdlinet::parse(int argc, const char **argv)
{
assert(argc>0);
add_arg(argv[0]);

for(int i=1; i<argc; i++)
{
std::string argv_i=argv[i];

// file?
if(argv_i=="-" || !has_prefix(argv_i, "-"))
{
add_infile_arg(argv_i);
continue;
}

bool found=false;

// separated only, and also allow concatenation with "="
for(const char **o=goto_as86_options_with_argument;
*o!=NULL && !found;
++o)
{
std::string os(*o);

if(argv_i==os) // separated
{
found=true;
if(i!=argc-1)
{
set(argv_i, argv[i+1]);
++i;
}
else
set(argv_i, "");
}
else if(has_prefix(argv_i, os+"=")) // concatenated with "="
{
found=true;
set(os, argv_i.substr(os.size()+1));
}
}

// goto-as86-only command line argument found
if(found)
continue;

// add to new_argv
add_arg(argv_i);

// without argument; also store in cmdlinet
if(in_list(argv_i.c_str(), as86_options_without_argument))
{
set(argv_i);
continue;
}

for(const char **o=as86_options_with_argument;
*o!=NULL && !found;
++o)
{
std::string os(*o);

if(argv_i==os) // separated
{
found=true;
if(i!=argc-1)
{
set(argv_i, argv[i+1]);
add_arg(argv[i+1]);
++i;
}
else
set(argv_i, "");
}
else if(has_prefix(argv_i, os))
{
found=true;
set(os, argv[i]+os.size());
}
}

if(!found)
{
// unrecognized option
std::cerr << "Warning: uninterpreted as86 option '" << argv_i
<< "'" << std::endl;
}
}

return false;
}
27 changes: 27 additions & 0 deletions src/goto-cc/as86_cmdline.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
/*******************************************************************\

Module: A special command line object for as86 (of Bruce's C Compiler)

Author: Michael Tautschnig

Date: July 2016

\*******************************************************************/

#ifndef CPROVER_GOTO_CC_AS86_CMDLINE_H
#define CPROVER_GOTO_CC_AS86_CMDLINE_H

#include "goto_cc_cmdline.h"

class as86_cmdlinet:public goto_cc_cmdlinet
{
public:
// overload
virtual bool parse(int, const char**);

as86_cmdlinet()
{
}
};

#endif // CPROVER_GOTO_CC_AS86_CMDLINE_H
Loading