sawcore imports don't work correctly

[weaversa]

This may be a bit related to #1044.

Basically, saw seems to know that symbol names exist in imported saw core files, but it doesn't act on them. For example:

f : [32] -> [32]
f x = g x + 1

g : [32] -> [32]
g x = 0

import "unint.cry";

print_term (unfold_term ["f"] {{ \x -> f x > 0 }});

r <- prove (w4_unint_yices ["g"]) {{ \x -> f x > 0 }};
print r;

write_core "unint.core" {{ \x -> f x > 0 }};

prop <- read_core "unint.core";

print_term (unfold_term ["g"] {{ \x -> prop x }});

r <- prove (w4_unint_yices ["g"]) {{ \x -> prop x }};
print r;

$ saw $(pwd)/unint.saw
[15:35:38.479] Loading file "unint.saw"
[15:35:38.513] let { x@1 = Prelude.Vec 32 Prelude.Bool
      x@2 = Cryptol.TCNum 32
      x@3 = Cryptol.PLiteralSeqBool x@2
    }
 in \(x : x@1) ->
      Cryptol.ecGt x@1 (Cryptol.PCmpSeqBool x@2)
	((\(x' : x@1) ->
            Cryptol.ecPlus x@1 (Cryptol.PRingSeqBool x@2)
              (cryptol:/Main/g x')
              (Cryptol.ecNumber (Cryptol.TCNum 1) x@1 x@3))
           x)
	(Cryptol.ecNumber (Cryptol.TCNum 0) x@1 x@3)
Calling Yices to check sat
Running check sat
[15:35:38.581] prove: 1 unsolved subgoal(s)
[15:35:38.581] Invalid: [x = 0]
[15:35:38.614] let { x@1 = Prelude.Vec 32 Prelude.Bool
      x@2 = Cryptol.TCNum 32
    }
 in \(x : x@1) ->
      (\(x' : x@1) ->
         Cryptol.ecGt x@1 (Cryptol.PCmpSeqBool x@2) (cryptol:/Main/f x')
           (Cryptol.ecNumber (Cryptol.TCNum 0) x@1
              (Cryptol.PLiteralSeqBool x@2)))
        x
Calling Yices to check sat
Running check sat
[15:35:38.649] Valid

Both of these calls to yices should produce a counter example because we uninterpreted g in both. We know saw knows that g exists because saw would otherwise complain saying "Could not resolve name: g", but this does not happen. However, saw does not uninterpret g, nor does it unfold f when we try to print the term.

[brianhuffman]

I suspect that the naming environment is getting screwed up when we import an external saw-core file. I don't quite understand what's going on here yet, but something is definitely wrong under the surface. We should probably add some code (at least temporarily) to check and enforce the intended invariants on our naming environment.

[brianhuffman]

I think #1257 is also related; in that thread I mentioned some design questions about how should we handle re-import of external saw-core files that contain defined constants.