Skip to content
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

Add feature to allow reruns with different parameters in GobView #21

Open
wants to merge 48 commits into
base: master
Choose a base branch
from

Conversation

sxprz
Copy link

@sxprz sxprz commented May 16, 2023

This pull request introduces a feature that allows GobView users to rerun an analysis with different config options as part of my Bachelor Thesis. These have to be entered in an input bar. This input bar provides validation on whether the input is syntactically correct or whether the user is using not whitelisted options (in this case: parameters that are not compatible with the incremental analysis).

Parameters are following this format:

  • --set <option> <value>
  • --<option> <value>
  • --[enable/disable] <option> (syntactical sugar for boolean options)

Screenshot from 2023-07-07 11-58-34

Options in the whitelist are:

  • incremental.force-reanalyze.funs
  • incremental.reluctant.enabled
  • incremental.compare
  • incremental.detect-renames
  • incremental.restart
  • incremental.postsolver
  • annotation.goblint_precision

The arrow in the parameter history allows for sorting its entries in regards to the analysis clock time.
Parameters in the history are clickable. When clicked, they will be added into the input bar.
Hovering over the status icon when it depicts a warning sign, shows an error message for the respective error that happened in the rerun.

@sim642 sim642 added the enhancement New feature or request label May 16, 2023
@sxprz sxprz changed the title Add feature to allow reruns with different parameters Add feature to allow reruns with different parameters in GobView May 17, 2023
@sxprz sxprz force-pushed the sxprz-fork/rerun-with-different-params branch from 28977ad to 7546339 Compare May 30, 2023 14:02
@sxprz sxprz marked this pull request as ready for review July 11, 2023 12:31
Copy link
Member

@stilscher stilscher left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the PR and implementation of the analysis rerun option in GobView! Somehow the PR contains a set of commits for the inclusion of the goblint-http server that I think were already merged into master with #22. Could you try to rebase your branch? I think that would clean up the Thank you for the PR and implementation of the analysis rerun option in GobView! Somehow the PR contains a set of commits for the inclusion of the goblint-http server that I think were already merged into master with #22. Could you try to rebase your branch? I think that would help to see what changes were actually done in this PR and make the reviewing a little easier.

Comment on lines +1 to +6
[@react.component]
let make = () => {
<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" fill="currentColor" className="bi bi-arrow-down" viewBox="0 0 16 16">
<path fillRule="evenodd" d="M8 1a.5.5 0 0 1 .5.5v11.793l3.146-3.147a.5.5 0 0 1 .708.708l-4 4a.5.5 0 0 1-.708 0l-4-4a.5.5 0 0 1 .708-.708L7.5 13.293V1.5A.5.5 0 0 1 8 1z"/>
</svg>
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there some library where one could import the Icons from instead of defining an svg component?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This icon is from Bootstrap Icons. The idea was to not import the whole JS library and use only a couple of icons that were necessary, but the library can be found here.

Comment on lines +6 to +10
let parameters_regex = Str.regexp({|\(--\(enable\|disable\) [-a-zA-Z0-9\._]+\)\|\(--set [-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)? \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)\)\|\(--[-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)? \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)\)|});
let enable_disable_regex = Str.regexp({|--\(enable\|disable\) \([-a-zA-Z0-9\._]+\)|});
let set_regex = Str.regexp({|--set \([-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)?\) \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)|});
let other_regex = Str.regexp({|--\([-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)?\) \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)|});
let string_with_upticks_regex = Str.regexp({|'\(.*\)'|});
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This regex is quite hard to process. I think it would be nice to reuse the checking of command line arguments that is implemented for Goblint already. @sim642 Or do you think that is not possible?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, these regexes are something we should avoid. I haven't looked at this PR in more detail: why does Gobview need to parse Goblint command lines at all, instead of just letting Goblint do it as usual?

@sxprz sxprz force-pushed the sxprz-fork/rerun-with-different-params branch from 4588ee6 to 8a1bc4a Compare August 11, 2023 18:28
@sxprz
Copy link
Author

sxprz commented Aug 11, 2023

Branch is now rebased onto gobview:master and does not contain duplicate commits from goblint-http-server any longer, @stilscher 👍🏻

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants