Looking for breakthrough ideas for innovation challenges? Try Patsnap Eureka!

C + + compiler variable action domain formalization method based on Coq

A formal method and scope technology, applied in the field of variable scope formalization of C++ compiler based on Coq, which can solve problems such as inexplicability

Active Publication Date: 2020-02-28
UNIV OF ELECTRONIC SCI & TECH OF CHINA +1
View PDF6 Cites 0 Cited by
  • Summary
  • Abstract
  • Description
  • Claims
  • Application Information

AI Technical Summary

Problems solved by technology

[0005] The invention discloses a method for formalizing the variable scope of a C++ compiler based on Coq, and aims to solve the problem that the Coq interpreter cannot correctly interpret the code containing the variable scope characteristic as a virtual memory instruction sequence

Method used

the structure of the environmentally friendly knitted fabric provided by the present invention; figure 2 Flow chart of the yarn wrapping machine for environmentally friendly knitted fabrics and storage devices; image 3 Is the parameter map of the yarn covering machine
View more

Image

Smart Image Click on the blue labels to locate them in the text.
Viewing Examples
Smart Image
  • C + + compiler variable action domain formalization method based on Coq

Examples

Experimental program
Comparison scheme
Effect test

Embodiment 1

[0081] A Coq-based C++ compiler variable scope formalization method, using the record mathematical model to formalize the table structure, using Inductive induction to define the formal stack structure, using match to match the formal code to cause branching operation logic, using Fixpoint recursive function Formalize the logic of repeated actions.

[0082] Such as figure 1 As shown, the present invention is based on the FSPVM formal verification system and is applied to the Coq interpreter in order to solve the problem that the Coq interpreter cannot correctly interpret the code with variable scope characteristics as a virtual memory instruction sequence. The Coq interpreter cannot correctly interpret the code with the variable scope feature, that is, the Coq interpreter cannot correctly interpret the variable operation method with scope restrictions.

[0083] In order to solve this problem, the present invention abstracts the formalization of the C++ variable scope characteristi...

Embodiment 2

[0087] A Coq-based C++ compiler variable scope formal method, based on the FSPVM formal verification engine, aims to solve the problem that the Coq interpreter cannot correctly interpret the code with variable scope characteristics as a virtual memory instruction sequence. It mainly includes the following steps:

[0088] 1. Formal method of stack structure of global variable scope table and local variable scope table:

[0089] S1. Formalize the table value structure, use the Inductive structure to define the table value, the dmt_init induction represents the initialization table value, and the internal storage of the dmt_unit induction: virtual memory address, variable scope identifier.

[0090] Inductive domain_map_table_v: Type :=

[0091] | dmt_init: domain_map_table_v

[0092] | dmt_unit: high_addres -> address -> dmt_sign -> domain_map_table_v.

[0093] S2. Formalize the table structure, use the Record mathematical model to simulate the table structure, and use the direct access...

the structure of the environmentally friendly knitted fabric provided by the present invention; figure 2 Flow chart of the yarn wrapping machine for environmentally friendly knitted fabrics and storage devices; image 3 Is the parameter map of the yarn covering machine
Login to View More

PUM

No PUM Login to View More

Abstract

The invention discloses a C + + compiler variable action domain formalization method based on Coq. According to the method, a formal table structure of a record mathematical model is adopted, an Inductive induction is adopted to define a formal stack structure, match is adopted to match operation logic causing branches in formal codes, and a Fixpoint recursive function is adopted to formalize repetitive behavior operation logic. When an FSPVM interpreter in the prior art interprets a variable operation method, if the variable operation method has action domain characteristics, wrong interpretation can be caused. By adopting the variable operation method provided by the invention to replace an interpretation variable operation method in an FSPVM interpreter, a new FSPVM interpreter can interpret codes with action domain characteristics. According to the method, a Record mathematical model is used for formalizing a dictionary data structure, and compared with a traditional formalizationmode using an Inductive induction method, the execution efficiency is obviously improved.

Description

Technical field [0001] The invention belongs to the technical field of computer applications, and specifically relates to a Coq-based C++ compiler variable scope formalization method. Background technique [0002] Since the birth of the blockchain and virtual currency market, various security issues have emerged one after another, and the losses caused by hacker attacks due to various security issues have also become the focus of the industry. In order to ensure code security, the industry has proposed a variety of code detection methods. [0003] But regarding the formal verification of EOS smart contracts, there is no mature plan at this stage. This phenomenon is mainly due to the difficulty of formalizing the semantics of industrial-level programs. Formal semantics and formal modeling are to infer and verify the behavior of computer systems. It is necessary to strictly define the semantics of programming languages ​​and use formal models to model the behavior of computer syste...

Claims

the structure of the environmentally friendly knitted fabric provided by the present invention; figure 2 Flow chart of the yarn wrapping machine for environmentally friendly knitted fabrics and storage devices; image 3 Is the parameter map of the yarn covering machine
Login to View More

Application Information

Patent Timeline
no application Login to View More
IPC IPC(8): G06F8/41
CPCG06F8/41
Inventor 雷航王自升李昂杨拯钱伟中唐琴曾惟如晏昃晖
Owner UNIV OF ELECTRONIC SCI & TECH OF CHINA
Who we serve
  • R&D Engineer
  • R&D Manager
  • IP Professional
Why Patsnap Eureka
  • Industry Leading Data Capabilities
  • Powerful AI technology
  • Patent DNA Extraction
Social media
Patsnap Eureka Blog
Learn More
PatSnap group products

Browse by: Latest US Patents, China's latest patents, Technical Efficacy Thesaurus, Application Domain, Technology Topic, Popular Technical Reports.

© 2024 PatSnap. All rights reserved.Legal|Privacy policy|Modern Slavery Act Transparency Statement|Sitemap|About US| Contact US: help@patsnap.com