search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Error of checking an element in the keys of a map when I use C options to input a configuration #789

Closed liyili2 closed 10 years ago

liyili2 commented 10 years ago

I spent two days to understand this problem really. If I have this set of rules:

module TEST

   configuration  
<T multiplicity="?">   
    <k color="green" multiplicity="?"> 
          loadMergeObj(
               unwrapObj($OBJ1:Bag), 
               unwrapObj($OBJ2:Bag))
          ~> ($PGM:K)
     </k>
<options> $OPTIONS:Set </options>
</T>
<global>
<tu>
<env>.Map</env>
</tu>
</global>

     syntax Bag ::= unwrapObj(Bag) [function]

     rule unwrapObj(<generatedTop>... 
               <global> G:Bag </global> 
          ...</generatedTop>) 
          => <global> G </global>

     rule unwrapObj(.Bag) => .Bag

     syntax KItem ::= loadMergeObj(Bag , Bag) [function]
     syntax KItem ::= loadObj(Bag)

     rule loadMergeObj(A:Bag , .Bag) => loadObj(A)
     rule loadMergeObj(.Bag , A:Bag) => loadObj(A)

     rule <k> loadObj(<global> G:Bag </global>) => .K ...</k>
          <global> (_:Bag => G) </global>
          requires (G =/=Bag .Bag)
          [structural]

     rule loadObj(.Bag) => .K
          [structural]

   syntax KItem ::= "start" | "end"

   syntax CId ::= Identifier(String)

   syntax Map ::= "builtins" [function]

   rule builtins =>
          "__debug" |-> 1
          "__fslCloseFile" |-> 1
          "__fslFGetC" |-> 2
          "__fslOpenFile" |-> 1
          "__fslPutc" |-> 1
          "__va_copy" |-> 1
          "__va_end" |-> 1
          "__va_inc" |-> 1
          "__va_start" |-> 1
          "abort" |-> 1
          "asin" |-> 1
          "atan" |-> 1
          "atan2" |-> 1
          "calloc" |-> 1
          "cos" |-> 1
          "exit" |-> 1
          "exp" |-> 1
          "floor" |-> 1
          "fmod" |-> 1
          "free" |-> 1
          "getchar" |-> 1
          "log" |-> 1
          "longjmp" |-> 1
          "malloc" |-> 1
          "mtx_init" |-> 1
          "mtx_lock" |-> 1
          "mtx_unlock" |-> 1
          "printf" |-> 1
          "putchar" |-> 1
          "rand" |-> 2
          "realloc" |-> 2
          "setjmp" |-> 2
          "sin" |-> 2
          "snprintf" |-> 2
          "sprintf" |-> 2
          "sqrt" |-> 3
          "srand" |-> 3
          "strcpy" |-> 3
          "tan" |-> 3
          "thrd_create" |-> 3
          "thrd_current" |-> 3
          "thrd_join" |-> 3
          "time" |-> 3

   syntax KItem ::= addBuiltins(Map) | addBuiltin(CId,Int)

   rule addBuiltins(.Map) => .K

   rule <k> (.K => addBuiltin(Identifier(C),I)) ~> addBuiltins((C:String |-> I:Int => .Map) S:Map)  
    ...</k>

   rule <k> addBuiltin(C:CId,I:Int) => .K ...</k>
        <env>... (.Map => C |-> I) ...</env>

   rule <T><k> true </k><options>S:Set</options> </T> => . [structural]

   rule start => addBuiltins(builtins) ~> end
   rule <k> end => (Identifier("atan") in keys(M)) ...</k><env>M:Map</env>

endmodule

and I run the program "start" by the following command:

krun --smt none --output "pretty" --output-file "ctype.pretty.o" -cOPTIONS="(SetItem(1) .Set)" -cOBJ1=".Bag" -cOBJ2=".Bag" a.test

I will get a correct result as:

<global>
    <tu>
        <env>
            Identifier ( "__debug" ) |-> 1 Identifier ( "__fslCloseFile" ) |->
               1 Identifier ( "__fslFGetC" ) |-> 2 Identifier ( 
              "__fslOpenFile" ) |-> 1 Identifier ( "__fslPutc" ) |-> 1 
              Identifier ( "__va_copy" ) |-> 1 Identifier ( "__va_end" ) |-> 1
               Identifier ( "__va_inc" ) |-> 1 Identifier ( "__va_start" ) |->
               1 Identifier ( "abort" ) |-> 1 Identifier ( "asin" ) |-> 1 
              Identifier ( "atan2" ) |-> 1 Identifier ( "atan" ) |-> 1 
              Identifier ( "calloc" ) |-> 1 Identifier ( "cos" ) |-> 1 
              Identifier ( "exit" ) |-> 1 Identifier ( "exp" ) |-> 1 
              Identifier ( "floor" ) |-> 1 Identifier ( "fmod" ) |-> 1 
              Identifier ( "free" ) |-> 1 Identifier ( "getchar" ) |-> 1 
              Identifier ( "log" ) |-> 1 Identifier ( "longjmp" ) |-> 1 
              Identifier ( "malloc" ) |-> 1 Identifier ( "mtx_init" ) |-> 1 
              Identifier ( "mtx_lock" ) |-> 1 Identifier ( "mtx_unlock" ) |-> 
              1 Identifier ( "printf" ) |-> 1 Identifier ( "putchar" ) |-> 1 
              Identifier ( "rand" ) |-> 2 Identifier ( "realloc" ) |-> 2 
              Identifier ( "setjmp" ) |-> 2 Identifier ( "sin" ) |-> 2 
              Identifier ( "snprintf" ) |-> 2 Identifier ( "sprintf" ) |-> 2 
              Identifier ( "sqrt" ) |-> 3 Identifier ( "srand" ) |-> 3 
              Identifier ( "strcpy" ) |-> 3 Identifier ( "tan" ) |-> 3 
              Identifier ( "thrd_create" ) |-> 3 Identifier ( "thrd_current" )
               |-> 3 Identifier ( "thrd_join" ) |-> 3 Identifier ( "time" ) 
              |-> 3
        </env>
    </tu>
</global>

because K will evaluate the final boolean expression "(Identifier("atan") in keys(M))" to "true". To show the error, I will need to run the binary version of the command above as:

krun --smt none --output "binary" --output-file "ctype.o" -cOPTIONS="(SetItem(1) .Set)" -cOBJ1=".Bag" -cOBJ2=".Bag" a.test

Then, I will run another command as:

krun --smt none --output "pretty" --output-file "output.txt" -cOPTIONS="(SetItem(1) .Set)" -cOBJ1=".Bag" -pOBJ2="kast --parser binary" -cOBJ2="ctype.o" b.test

This command will input the final configuration above as a binary file "ctype.o" and run the program "end", which is in b.test. However, the Java bacend will incorrectly evaluate the final boolean expression "(Identifier("atan") in keys(M))" to "false". The final configuration of running the program "end" is:

<T>
    <k>
        false
    </k>
    <options>
        SetItem ( 1 )
    </options>
