ambiguous variable names in print_goal

[msaaltink]

When printing out proof goals, some confusion can arise if a function with a postcondition is called more than once. For example, with this simple C code

#include <stdint.h>

void bump(uint32_t *x) {
  *x += 1;
};

uint32_t bump2() {
  uint32_t y = 0;
  bump(&y);
  bump(&y);
  return y;
}

and this SAWscript

m <- llvm_load_module "naming.bc";

let u32 = llvm_int 32;

let bump_spec = do {
  x <- crucible_fresh_var "x" u32;
  xp <-crucible_alloc u32;
  crucible_points_to xp (crucible_term x);
  crucible_execute_func [xp];
  x' <- crucible_fresh_var "x'" u32;
  crucible_points_to xp (crucible_term x');
  crucible_postcond {{  x' == x+1 }};
  };

bump_ov <- crucible_llvm_verify m "bump" [] false bump_spec z3;

let bump2_spec = do {
  crucible_execute_func [];
  crucible_return (crucible_term {{ 2:[32] }});
  };

bump_ov <- crucible_llvm_verify m "bump2" [bump_ov] false bump2_spec do { print_goal; z3; };

we get this output:

Goal bump2 (safety assertion:):
let { x@1 = Prelude.Vec 32 Prelude.Bool
      x@2 = Prelude.bvNat 32 1
      x@3 = Cryptol.PEqWord 32
    }
 in Prelude.EqTrue
      (Prelude.implies Prelude.True
         (Prelude.implies
            (Prelude.and (Cryptol.ecEq x@1 x@3 x' x@2)
               (Cryptol.ecEq x@1 x@3 x' (Prelude.bvAdd 32 x' x@2)))
            (Prelude.eq x@1 x' (Prelude.bvNat 32 2))))

It can be seen that there are two different variable called x'. Here it is not too hard to work out which is which, but in larger proof goals it can be quite difficult.

[brianhuffman]

For Pi-bound or lambda-bound variables, the saw-core pretty printer adds suffixes to prevent name clashes. On the other hand, for ExtCns variables (like those made with fresh_symbolic) we have unique IDs to disambiguate them internally but those don't show up during printing.

We're planning to do some redesign of name handling in saw-core very soon (GaloisInc/saw-core#84) and this problem should be taken care of as part of that effort.

[brianhuffman]

We've made a bunch of changes to name handling in saw-core in the last few months, so we need to revisit this and see if it's still a problem.

[msaaltink]

On a recent (May 2) build, this still prints two indistinguishable names x'. The output is a bit different, but the issue remains.

[brianhuffman]

I found the source of the bug, in function refreshTerms:

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Lines 701 to 714 in 2e4fc06

	-- | Allocate fresh variables for all of the "fresh" vars
	-- used in this phase and add them to the term substitution.
	refreshTerms ::
	SharedContext {- ^ shared context -} ->
	MS.StateSpec (LLVM arch) {- ^ current phase spec -} ->
	OverrideMatcher (LLVM arch) md ()
	refreshTerms sc ss =
	do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
	OM (termSub %= Map.union extension)
	where
	freshenTerm (TypedExtCns _cty ec) =
	do new <- liftIO $ do i <- scFreshGlobalVar sc
	scExtCns sc (EC i (ecName ec) (ecType ec))
	return (ecVarIndex ec, new)

This function is called whenever you apply an override that uses crucible_fresh_var in its post-condition section, which is when you're supposed to create a fresh saw-core ExtCns variable. Each ExtCns contains both a VarIndex (which must be unique) and a NameInfo. The SharedContext maintains a mapping from NameInfo URIs to VarIndex.

So here's the problem: When refreshTerms runs, it takes an existing ExtCns, generates a new VarIndex for it, and then reuses the same NameInfo. This is already bad, since each NameInfo can only be associated with a single VarIndex. The reason it goes undetected is that refreshTerms never tries to register the NameInfo with the fresh VarIndex in the SharedContext (it uses the lower-level function scExtCns instead of scFreshEC, which also does name registration). Finally, the pretty printer ignores the VarIndex and only looks at the NameInfo, so it thinks that all the variables are actually the same; according to the naming environment, only one variable named x' was ever registered, so it thinks that it's an unambiguous name.

To protect against this kind of problem in the future, we should probably remove the low-level scExtCns function from the SharedTerm API, and require all ExtCns variables to be created with scFreshEC or something similar. This way we can enforce that all ExtCns variables have their names properly registered.

[robdockins]

I think removing scExtCns might be the wrong approach (it's important for some of the term-to-term evaluation work I'm doing). Perhaps we could make the ExtCns type opaque and limit the ways they can be created, since the real problem here is that the NameInfo was reused wiht a different VarIndex.

[brianhuffman]

For now I think I'll fix the problem by rewriting refreshTerms to use scFreshEC instead of scExtCns. If we decide we want to change the shared term API to prevent future bugs like this, we can address that separately at a later time.