search

CozySynthesizer / cozy

The collection synthesizer
https://cozy.uwplse.org
Apache License 2.0
209 stars 18 forks source link

use extern to compare string with string literal causes model validation error #63

Closed izgzhen closed 6 years ago

izgzhen commented 6 years ago

spec:

Redmine:
    handletype ProjectModule = {
        id : Int,
        name : String
    }
    handletype Project = {
        id : Int,
        status : Int,
        modules : Bag<ProjectModule>
    }
    handletype IssueStatus = {
        id : Int,
        is_closed : Bool
    }
    handletype Issue = {
        id : Int,
        author_id : Int,
        project : Project,
        statuses : Bag<IssueStatus>,
        assigned_to : Int
    }
    extern is_issue_tracking(x : String) : Bool = "x == \"issue_tracking\""
    state issues : Bag<Issue>
    query countIssues(p1 : Int)
        len [ i | i <- issues,
                  i.val.project.val.status != 9,
                  exists [ m | m <- i.val.project.val.modules, is_issue_tracking(m.val.name) ],
                  i.val.assigned_to == p1,
                  exists [ s | s <- i.val.statuses, s.val.is_closed == false ] ]
Traceback (most recent call last):
  File "/home/zgzhen/projects/cozy/cozy/jobs.py", line 29, in _run
    self.run()
  File "/home/zgzhen/projects/cozy/cozy/synthesis/high_level_interface.py", line 85, in run
    ops=self.ops)):
  File "/home/zgzhen/projects/cozy/cozy/synthesis/core.py", line 198, in improve
    counterexample = solver.satisfy(ENot(EEq(target, new_target)))
  File "/home/zgzhen/projects/cozy/cozy/solver.py", line 1297, in satisfy
    x = self.solver.satisfy(e)
  File "/home/zgzhen/projects/cozy/cozy/solver.py", line 1251, in satisfy
    raise ModelValidationError("model validation failed {}".format(e))
cozy.solver.ModelValidationError: model validation failed EUnaryOp('not', EBinOp(EUnaryOp('len', EMap(EFilter(EStateVar(EVar('issues').with_type(TBag(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))))).with_type(TBag(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))))), ELambda(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), EBinOp(EBinOp(EBinOp(EUnaryOp('exists', EMap(EFilter(EGetField(EGetField(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), 'val').with_type(TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))), 'statuses').with_type(TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ELambda(EVar('s').with_type(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool()))))), EBinOp(EGetField(EGetField(EVar('s').with_type(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool()))))), 'val').with_type(TRecord((('id', TInt()), ('is_closed', TBool())))), 'is_closed').with_type(TBool()), '==', EBool(False).with_type(TBool())).with_type(TBool()))).with_type(TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ELambda(EVar('s').with_type(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool()))))), EVar('s').with_type(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool()))))))).with_type(TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool()))))))).with_type(TBool()), 'and', EBinOp(EGetField(EGetField(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), 'val').with_type(TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))), 'assigned_to').with_type(TInt()), '==', EVar('p1').with_type(TInt())).with_type(TBool())).with_type(TBool()), 'and', EUnaryOp('exists', EMap(EFilter(EGetField(EGetField(EGetField(EGetField(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), 'val').with_type(TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))), 'project').with_type(THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), 'val').with_type(TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))))))), 'modules').with_type(TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))), ELambda(EVar('m').with_type(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))), ECall('is_issue_tracking', (EGetField(EGetField(EVar('m').with_type(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))), 'val').with_type(TRecord((('id', TInt()), ('name', TString())))), 'name').with_type(TString()),)).with_type(TBool()))).with_type(TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))), ELambda(EVar('m').with_type(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))), EVar('m').with_type(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))))).with_type(TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))))).with_type(TBool())).with_type(TBool()), 'and', EBinOp(EGetField(EGetField(EGetField(EGetField(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), 'val').with_type(TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))), 'project').with_type(THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), 'val').with_type(TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString()))))))))), 'status').with_type(TInt()), '!=', ENum(9).with_type(TInt())).with_type(TBool())).with_type(TBool()))).with_type(TBag(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt())))))), ELambda(EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))), EVar('i').with_type(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))))).with_type(TBag(THandle('Issue', TRecord((('id', TInt()), ('author_id', TInt()), ('project', THandle('Project', TRecord((('id', TInt()), ('status', TInt()), ('modules', TBag(THandle('ProjectModule', TRecord((('id', TInt()), ('name', TString())))))))))), ('statuses', TBag(THandle('IssueStatus', TRecord((('id', TInt()), ('is_closed', TBool())))))), ('assigned_to', TInt()))))))).with_type(TInt()), '==', ENum(0).with_type(TInt())).with_type(TBool())).with_type(TBool())
failed job: ImproveQueryJob[countIssues]
Stopping jobs
requesting stop for ImproveQueryJob[countIssues]
Stopping SafeQueue...
Done!
Generating IR...
Inlining calls...
Loading concretization functions...

_var262 : Bag<Issue> = issues

Redmine:
  type ProjectModule = ProjectModule
  type Project = Project
  type IssueStatus = IssueStatus
  type Issue = Issue
  state _var262 : Bag<Issue>

  query countIssues(p1 : Int):
    (len Map {i -> i} (Filter {i -> ((((exists Map {s -> s} (Filter {s -> (((s).val).is_closed == false)} (((i).val).statuses))) and (((i).val).assigned_to == p1)) and (exists Map {m -> m} (Filter {m -> is_issue_tracking(((m).val).name)} (((((i).val).project).val).modules)))) and (((((i).val).project).val).status != 9))} (_var262)))

the e is printed by updated raise ModelValidationError("model validation failed {}".format(e)) line, which I think is the same e passed to the satisfy function.

Calvin-L commented 6 years ago

If you look at /tmp/countIssues.log you should see the full call, but I think this should be enough to go on.

izgzhen commented 6 years ago

countIssues.log

Calvin-L commented 6 years ago

Also, unrelated: the extern declaration should be "{x} == \"issue_tracking\"". Variables need to be wrapped in braces to distinguish them from keywords in the target language (e.g. Java).

izgzhen commented 6 years ago

Also, unrelated: the extern declaration should be "{x} == \"issue_tracking\"". Variables need to be wrapped in braces to distinguish them from keywords in the target language (e.g. Java).

ah, I see. I think it is my typo.

Calvin-L commented 6 years ago

This will take some time to address. Cozy assumes that Z3's model for uninterpreted functions is a mapping from inputs to outputs, with a default fallback value. (See mkfunc in solver.py.) In reality, the default value in the mapping is a formula that can refer to inputs, meaning we have to do a lot more work to extract functions in the Z3 model as native Python objects.

I will continue working on this, but it is unlikely I will finish today.

Calvin-L commented 6 years ago

Also, could you run python3 -c 'import z3; print(z3.get_version_string())' and send me the output? On my machine this issue is caught earlier by an internal Z3 library routine. I think there might be a difference between our Z3 library versions.

izgzhen commented 6 years ago

Also, could you run python3 -c 'import z3; print(z3.get_version_string())' and send me the output? On my machine this issue is caught earlier by an internal Z3 library routine. I think there might be a difference between our Z3 library versions.

My version is 4.8.0

Thanks!

Calvin-L commented 6 years ago

Hm, that's the same as me. Not sure what the difference is, then.