</T>
<global>
    <tu>
        <env>
            Identifier ( "__debug" ) |-> 1 Identifier ( "__fslCloseFile" ) |->
               1 Identifier ( "__fslFGetC" ) |-> 2 Identifier ( 
              "__fslOpenFile" ) |-> 1 Identifier ( "__fslPutc" ) |-> 1 
              Identifier ( "__va_copy" ) |-> 1 Identifier ( "__va_end" ) |-> 1
               Identifier ( "__va_inc" ) |-> 1 Identifier ( "__va_start" ) |->
               1 Identifier ( "abort" ) |-> 1 Identifier ( "asin" ) |-> 1 
              Identifier ( "atan2" ) |-> 1 Identifier ( "atan" ) |-> 1 
              Identifier ( "calloc" ) |-> 1 Identifier ( "cos" ) |-> 1 
              Identifier ( "exit" ) |-> 1 Identifier ( "exp" ) |-> 1 
              Identifier ( "floor" ) |-> 1 Identifier ( "fmod" ) |-> 1 
              Identifier ( "free" ) |-> 1 Identifier ( "getchar" ) |-> 1 
              Identifier ( "log" ) |-> 1 Identifier ( "longjmp" ) |-> 1 
              Identifier ( "malloc" ) |-> 1 Identifier ( "mtx_init" ) |-> 1 
              Identifier ( "mtx_lock" ) |-> 1 Identifier ( "mtx_unlock" ) |-> 
              1 Identifier ( "printf" ) |-> 1 Identifier ( "putchar" ) |-> 1 
              Identifier ( "rand" ) |-> 2 Identifier ( "realloc" ) |-> 2 
              Identifier ( "setjmp" ) |-> 2 Identifier ( "sin" ) |-> 2 
              Identifier ( "snprintf" ) |-> 2 Identifier ( "sprintf" ) |-> 2 
              Identifier ( "sqrt" ) |-> 3 Identifier ( "srand" ) |-> 3 
              Identifier ( "strcpy" ) |-> 3 Identifier ( "tan" ) |-> 3 
              Identifier ( "thrd_create" ) |-> 3 Identifier ( "thrd_current" )
               |-> 3 Identifier ( "thrd_join" ) |-> 3 Identifier ( "time" ) 
              |-> 3
        </env>
    </tu>
</global>

I expect the final configuration of running program "end" by inputing ctype.o the same as the final configuration as the final configuration by running program "start" through the command:

krun --smt none --output "pretty" --output-file "ctype.pretty.o" -cOPTIONS="(SetItem(1) .Set)" -cOBJ1=".Bag" -cOBJ2=".Bag" a.test
liyili2 commented 10 years ago

This is a small example:

module TEST

   configuration  
<T multiplicity="?">   
    <k color="green" multiplicity="?"> 
          loadMergeObj(
               unwrapObj($OBJ1:Bag), 
               unwrapObj($OBJ2:Bag))
          ~> ($PGM:K)
     </k>
<options> $OPTIONS:Set </options>
</T>
<global>
<tu>
<env>.Map</env>
</tu>
</global>

     syntax Bag ::= unwrapObj(Bag) [function]

     rule unwrapObj(<generatedTop>... 
               <global> G:Bag </global> 
          ...</generatedTop>) 
          => <global> G </global>

     rule unwrapObj(.Bag) => .Bag

     syntax KItem ::= loadMergeObj(Bag , Bag) [function]
     syntax KItem ::= loadObj(Bag)

     rule loadMergeObj(A:Bag , .Bag) => loadObj(A)
     rule loadMergeObj(.Bag , A:Bag) => loadObj(A)

     rule <k> loadObj(<global> G:Bag </global>) => .K ...</k>
          <global> (_:Bag => G) </global>
          requires (G =/=Bag .Bag)
          [structural]

     rule loadObj(.Bag) => .K
          [structural]

   syntax KItem ::= "start" | "end"

   syntax CId ::= Identifier(String)

   syntax Map ::= "builtins" [function]

   rule builtins =>
          "atan" |-> 1
          "atan2" |-> 1

   syntax KItem ::= addBuiltins(Map) | addBuiltin(CId,Int)

   rule addBuiltins(.Map) => .K

   rule <k> (.K => addBuiltin(Identifier(C),I)) ~> addBuiltins((C:String |-> I:Int => .Map) S:Map)  
    ...</k>

   rule <k> addBuiltin(C:CId,I:Int) => .K ...</k>
        <env>... (.Map => C |-> I) ...</env>

   rule <T><k> true </k><options>S:Set</options> </T> => . [structural]

   rule start => addBuiltins(builtins) ~> end
   rule <k> end => (Identifier("atan") in keys(M)) ...</k><env>M:Map</env>

