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

Heapster ide info #1821

Merged
merged 35 commits into from
Mar 2, 2023
Merged

Heapster ide info #1821

merged 35 commits into from
Mar 2, 2023

Conversation

scuellar
Copy link
Collaborator

This PR adds the heapster_dump_ide_info command to Heapster. The new instruction produces a json file with Heapster permissions for each code block. The 'json' file can then be used by the VSCode extension to display the permissions on each block of source C code.

This branch was developped a year ago and so the last handful of commits are bringing it up to date with master. We should merge it before it falls behind again.

The key files to look at are:

  • IDESupport.hs creates the structures that gather the permission logs that will be exported to json
  • JSONExport.hs has the JSON instance declarations and the logic to export the permissions.
  • NamedMb.hs Creates a wrapper around the old Mb that includes human readable names for variables, objects and code. Most of the changes are transforming Mb instances into Mb' instances
  • Implication.hs has a new error type that is more descriptive and provides feedback when the derivation fails. This is passed to the json file and can be seen from the VSCode extension.

Karl Smeltzer and others added 30 commits June 28, 2021 13:35
@eddywestbrook
Copy link
Contributor

@scuellar it looks like the build is failing, due to some pattern-matching coverage warnings. Could you please take a shot at fixing these?

@eddywestbrook eddywestbrook added the subsystem: heapster Issues specifically related to memory verification using Heapster label Feb 28, 2023
Eddy Westbrook added 3 commits February 28, 2023 16:59
…nged the names of all of its operationsto use 'Named' as a suffix instead of just using a prime
Copy link
Contributor

@eddywestbrook eddywestbrook left a comment

Choose a reason for hiding this comment

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

I worked closely with Karl and Eric M when they originally made this PR, so I'm pretty familiar with it. It adds some very useful functionality, specifically, the ability to export a JSON representation of a type-checked Crucible term, so that a UI can display that to the user.

@eddywestbrook
Copy link
Contributor

Hmm, I'm now getting a seg fault on this branch on my local machine. Still debugging...

@eddywestbrook eddywestbrook self-requested a review March 2, 2023 01:11
@eddywestbrook eddywestbrook added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Mar 2, 2023
@eddywestbrook
Copy link
Contributor

Never mind, it was a known issue with GHC 9.0. It works with GHC 8.10.4. So let's merge this sucker!

@eddywestbrook eddywestbrook merged commit 9d66afc into master Mar 2, 2023
Copy link

@KarmaHaze KarmaHaze left a comment

Choose a reason for hiding this comment

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

@mergify mergify bot deleted the heapster-ide-info branch March 27, 2023 14:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants