Use Asrt.t instead of fixes!

[N1ark]

• Remove c_fix_t from SMemory, use Asrt.t instead
• Remove fix_t from State, use Asrt.t instead
• Simplify the signature of get_fixes: err_t -> (Asrt.t list * Containers.SS.t) list (ie. remove PFS, TypeEnv and State; the error should be enough to generate fixes)
• Remove apply_fix, pp_fix_t, fix_t
• Adapt Gillian instantiations to match

(ping @NatKarmios / @giltho!)

[giltho]

Why are SpecVar fixes required?

[giltho]

But also thank you, I wanted to have this forever! This is really nice

[N1ark]

Why are SpecVar fixes required?

Well I'm not 100% sure they're needed; they just list the logical variables that need to be kept for the specification and can't be removed/renamed, I think? Didn't try to get rid of them

[N1ark]

Hmm turns out SpecVars was apparently not needed? When running my biab tests I get the same results for WISL+C except that one postcondition for one C spec has one less logical variable, which is not used anyway:

  spec listPrepend (x, z)
    [[ (x == #x) *
       (z == #z) *
       (#x == {{ _$l_40, _lvar_7 }}) *
       (#z == {{ "long", 0i }}) *
       (0i i<=# _lvar_7) *
       (0i i<=# (l-len #x)) *
       (0i i<=# (l-len #z)) *
       types(#x : List, _lvar_7 : Int, _lvar_34 : Int, #z : List) *
       types(_lvar_34 : Int) *
       <mem_single>(_$l_40, (8i i+ _lvar_7), "ptr"; {{ _$l_39, _lvar_34 }}, "Freeable") ]]
    [[ (ret == #x) *
       (#x == {{ _$l_35, _lvar_7 }}) *
       (#z == {{ "long", 0i }}) *
-      (_lvar_33 == _$l_36) *
       (_lvar_8 == _$l_35) *
       (0i i<=# _lvar_7) *
       (0i i<=# (l-len #x)) *
       (0i i<=# (l-len #z)) *
       types(#x : List, _lvar_7 : Int, _lvar_8 : Obj, _lvar_34 : Int, 
+            #z : List) *
-            #z : List, _lvar_33 : Obj) *
       types(l-nth(#z, 1i) : Int) *
       <mem_single>(_$l_35, (8i i+ _lvar_7), "ptr"; {{ "long", l-nth(#z, 1i) }}, "Freeable") ]]

[N1ark]

So basically I removed everything fix-related and now fixes are simple assertions :) The only thing is I throw an error when the fix encountered is a Wand/Pred since I'm not really sure these are ok fixes anyways (in particular Wand; does it make any sense?)

[giltho]

It looks like the specvars are needed

This is master for bi-abduction on collections-c:

This is current version of this PR:

This is version of this PR with the SpecVar still there:

[giltho]

I'm impressed at how you get EXACTLY the same results by using Asrt.t as fixes

[giltho]

What I'm thinking is that SpecVars shouldn't be fixed, but they still need to be properly added:
any logical variable that makes it to the pre-condition should be added as a specvar in the state, at risk of disconnecting things otherwise.
So we don't need specific specvar fixes, it's just that when you're producing a given fix: Asrt.t, you should get Asrt.lvars fix and add those to the specvars, in both the current state and anti-frame

[giltho]

What I'm running, btw, is :

opam exec -- dune exec -- gillian-c act \
  ../collections-c-for-gillian/gillian-compcert/biabduction/array/array_test_add.c \
  -I ../collections-c-for-gillian/gillian-compcert/utils \
  -I ../collections-c-for-gillian/libs/fixed-bi/include \
  -S ../collections-c-for-gillian/gillian-compcert/utils \
  -S ../collections-c-for-gillian/libs/fixed-bi \
  --ignore-undef --allocated-functions --ignore-multdef \
  --bi-unroll 3 -l disabled

where collections-c-for-gillian is cloned next to Gillian

[N1ark]

Ahhhh right yes! Ok makes sense, I'll fix this then
And yeah I had already gone through the changes for C for my state model library so I more or less copy pasted the change :P
Thanks for checking for SpecVars, it did feel odd I guess

[N1ark]

Oh wow just 2 lines of code were enough to re-add the spec vars automatically! Cool now same results as before

[N1ark]

Also fyi I have a branch (https://github.com/N1ark/Gillian/tree/asrt-as-list) to try to remove Star from Asrt.t and basically do as #159 suggests because it seemed like a related simple change, currently running into a few issues with the C instantiation and AWS but hopefully should be mergeable soon :)

[giltho]

👀👀👀👀👀👀

[giltho]

Merging when CI's done

[giltho]

I think CI is done now lmao