Using Boolean value as condition causes exception in Z3

[jklmnn]

Using a boolean variable or field as a condition value as follows:

package Test is

   type Tag is (Tag_A, Tag_B) with Size => 8;

   type Message (Has_Tag : Boolean) is
      message
         Tag_1 : Tag
            then Tag_2
               if Has_Tag
            then null
               if Has_Tag = False;
         Tag_2 : Tag;
      end message;

end Test;

Causes the following error:

Parsing test.rflx
Processing Test                                                                                                       

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.7.0                                                                                               
attrs 20.3.0
icontract 2.5.0                                                                                                       
pydotplus 2.0.2
z3-solver 4.8.10.0                                                                                                                                                                                                                          
                                                           
Optimized: True
                                                           
Command: /.../RecordFlux/venv/bin/rflx check test.rflx

Traceback (most recent call last):                                                                                                                                                                                                          
  File "/.../RecordFlux/rflx/cli.py", line 120, in main                                                                                                                                                                       
    args.func(args)                                                                                                                                                                                                                         
  File "/.../RecordFlux/rflx/cli.py", line 161, in check                                                                                                                                                                      
    parse(args.files, args.no_verification, args.workers)                                                                                                                                                                                   
  File "/.../RecordFlux/rflx/cli.py", line 208, in parse                                                                                                                                                                      
    model = parser.create_model()                                                                                                                                                                                                           
  File "/.../RecordFlux/rflx/specification/parser.py", line 1543, in create_model                                                                                                                                             
    self.__evaluate_specification(error, spec_node.spec, spec_node.filename)                                                                                                                                                                
  File "/.../RecordFlux/rflx/specification/parser.py", line 1591, in __evaluate_specification                                                                                                                                 
    new_type = handlers[t.f_definition.kind_name](                                                                    
  File "/.../RecordFlux/rflx/specification/parser.py", line 804, in create_message                      
    result = create_proven_message(                                                                                   
  File "/.../RecordFlux/rflx/specification/parser.py", line 1288, in create_proven_message              
    proven_message = unproven_message.proven(                                                                         
  File "/.../RecordFlux/rflx/model/message.py", line 1844, in proven 
    return Message(                                                                                                   
  File "/.../RecordFlux/rflx/model/message.py", line 749, in __init__                                   
    self.verify()                                                                                                     
  File "/.../RecordFlux/rflx/model/message.py", line 755, in verify                                     
    self.__verify_expression_types()                
  File "/.../RecordFlux/rflx/model/message.py", line 1060, in __verify_expression_types                 
    proof = self.__prove_path_property(expr.TRUE, p)                                                                  
  File "/.../RecordFlux/rflx/model/message.py", line 1729, in __prove_path_property                     
    return prop.check([*self.type_constraints(prop), *conditions, *sizes])
  File "/.../RecordFlux/rflx/expression.py", line 261, in check                                         
    return Proof(self, facts)                                                                                         
  File "/.../RecordFlux/rflx/expression.py", line 58, in __init__                                       
    solver.add(f.z3expr())                                                                                            
  File "/.../RecordFlux/venv/lib/python3.9/site-packages/z3/z3.py", line 6613, in add                   
    self.assert_exprs(*args)                                                                                                                                                                                                                
  File "/.../RecordFlux/venv/lib/python3.9/site-packages/z3/z3.py", line 6602, in assert_exprs          
    Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
  File "/.../RecordFlux/venv/lib/python3.9/site-packages/z3/z3core.py", line 3754, in Z3_solver_assert
    _elems.Check(a0)                                      
  File "/.../RecordFlux/venv/lib/python3.9/site-packages/z3/z3core.py", line 1414, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'invalid argument'                                                                           

----------------------------------------------------------------------------

[senier]

Looks related to #611

[jklmnn]

I noticed an architectural problem when setting the types. In message.py:Message.verify the function self._verify_expression_types does two things: It checks that no path contains any contradictions and that all variables are defined in that order. If no types are set this seems to work. With the changes introduced with this issue the types are not only set for conditions but also for type constraints. This causes a mismatch when the types of the conditions are not set which will then cause a Z3 exception. This is generally the case when a variable is not defined.

I think the proper fix to that problem is to move the check if all variables are set before the path condition check and abort checking the message when a variable is not defined. While this seems to conflict with the approach to gather as many errors as possible before aborting I think we cannot make any assumptions about the remaining message if it contains an unset variable.