function

การทำงาน

ฟังก์ชั่นเป็นเครื่องวิเคราะห์แบบคงที่ต้นแบบการวิจัยที่ออกแบบมาเพื่อพิสูจน์การเลิกจ้างตามเงื่อนไขและการรับประกันแบบมีเงื่อนไขและคุณสมบัติการเกิดซ้ำของโปรแกรม C เครื่องมือจะทำให้ฟังก์ชั่นการจัดอันดับที่กำหนดโดยอัตโนมัติและเงื่อนไขที่เพียงพอสำหรับการยกเลิกการรับประกันและคุณสมบัติการเกิดซ้ำโดยใช้การตีความเชิงนามธรรม

ฟังก์ชั่นได้รับการพัฒนาเพื่อนำไปใช้และทดสอบวิธีการวิเคราะห์และโดเมนนามธรรมที่อธิบายไว้ในบทความ:

 N. Courant, C. Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation.

C. Urban, A. Miné. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation.
In Proc. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015). 

C. Urban, A. Miné. A Decision Tree Abstract Domain for Proving Conditional Termination.
In Proc. 21st International Static Analysis Symposium (SAS 2014).

C. Urban, A. Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions.
In Proc. 23rd European Symposium on Programming (ESOP 2014).

C. Urban. The Abstract Domain of Segmented Ranking Functions.
In Proc. 20th International Static Analysis Symposium (SAS 2013).

เว็บไซต์หลักของฟังก์ชั่นคือ: http://www.di.ens.fr/~urban/function.html

ผู้เขียน

 Caterina Urban, ETH Zurich, [email protected] 

ผู้มีส่วนร่วม

 Naïm Moussaoui Remil, École Normale Supérieure
Samuel Ueltschi, ETH Zurich
Nathanaëlle Courant, École Normale Supérieure

การติดตั้ง

ฟังก์ชั่นต้องใช้แอปพลิเคชันและไลบรารีต่อไปนี้:

• Ocaml

   (sudo) apt-get install ocaml-interp
  

• Findlib

   (sudo) apt-get install ocaml-findlib
  

• Menhir: LR (1) ตัวแยกวิเคราะห์

   (sudo) apt-get install menhir
  

• OPAM: https://opam.ocaml.org/doc/install.html

   (sudo) apt-get install opam
  

• Dune: Ocaml Build System

   opam install dune
  

• ออนซ์

   opam install ounit
  

• ผ้ากันเปื้อน: ไลบรารีโดเมนนามธรรมเชิงตัวเลข

   opam install apron
  

• Zarith: การดำเนินการจำนวนเต็มตามอำเภอใจ

   opam install zarith
  

ฟังก์ชั่นการรวบรวม

เมื่อมีการติดตั้งไลบรารีที่จำเป็นทั้งหมดแล้วฟังก์ชั่นสามารถรวบรวมด้วย 'Dune':

 dune build

สิ่งนี้จะสร้าง 'ฟังก์ชั่น' ฟังก์ชั่น 'ฟังก์ชั่น' ในไดเรกทอรีโครงการ

อีกทางเลือกหนึ่งคือ 'Ocamlbuild' สามารถใช้ในการสร้างฟังก์ชั่นด้วยคำสั่งต่อไปนี้:

 ocamlbuild ml_float.o Main.native -use-ocamlfind -use-menhir -pkgs 'apron,gmp,oUnit,zarith' -I utils -I banal -I domains -I frontend -I cfgfrontend -I main -libs boxMPQ,octD,polkaMPQ,str,zarith -lflags banal/ml_float.o

การใช้งาน

ตัววิเคราะห์บรรทัดคำสั่งสามารถเรียกใช้โดยใช้รูปแบบการโทรต่อไปนี้:

 ./function <file> <analysis> [options] 

โดยที่ "ไฟล์" เป็นพา ธ ไปยังไฟล์ C ที่จะวิเคราะห์และ "การวิเคราะห์" ประเภทของการวิเคราะห์ที่จะดำเนินการ

เครื่องวิเคราะห์ทำการวิเคราะห์การเข้าถึงไปข้างหน้าเป็นครั้งแรกจากนั้นการวิเคราะห์ย้อนหลังเพื่อค้นหาฟังก์ชั่นการจัดอันดับที่กำหนดไว้เป็นชิ้น ๆ

ตัวเลือกบรรทัดคำสั่งทั่วไปต่อไปนี้ได้รับการยอมรับ (แสดงค่าเริ่มต้นของพวกเขา):

 -main main                         set the analyzer entry point (defaults to main)
 -domain boxes|octagons|polyhedra   set the abstract domain (defaults to boxes)
 -joinfwd 2                         set the widening delay in forward analysis
 -joinbwd 2                         set the widening delay in backward analysis
 -meetbwd 2			                set the dual widening delay in backward analysis
 -ordinals 2                        set the maximum ordinal value for the ranking functions
 -refine            			    reduces the backward analysis to the reachabile states

เครื่องวิเคราะห์ตอบเป็นจริงในกรณีที่สามารถพิสูจน์คุณสมบัติได้สำเร็จ มิฉะนั้นจะไม่ทราบคำตอบ

ฟังก์ชั่นสามารถวิเคราะห์คุณสมบัติต่อไปนี้:

• การเลิก
• รับประกัน / กำเริบ
• การคำนวณ-Tree-Logic (CTL)

การเลิก

หากต้องการตรวจสอบการเลิกจ้างให้โทรหาเครื่องวิเคราะห์ด้วยรูปแบบการโทรต่อไปนี้:

 ./function <file> -termination [options]

รับประกัน / กำเริบ

รูปแบบการโทรต่อไปนี้สามารถใช้สำหรับคุณสมบัติการรับประกันหรือคุณสมบัติการเกิดซ้ำ:

 ./function <file> -guarantee <property_file> [options]
./function <file> -recurrence <property_file> [options] 

โดยที่ "property_file" เป็นพา ธ ไปยังไฟล์ที่มีคุณสมบัติการรับประกันหรือการเกิดซ้ำ

CTL

คุณสมบัติ CTL สามารถวิเคราะห์ได้โดยใช้รูปแบบการโทรต่อไปนี้:

 ./function <file> -ctl <property> [options]

โดยที่ "คุณสมบัติ" คือคุณสมบัติ CTL ที่จะวิเคราะห์

ตัวเลือกบรรทัดคำสั่งเพิ่มเติมต่อไปนี้มีอยู่สำหรับการวิเคราะห์ CTL: (แสดงค่าเริ่มต้นของพวกเขา):

 -precondition true                 a precondition that is assumed to hold at the start of the program
 -noinline			                disable inlining of function calls
 -ast                               run the analysis on the abstract-syntax-tree instead of the control-flow-graph,
                                    note that in that case function calls and goto/break/continue are not supported
 -dot                               print out control-flow-graph and decision trees in graphviz dot format