Merge pull request #191 from marcoeilers/better_unknown_bool

Let arbitrary boolean values used in MaySet encoding depend on reference
marcoeilers · May 9, 2024 · 8e85db3 · 8e85db3
2 parents 9ee9d5f + ea98a33
commit 8e85db3
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/src/nagini_translation/translators/common.py b/src/nagini_translation/translators/common.py
@@ -921,15 +921,15 @@ def get_fresh_int_lit(self, ctx: Context) -> Expr:
         return self.viper.IntLit(ctx.get_fresh_int(), self.no_position(ctx),
                                  self.no_info(ctx))
 
-    def get_unknown_bool(self, ctx: Context) -> Expr:
+    def get_unknown_bool(self, arg: Expr, ctx: Context) -> Expr:
         """
-        Returns an arbitrary but fixed boolean value.
+        Returns an arbitrary but fixed boolean value that depends on the value of arg.
         """
         pos = self.no_position(ctx)
         info = self.no_info(ctx)
         fresh_int = self.get_fresh_int_lit(ctx)
         param = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
-        return self.viper.FuncApp(ARBITRARY_BOOL_FUNC, [fresh_int], pos, info,
+        return self.viper.FuncApp(ARBITRARY_BOOL_FUNC, [fresh_int, self.to_ref(arg, ctx)], pos, info,
                                   self.viper.Bool, [param])
 
     def _conjoin(self, eqs: List[Expr], pos: Position, info: Info) -> Expr:

diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py
@@ -312,7 +312,7 @@ def translate_may_set(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
                                                 pos, info)
         result_ex = self.viper.CondExp(have_normal_perm, normal_acc, may_set_pred, pos,
                                        info)
-        unknown = self.get_unknown_bool(ctx)
+        unknown = self.get_unknown_bool(rec, ctx)
         result_in = self.viper.CondExp(unknown, normal_acc, may_set_pred, pos, info)
         return [], self.viper.InhaleExhaleExp(result_in, result_ex, pos, info)
 

diff --git a/src/nagini_translation/translators/program.py b/src/nagini_translation/translators/program.py
@@ -688,7 +688,8 @@ def create_arbitrary_bool_func(self, ctx: Context) -> 'silver.ast.Function':
         pos = self.no_position(ctx)
         info = self.no_info(ctx)
         i_param_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
-        return self.viper.Function(ARBITRARY_BOOL_FUNC, [i_param_decl],
+        r_param_decl = self.viper.LocalVarDecl('r', self.viper.Ref, pos, info)
+        return self.viper.Function(ARBITRARY_BOOL_FUNC, [i_param_decl, r_param_decl],
                                    self.viper.Bool, [], [], None, pos, info)
 
     def create_may_set_predicate(self, ctx: Context) -> 'silver.ast.Predicate':