endmodule

This is the expected output:

<global>
    <tu>
        <env>
            Identifier ( "atan2" ) |-> 1 Identifier ( "atan" ) |-> 1
        </env>
    </tu>
</global>

This is the actually output:

<T>
    <k>
        false
    </k>
    <options>
        SetItem ( 1 )
    </options>
</T>
<global>
    <tu>
        <env>
            Identifier ( "atan2" ) |-> 1 Identifier ( "atan" ) |-> 1
        </env>
    </tu>
</global>
liyili2 commented 10 years ago

Update some info:

I use the Java debugger to run the program. I find the main problem is from the "BuiltinSetOperations.in" function.

Evaluating the boolean expression "Identifier( "atan" ) in Identifier ( "atan2" ) Identifier ( "atan" )" will return false.

I set up a break point in the Java program of the builtin function and find that the hash code for the term of "Identifier( "atan" )" in the LHS is different from the hash code for the same term in the RHS set. They have the same klabel but they don't have the same klist, even if their klist terms look the same as "String(#""atan"")".

When I go deep in comparing the structure of their klist terms. I find that their structures are the same: "KList ---- StringToken ---- Value". However, the values are different, the LHS term has value atan, while the RHS has value "atan".

liyili2 commented 10 years ago

@yilongli , Hi, Would you mind to tell me what is the status of the bug fixing?

yilongli commented 10 years ago

I haven't got a chance to look into this issue.

yilongli commented 10 years ago

@dwightguth @andreistefanescu I am not sure how to fix this. The problem is that when you convert a Java-backend StringToken back to generic KIL in BackendJavaKILtoKILTransformer#transform(Token), the sort of the StringToken is String rather than #String, which makes org.kframework.kil.Token.kAppOf to return a GenericToken insteadof StringBuiltin. Therefore, when that GenericToken is converted to Java backend again, it becomes an UninterpretedToken. Any suggestion? Thanks.

radumereuta commented 10 years ago

The #String sort should be eliminated. So the StringToken should be created from something that has sort String instead. I tried to do that at one point, but I got so many errors from the backend that I gave up.

liyili2 commented 10 years ago

How can I proceed here. I need the problem to be solved in order to move forward for my C semantics.

On Sun, Aug 10, 2014 at 5:13 PM, Radu Mereuta notifications@github.com wrote:

The #String sort should be eliminated. So the StringToken should be created from something that has sort String instead. I tried to do that at one point, but I got so many errors from the backend that I gave up.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/789#issuecomment-51729103.

andreistefanescu commented 10 years ago

I think we should get rid of #String and the likes. I'm not sure who is best to do it...

On Sun, Aug 10, 2014 at 10:29 PM, Liyi Li notifications@github.com wrote:

How can I proceed here. I need the problem to be solved in order to move forward for my C semantics.

On Sun, Aug 10, 2014 at 5:13 PM, Radu Mereuta notifications@github.com wrote:

The #String sort should be eliminated. So the StringToken should be created from something that has sort String instead. I tried to do that at one point, but I got so many errors from the backend that I gave up.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/789#issuecomment-51729103.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/789#issuecomment-51739027.

yilongli commented 10 years ago

@radumereuta Since I have changed the sort representation from String to class, I guess the backend errors should be much easier to fix now.

radumereuta commented 10 years ago

There were also problems in the maude backend. Those are the ones that I couldn't fix.

liyili2 commented 10 years ago

what should i do to avoid the problem

yilongli commented 10 years ago

@radumereuta yeah, I am aware of that this morning when I tried to fix this issue. What about this? First, you change the front-end to eliminate #String(just this one for now). Then I continue on your branch to fix any issues in the Java backend. This should temporarily unblock the progress on C semantics.

yilongli commented 10 years ago

Try to use https://github.com/kframework/k/pull/837 as a temporary solution if all tests pass.