Proposal: Globals (pre-cursor to Compilation Units) #30

gmalecha · 2018-09-10T13:13:16Z

This generalizes functions into globals. It still doesn't support function pointers though doing so is relatively simple. In summary,

funname -> globname

expr := ..
  | global (_ : globname)

Because it was simple, I also changed call from taking a funname to taking an expr (so f becomes global f). Generalizing the semantics completely isn't too difficult. I can add that to this PR if it would be useful. #27 is preventing a complete operational semantics, but if we solve that, it shouldn't be difficult to do this.

gmalecha · 2018-09-10T13:15:17Z

Just a note, on top of this definition we would have something like:

Record module :=
{ imports : list globname
; definitions : map globname (function + data)
; exports : list globname
}.

samuelgruetter · 2018-09-11T01:35:51Z

bedrock2/src/WeakestPrecondition.v

@@ -46,7 +49,7 @@ Section WeakestPrecondition.
  End WithF.

  Section WithFunctions.
-    Context (call : funname -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
+    Context (call : word -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).


funname should remain abstract in this file

It is abstract, in this version of the semantics you don't call a funname, you call the word that it resolves to.

Further clarification. The resolve function maps globname to option word and global g denotes to resolve g (if it is defined). So previously, if you wanted to say that ""swap" has this specification", you would now say "resolve "swap" has this specification".

It wouldn't be difficult to remove this functionality (just don't allow calling expressions), if that is truly desireable. This seems like an easy way to support function pointers within the "be concrete" mantra of bedrock2.

I'd like to be able to use the file WeakestPrecondition.v with funname being instantitated to string, while others might want to instantiate it to word or to Z or whatever. Can you adapt it so that this becomes possible again?

samuelgruetter · 2018-09-11T02:01:34Z

I'd like to see what compiler.ExprImp.eval_cmd looks like with this (I think this could be done before or after moving the semantics in ExprImp.v from the compiler folder to the bedrock2 folder, whatever seems more convenient).

I still believe that funname and globname should be two different abstract types (but of course you can have files inside which the two are defined to be the same, if all users of such files are ok with it). But since I'm not working with functions myself at the moment, I'm fine with using the same name for funname and globname for the moment, and once I start working with functions myself, I'll see whether/why I want to separate them, so be prepared that I'll want to change it, but for the moment I'm ok to stick to the YAGNI principle 😉

"Because it was simple" is not a good reason for replacing funname by expr in call. Could you make the change in such a way that there's a simple way to restrict the input language back to what we have now for users who wish to do so?

samuelgruetter · 2018-09-11T02:04:26Z

bedrock2/src/CompilationUnit.v

+Require Import Coq.ZArith.BinIntDef.
+Require Import ExtLib.Data.HList.
+Require Import ExtLib.Data.Fin.
+Require Import ExtLib.Data.Map.FMapAList.


looks like these ExtLib dependencies are not needed (but make the build fail)

gmalecha · 2018-09-11T02:37:46Z

@samuelgruetter I've ported compiler.ExprImp.eval_cmd. As the diff shows, it is mostly just alpha renaming and adding some cases for the global constructor.

If you can think of any reason within the compiler to separate the two, I'd be really interested in knowing what it is.

I've reverted the ability to call expressions per your request. I guess we can also drop the call_rec function that I implemented.

samuelgruetter · 2018-09-11T20:06:47Z

In the latest build, ExprImp.v is never compiled, because the build fails before that. Before I spend more time on trying to understand what you're doing, would you mind making sure that ExprImp.v is compiled by travis?

- the automation needs some work right now.

gmalecha · 2018-09-12T00:53:30Z

@samuelgruetter The only thing that didn't compile in the bedrock2 directory is the swap example. I've updated that with the latest push. Now what breaks is in the compiler directory.

samuelgruetter · 2018-09-12T03:40:30Z

compiler/src/ExprImp.v


  Context {stateMap: MapFunctions var (mword)}.
  Notation state := (map var mword).
  Context {varset: SetFunctions var}.
  Notation vars := (set var).

+  Variable resolve : glob -> option word.


nitpick: I'd prefer mword over word here, even though both refer to the same in this context, it's just that this file consistently uses mword. Or if you prefer, you could make sure nothing of bbv is imported to avoid confusion with bbv's word, and then replace all occurrences of mword by word.

That's fine. Does nitpicking mean that you're considering merging this?

If you think that you want to keep using and contributing to (a part of) the code in this repo, and you tell me that merging this would enable you to do so, and you're willing to fix what you broke in the compiler subdirectory so that the build becomes green, and you're willing to deal with further potential nitpicks from my side, then I'd be happy to merge it

compilation units.

6b118a3

gmalecha added 3 commits September 10, 2018 14:44

allow for recursive functions.

4dd974a

very rough sketch of what a compilation unit might look like.

ae9de05

only export the exports

bafffad

samuelgruetter reviewed Sep 11, 2018

View reviewed changes

gmalecha added 2 commits September 10, 2018 22:14

reverting function pointers.

c8c1d75

porting ExprImp.

8e9acb2

fixing the broken proofs in the bedrock2 directory

2ad2788

- the automation needs some work right now.

samuelgruetter reviewed Sep 12, 2018

View reviewed changes

verification condition for compilation units.

dd1f540

andres-erbsen force-pushed the master branch from 7a467d7 to 9b427dc Compare March 11, 2019 22:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Proposal: Globals (pre-cursor to Compilation Units) #30

Proposal: Globals (pre-cursor to Compilation Units) #30

gmalecha commented Sep 10, 2018

gmalecha commented Sep 10, 2018 •

edited

samuelgruetter Sep 11, 2018

gmalecha Sep 11, 2018

gmalecha Sep 11, 2018

gmalecha Sep 11, 2018

samuelgruetter Sep 12, 2018

samuelgruetter commented Sep 11, 2018

samuelgruetter Sep 11, 2018

gmalecha commented Sep 11, 2018

samuelgruetter commented Sep 11, 2018

gmalecha commented Sep 12, 2018

samuelgruetter Sep 12, 2018

gmalecha Sep 12, 2018

samuelgruetter Sep 12, 2018

Proposal: Globals (pre-cursor to Compilation Units) #30

Are you sure you want to change the base?

Proposal: Globals (pre-cursor to Compilation Units) #30

Conversation

gmalecha commented Sep 10, 2018

gmalecha commented Sep 10, 2018 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

samuelgruetter commented Sep 11, 2018

Choose a reason for hiding this comment

gmalecha commented Sep 11, 2018

samuelgruetter commented Sep 11, 2018

gmalecha commented Sep 12, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gmalecha commented Sep 10, 2018 •

edited