Source language flag #42
Conversation
vecchiot-aws
force-pushed
the
source_language_flag
branch
from
a417f67 to
33d3b02
Compare
| ) | ||
| return parser | ||
|
|
||
| def source_language(parser): |
There was a problem hiding this comment.
What happens if we have mixed language code, e.g. Rust that calls C, which is then linked together.
There was a problem hiding this comment.
I'm not sure how to approach this. We could try to infer source language from the file extension, but if we want some way of explicitly passing it in, we'd need to pass in a mapping from file to language, which seems clunky.
| Language.C: C, | ||
| Language.RUST: Rust | ||
| } | ||
| return name_map[name] |
There was a problem hiding this comment.
if the language isn't in, do we want to return None or throw an exception
There was a problem hiding this comment.
This was meant to act like an enum, in which case a missing look-up shouldn't happen. I'm not sure which is better in that case (None is more generally usable, but more prone to bugs in Python).
cbmc_viewer/optionst.py
Outdated
| '--source-language', | ||
| default=Language.C, | ||
| choices=Language.ALL_LANGUAGE_NAMES, | ||
| help='Set the source language of the analyzed file.' |
There was a problem hiding this comment.
How about "The source language compiled to produce the goto binary."
cbmc_viewer/optionst.py
Outdated
| logging.warning("Use xml or json instead of text for " | ||
| "better results: %s", filenames) | ||
|
|
||
| def set_default_language(args): |
There was a problem hiding this comment.
This function appears to be unnecessary, since you set a default and you list all possible choices, so python itself seems to do the work of this function.
cbmc_viewer/source_language.py
Outdated
| return cls._default_language | ||
|
|
||
| @classmethod | ||
| def set_default_language(cls, lang): |
There was a problem hiding this comment.
Where is this function called? I'm not sure this style of using classes and subclasses is pythonic.
cbmc_viewer/source_language.py
Outdated
| # specific language implementations | ||
|
|
||
| @classmethod | ||
| def get_name(cls): |
There was a problem hiding this comment.
I would remove the "get_" prefix since you always invoke them with full qualification, and since they really could be class attributes. And maybe they should be (initialized by the subclass init that I expected to see).
cbmc_viewer/source_language.py
Outdated
| return '^([a-zA-Z0-9_<>: ]+)$', 1 | ||
|
|
||
| @staticmethod | ||
| def get_symbol_regex(): |
There was a problem hiding this comment.
Are you sure the symbol name and pretty name have different regular expressions? Are you sure there are no prefixes like "tag-" and "struct-" that should be considered?
cbmc_viewer/symbol_table.py
Outdated
| if match: | ||
| return match.group(2) | ||
| # Match the shape of the input format | ||
| line_match = re.match("^Symbol\.\.\.\.\.\.: (.*)$", sym) |
There was a problem hiding this comment.
Prefer to use the original construct modified to be sym.strip.split(":", 1)[-1]. This would also allow removing the following if statement.
cbmc_viewer/symbol_table.py
Outdated
| if re.match('^[a-zA-Z0-9_]+$', name): | ||
| return name | ||
| # Match the shape of the input format | ||
| line_match = re.match("^Pretty name\.: (.*)$", sym) |
There was a problem hiding this comment.
Prefer to use the original construct modified to be sym.strip.split(":", 1)[-1]. This would also allow removing the following if statement.
cbmc_viewer/source_language.py
Outdated
|
|
||
| @staticmethod | ||
| def get_pretty_name_regex(): | ||
| return '.*[^\S]([a-zA-Z0-9_]+)$', 1 |
There was a problem hiding this comment.
This is different from the regexp you are replacing. Please confirm that the C regexps match the regexps you are replacing.
cbmc_viewer/source_language.py
Outdated
| return cls._default_language | ||
|
|
||
| @classmethod | ||
| def get_default_language_or_fail(cls): |
There was a problem hiding this comment.
Delete get_default_language and make this get_default_language.
vecchiot-aws
force-pushed
the
source_language_flag
branch
from
20a56df to
d1c1ec6
Compare
vecchiot-aws
force-pushed
the
source_language_flag
branch
from
d1c1ec6 to
3d5bc8a
Compare
This commit has the effect of doubling the number of C symbols since the list now includes fully-qualified symbols like function::1::x that denotes local variable x in scope 1 of function. But this doesn't change the html generated by viewer for C code. Proposing this pull request in favor of model-checking#42
|
Please consider a simpler solution #48 and try it out on Rust. |
|
Closing in favor of #48 |
This commit has the effect of doubling the number of C symbols since the list now includes fully-qualified symbols like function::1::x that denotes local variable x in scope 1 of function. But this doesn't change the html generated by viewer for C code. Proposing this pull request in favor of #42
Issue #, if available:
Description of changes:
This PR introduces the ability to specify a source file language in order to have language-specific functionality. The language is set with a flag, and defaults to C to allow currently existing uses of cbmc-viewer to continue functioning the same as before.
This PR additionally introduces language-specific regex patterns for pretty names in order to fix some issues with trace visualizations in Rust.
The two changes are coupled together in a single PR in order to discuss the design of the new
Languageclass.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.