search

CozySynthesizer / cozy

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

support code-gen for TTuple construction #73

Closed izgzhen closed 5 years ago

izgzhen commented 5 years ago

fixes #70

izgzhen commented 5 years ago 
Traceback (most recent call last):
  File "/home/zgzhen/repos/cozy/cozy/jobs.py", line 29, in _run
    self.run()
  File "/home/zgzhen/repos/cozy/cozy/synthesis/high_level_interface.py", line 85, in run
    ops=self.ops)):
  File "/home/zgzhen/repos/cozy/cozy/synthesis/core.py", line 197, in improve
    assert is_good, "WARNING: this target is already a bad idea\n is_good = {}, target = {}".format(is_good, target)
AssertionError: WARNING: this target is already a bad idea
 is_good = no: collection of nonscalar: e EMap(EStateVar(EVar('classes').with_type(TBag(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))))).with_type(TBag(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))))), ELambda(EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), ETuple((EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), EMap(EFilter(EGetField(EGetField(EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), 'val').with_type(TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), 'members').with_type(TBag(TRecord((('id', TInt()), ('name', TString()))))), ELambda(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), EBinOp(EGetField(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), 'id').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TRecord((('id', TInt()), ('name', TString()))))), ELambda(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), EGetField(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), 'id').with_type(TInt()))).with_type(TBag(TInt())))).with_type(TTuple((THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), TBag(TInt())))))).with_type(TBag(TTuple((THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), TBag(TInt())))))
 elem_type: TTuple((THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), TBag(TInt())))
, target = EMap(EStateVar(EVar('classes').with_type(TBag(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))))).with_type(TBag(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))))), ELambda(EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), ETuple((EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), EMap(EFilter(EGetField(EGetField(EVar('c').with_type(THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString()))))))))), 'val').with_type(TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), 'members').with_type(TBag(TRecord((('id', TInt()), ('name', TString()))))), ELambda(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), EBinOp(EGetField(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), 'id').with_type(TInt()), '>', ENum(10).with_type(TInt())).with_type(TBool()))).with_type(TBag(TRecord((('id', TInt()), ('name', TString()))))), ELambda(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), EGetField(EVar('m').with_type(TRecord((('id', TInt()), ('name', TString())))), 'id').with_type(TInt()))).with_type(TBag(TInt())))).with_type(TTuple((THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), TBag(TInt())))))).with_type(TBag(TTuple((THandle('Clz', TRecord((('id', TInt()), ('members', TBag(TRecord((('id', TInt()), ('name', TString())))))))), TBag(TInt())))))
izgzhen commented 5 years ago

the traceback comes from cozy examples/codegen.ds --java codegen.java (the ds example is just pushed to this PR).

izgzhen commented 5 years ago

synthesis core considers this non-scalar not supported. I previously thought that this is a code-gen only problem.

Calvin-L commented 5 years ago

@izgzhen the trace you pasted is a separate, deep-seated restriction in Cozy's internals. Removing it will require a lot of work and should be handled separately (if at all).

I suspect that this fix is necessary whether or not we remove that restriction. We can probably construct specifications that use this code even without collections of non-scalars.

izgzhen commented 5 years ago

@izgzhen the trace you pasted is a separate, deep-seated restriction in Cozy's internals. Removing it will require a lot of work and should be handled separately (if at all).

I see. I just realized that cozy threw two exceptions, one is the failure in improving the query (because core is not happy), and second is in codegen stage.

It is also curious to me that the generated java code is actually correct, despite the core is unhappy.

izgzhen commented 5 years ago

I think maybe we can merge this