[CN] Feature: add logical implication to the spec language

[septract]

Currently: CN's spec language only supports C's ternary conditional operator B ? P : Q

Ideally: CN should support logical implication A ==> B (or whatever symbol we prefer for implication - but I suggest we use ==> which is the ACSL / FramaC's syntax).

How: Desugar to a ternary conditional, or duplicate and modify the code which supports the ternary conditional.

This might be an easy first change for someone diving into the CN codebase.

[elaustell]

Where is the code that supports the ternary conditional?

[dc-mak]

@elaustell it starts here

cerberus/parsers/c/c_parser.mly

Line 2071 in 4b3b206

| e1= list_expr QUESTION e2= list_expr COLON e3= list_expr

And ends up hitting this

cerberus/backend/cn/terms.ml

Line 78 in 4b3b206

| ITE of 'bt term * 'bt term * 'bt term

Though for the sake of location info fidelity it's probably worth just adding it as new construct.

[elaustell]

I notice that there is already some support for impl in the codebase here

cerberus/backend/cn/terms.ml

Lines 192 to 193 in c6524d2

	| Impl ->
	mparens (flow (break_op (minus ^^ rangle ())) [aux true it1; aux true it2])

which appears to have -> as the impl syntax. However I know @bcpierce00 mentioned using -> to talk about the fields of structs in ghost code. Should we change the existing support for impl to something like ==>, or leave what exists unchanged and add something else entirely?

[cp526]

Changing it to ==> sounds like a very good idea.

And regarding adding implication: I had forgotten we internally have a term for implication already; this means this change just needs additions to the frontend.

[septract]

@elaustell it sounds like you are going to implement this (thank you!). Once you are done, it would be great to also add some examples of the new syntax to the example archive and/or tutorial example set.

[elaustell]

Something else I notice (and maybe the reason it hasn't been implemented yet) is that there are currently two different uses of Impl in the code base:

cerberus/backend/absint/src/cfg.ml

Lines 274 to 276 in ec8db7e

	let show_name = function
	| Sym a -> Sym.show a
	| Impl i -> Implementation.string_of_implementation_constant i

Here, Impl seems to refer to some sort of implementation. This use of Impl is referenced in many other parts of the code base. However, Impl is also used in

cerberus/backend/cn/solver.ml

Line 794 in ec8db7e

| Impl -> Z3.Boolean.mk_implies context (term t1) (term t2)

Here, it refers to implication. There are also many cases of this use of Impl. Now that I am adding the implication Impl in more places, I am running into errors. Should I change the existing usage of Impl as an implication? Or what is the best course of action?

[kmemarian]

@cp526 @dc-mak We need to move CN to using it's own lexer before changing to ==>.

Because this will require adding a new punctuator to the lexer which in the current setup will affect base Cerberus because of CN's reuse of the C lexer. It was fine to add CN keywords because they are in a separated lexicon which we use at runtime just for CN, but we can't do that for punctuators.

[bcpierce00]

Maybe we could write it as "implies" for now? But I'm not sure this addresses Liz's confusion...

…

On Fri, Jun 21, 2024 at 6:24 PM Kayvan Memarian ***@***.***> wrote: @cp526 <https://urldefense.com/v3/__https://github.com/cp526__;!!IBzWLUs!RbcmZGRBnVdBrqnP4UYGJGcDR_kiWeWgEBHel8encmnSDw66sOPkm8KNvfCo9Z2qPokW8yn6xiO_bCHgYdSJLlVhOOcF$> @dc-mak <https://urldefense.com/v3/__https://github.com/dc-mak__;!!IBzWLUs!RbcmZGRBnVdBrqnP4UYGJGcDR_kiWeWgEBHel8encmnSDw66sOPkm8KNvfCo9Z2qPokW8yn6xiO_bCHgYdSJLog_frSr$> We need to move CN to using it's own lexer before changing to ==>. Because this will require adding a new punctuator to the lexer which in the current setup will affect base Cerberus because of CN's reuse of the C lexer. It was fine to add CN keywords because they are in a separated lexicon which we use at runtime just for CN, but we can't do that for punctuators. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/329*issuecomment-2183539207__;Iw!!IBzWLUs!RbcmZGRBnVdBrqnP4UYGJGcDR_kiWeWgEBHel8encmnSDw66sOPkm8KNvfCo9Z2qPokW8yn6xiO_bCHgYdSJLr5k-9Q1$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC6DINFZCY5TNTZHIM3ZISR2FAVCNFSM6AAAAABJOIRLRKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBTGUZTSMRQG4__;!!IBzWLUs!RbcmZGRBnVdBrqnP4UYGJGcDR_kiWeWgEBHel8encmnSDw66sOPkm8KNvfCo9Z2qPokW8yn6xiO_bCHgYdSJLqbZy3B9$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[kmemarian]

@bcpierce00 "implies" would indeed work. I started the splitting of C/CN lexers and parsers so we should be able to move to ==> soon-ish. We need to see how much of the parsing of C type-names we need to duplicate (e.g. do we need arbitrary C constant expressions in the size of C array types written from CN?).

[kmemarian]

@elaustell I had a look at your austell_addImpl branch, unless I'm misunderstanding the feature request you shouldn't be changing anything to Cabs, Ail or the rest of the pipeline in base Cerberus. You just need the new CN_impl you added to Cn.cn_binop.

And don't do merge commits of master into your branch, you should instead rebase your branch on top of master. Otherwise you won't be able to get your PR into master as the history will not be linear if there were conflicts when merging.

[dc-mak]

Just popping in to say thanks to Kayvan, and also confirm that Kayvan is correct.

cerberus/backend/cn/ONBOARDING.md

Line 34 in ec8db7e

* Rebase on master frequently (daily: `git pull --rebase master`).

Thanks for the feature! @elaustell do feel free open draft PRs and request reviews frequently so we can can discuss questions about the code (and I can get notified as a reviewer!)

[cp526]

@bcpierce00 "implies" would indeed work. I started the splitting of C/CN lexers and parsers so we should be able to move to ==> soon-ish. We need to see how much of the parsing of C type-names we need to duplicate (e.g. do we need arbitrary C constant expressions in the size of C array types written from CN?).

CN parsing of C-types should be the same as in Cerberus base; i expect if we make it less general we’ll sooner or later run into code that needs it.

Can we not make CN’s parser “import” the whole standard C parser and then build on top (even if that means including expression parsing)?

[kmemarian]

@cp526 that makes sense. Menhir has a grammar concatenation feature that would allow us to "import" the C grammar when building CN's, but that requires using the same token type for the two grammars (which would mean keeping two version in sync when Cerberus and CN are separated).

I have a first attempt that involves calling the C parser on C type-names from the CN lexer and producing CTYPE tokens. This requires a (maybe too hacky? I'm not sure what to think) recovery when the lexer first thought there was a C type-name when in fact it was a < relational operator. This seems to work, but if the hack is too offensive, a slight change to the CN syntax would make it go away.

I've created a draft PR #342 so we can move the discussion there.