STATOR:Establishing code-base - Revision history

Marek Trtik: /* Results */

2014-07-29T09:02:51Z

Results

Marek Trtik: /* Answers to important questions */

2014-07-29T08:43:23Z

Answers to important questions

Marek Trtik: /* Answers to important questions */

2014-07-29T08:40:06Z

Answers to important questions

Marek Trtik: /* Answers to important questions */

2014-07-29T08:36:26Z

Answers to important questions

Marek Trtik: /* Answers to important questions */

2014-07-29T08:34:54Z

Answers to important questions

Marek Trtik: /* Important questions */

2014-07-29T08:33:16Z

Important questions

Marek Trtik: /* Open questions */

2014-07-29T07:29:37Z

Open questions

Marek Trtik: /* PAGAI */

2014-07-28T09:57:32Z

PAGAI

Marek Trtik: /* KLEE */

2014-07-28T09:56:57Z

KLEE

Marek Trtik: /* CPAchecker */

2014-07-28T09:51:49Z

CPAchecker

← Older revision		Revision as of 09:02, 29 July 2014
Line 229:		Line 229:

	== Results ==		== Results ==
		+
		+	We excluded OCaml's approach for these reasons:
		+	* We won't get noticeable development speed up compared to Java, since OCaml does not have any IDE.
		+	* Although we could rather easily take C front-end from either CPAchecker or Stanse and use it as en external compiler into internal CFG representation, we would not get any other code. So, taking CPAchecker seems more beneficial, from this point of view.
		+	* There are portability issues.
		+
		+
		+	We excluded F# approach for these reasons:
		+	* Although development in .NET will be fast, port to Mono may be problematic. Moreover, George does not want to switch to Windows.
		+	* Although we could rather easily take C front-end from either CPAchecker or Stanse and use it as en external compiler into internal CFG representation, we would not get any other code. So, taking CPAchecker seems more beneficial, from this point of view.
		+
		+
		+	We excluded Stanse approach for these reasons:
		+	* Only C front-end and makefile support can be reused. With CPAchecker we can get more.
		+
		+
		+	We excluded PAGAI, Bugst, KLEE, and Predator approach for these reasons:
		+	*
		+
		+
		+	We excluded the approach in which we take code from several different tools for these reasons:
		+	*
		+
		+	<b>The right approach is</b> to use a single tool CPAchecker as a code-base for STATOR. The key reasons for this decisions are:
		+	*

@@ Line 222: / Line 222: @@
 * Result from the discussion on July 28: This was not discussed.
 * Marek: In this moment I cannot say, because I do not have clear view of features of our analyses. I need to read related papers first. Even such essential things like "new-school vs. new-school" control-flow graph representation is a mystery for me. So, my opinion to this question does not matter.
 How many PhD students we plan to join the STATOR project till the end of 2017?
 * Result from the discussion on July 28: It was not discussed.
 == Results ==

@@ Line 217: / Line 217: @@
 How much restrictive is CPAchecker's concept of CPAs with respect to kind of program analyses we intend to implement in STATOR? (Of course, there is a possibility to circumvent their concept, but it is against tool's philosophy, i.e. it is bad.)
-* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and it modifies data of all other analyses during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occurs something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
+* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and it modifies data of all other analyses during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occurs something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such (CPA-concept-breaking) interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
 What is the ideal code-base (i.e. even not real/available, hypothetical) for STATOR from the point of view from members of the STATOR team?

@@ Line 217: / Line 217: @@
 How much restrictive is CPAchecker's concept of CPAs with respect to kind of program analyses we intend to implement in STATOR? (Of course, there is a possibility to circumvent their concept, but it is against tool's philosophy, i.e. it is bad.)
-* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and it modifies data of all other analyses during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occur something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
+* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and it modifies data of all other analyses during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occurs something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
 What is the ideal code-base (i.e. even not real/available, hypothetical) for STATOR from the point of view from members of the STATOR team?

@@ Line 217: / Line 217: @@
 How much restrictive is CPAchecker's concept of CPAs with respect to kind of program analyses we intend to implement in STATOR? (Of course, there is a possibility to circumvent their concept, but it is against tool's philosophy, i.e. it is bad.)
-* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and modifies data of all of them during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occur something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
+* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and it modifies data of all other analyses during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occur something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
 What is the ideal code-base (i.e. even not real/available, hypothetical) for STATOR from the point of view from members of the STATOR team?

@@ Line 205: / Line 205: @@
 TODO: complete the section!
-== Important questions ==
+== Answers to important questions ==
 How much time/programming effort can we actually save when we use languages like F# or OCaml relative to other languages like Java or C++?
-* According to David we cannot achieve notable speed up of implementation by using languages F# or OCaml.
+* Result from the discussion on July 28: According to David we cannot achieve notable speed up of implementation by using languages F# or OCaml.
 How much we can actually benefit (i.e. time/programming effort savings) from the "new-school" control-flow graph representation relative to the use of the "old-school" one?
-* I did not get a clear answer. But it seems that neither David nor George will complain if we do not have it. Perhaps, it is not that important after all.
+* Result from the discussion on July 28: It seems that neither David nor George will complain if we do not have it. Perhaps, it is not that important after all.
 How much is important for as that CPAchecker already provides several program analyses like predicate abstraction?
-* David mentioned pointer and shape analyses and predicate abstraction to be valuable for us.
+* Result from the discussion on July 28: David mentioned pointer and shape analyses and predicate abstraction to be valuable for us. George listed a code we can reuse: TODO.
 How much restrictive is CPAchecker's concept of CPAs with respect to kind of program analyses we intend to implement in STATOR? (Of course, there is a possibility to circumvent their concept, but it is against tool's philosophy, i.e. it is bad.)
-* David wants to be close to the design of Astree. The design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and modifies data of all of them. Moreover, Those other analyses may directly communicate with each other by direct queries.
+* Result from the discussion on July 28: David wants STATOR to be close to the design of Astree. We showed that the design is incompatible with the concept of CPAs in several ways. Instead of composing analyses using cartesian product of latices (with precision adjustment operator) Astree has pointer analysis above all other analyses and modifies data of all of them during whole program analysis as necessary. Moreover, those other analyses may directly communicate with each other by direct queries at any time. Finally, we will also need to run analyses in sequence, like applying constant propagation before other analyses. Regardless of the incompatibilities David and George say that we should try to use the concept of CPA for STATOR and we will see. If there occur something which cannot be implemented as CPA we hack it into CPAchecker differently (there already are analyses like TODO in CPAchecker which circumvent the main concept of the tool). Although Marek accepted the decision of other team members, he still sees this procedure as a source of troubles: Although we can get a functional code at the end, its structure can be unnecessary complex. The code might be difficult to read, understand and thus also difficult to maintain. We a priori cast restrictions to STATOR's code design, although we see from the beginning that the concept of CPAs does not fit our needs. It might be better to surrender the concept of CPA from very beginning, integrate into CPAchecker structure/interfaces which we actually need, and we can use the original concept only in cases when it is obviously applicable. Note that integration of such interfaces into CPAchecker does not imply any negotiation with developers of CPAchecker. We will use the "import" feature of GIT to get CPAchecker into STATOR's repository anyway.
 What is the ideal code-base (i.e. even not real/available, hypothetical) for STATOR from the point of view from members of the STATOR team?
-* David: ???
+* Result from the discussion on July 28: This was not discussed.
 * Marek: In this moment I cannot say, because I do not have clear view of features of our analyses. I need to read related papers first. Even such essential things like "new-school vs. new-school" control-flow graph representation is a mystery for me. So, my opinion to this question does not matter.
 How many PhD students we plan to join the STATOR project till the end of 2017?
-* ???
+* Result from the discussion on July 28: It was not discussed.
 == Results ==

@@ Line 105: / Line 105: @@
 ** Uses LLVM front-end. So we can parse ANSI/GNU programs.
 ** Since it is implemented in C++ we can get close to features of OCaml or F#, but it will require to overload several operators.
 * <b>cons</b>

@@ Line 167: / Line 167: @@
 === KLEE ===
 * <b>pros</b>
-** TODO
+** Uses LLVM front-end. So we can parse ANSI/GNU programs.
 * <b>cons</b>
-** TODO
+** It does not convert LLVM into internal representation. It directly analyses LLVM. So, changes in LLVM has impact potentially to entire tool. Nevertheless, this issue is maintained by LLVM community.
 === CBMC ===

@@ Line 89: / Line 89: @@
 ** According to README.txt file of CPAchecker: "CPAchecker is able to parse and analyze a large subset of (GNU)C." (But unfortunately, I did not find a list of missing features.)
 ** All preprocessed C files passed into the tool are linked into one big file. This is stated in README.txt file of the tool. Bit it is still unclear, whether it works as in a linker (e.i. properly are handled definitions/declarations, externa/static variables and functions, what about functions without definitions, ...), or whether they simply concatenate all the files into big one. Only the former case is valuable for us.
-** There is a support of Z3, MATH SAT 4, and CVC4 SMT solvers. TODO: check it, is it correct??
+** There is a support of Z3, MATH SAT 4, and CVC4 SMT solvers. TODO: check it, is it correct/complete??
 ** The tool has live community, it is frequently improved.
 ** They currently work on front-end to Java. Nevertheless, CFG representation differs from the one of C and it is also the "old-school" one.